add_torsor_auto.lean

/-
Copyright (c) 2020 Joseph Myers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Myers, Yury Kudryashov.
-/
import PrePort
import Lean3Lib.init.default
import Mathlib.algebra.group.prod
import Mathlib.algebra.group.type_tags
import Mathlib.algebra.group.pi
import Mathlib.algebra.pointwise
import Mathlib.data.equiv.basic
import Mathlib.data.set.finite
import PostPort

universes u_1 u_2 l u_3 u_4 u v w 

namespace Mathlib

/-!
# Torsors of additive group actions

This file defines torsors of additive group actions.

## Notations

The group elements are referred to as acting on points.  This file
defines the notation `+ᵥ` for adding a group element to a point and
`-ᵥ` for subtracting two points to produce a group element.

## Implementation notes

Affine spaces are the motivating example of torsors of additive group actions. It may be appropriate
to refactor in terms of the general definition of group actions, via `to_additive`, when there is a
use for multiplicative torsors (currently mathlib only develops the theory of group actions for
multiplicative group actions).

## Notations

* `v +ᵥ p` is a notation for `has_vadd.vadd`, the left action of an additive monoid;

* `p₁ -ᵥ p₂` is a notation for `has_vsub.vsub`, difference between two points in an additive torsor
  as an element of the corresponding additive group;

## References

* https://en.wikipedia.org/wiki/Principal_homogeneous_space
* https://en.wikipedia.org/wiki/Affine_space

-/

/-- Type class for the `+ᵥ` notation. -/

class has_vadd (G : Type u_1) (P : Type u_2) : Type (max u_1 u_2)
where
  vadd : G → P → P

/-- Type class for the `-ᵥ` notation. -/

class has_vsub (G : outParam (Type u_1)) (P : Type u_2) : Type (max u_1 u_2)
where
  vsub : P → P → G

infixl:65 " +ᵥ " => Mathlib.has_vadd.vadd

infixl:65 " -ᵥ " => Mathlib.has_vsub.vsub

/-- Type class for additive monoid actions. -/

class add_action (G : Type u_1) (P : Type u_2) [add_monoid G] : Type (max u_1 u_2)
where
  vadd : G → P → P
  zero_vadd' : ∀ (p : P), 0 +ᵥ p = p
  vadd_assoc' : ∀ (g1 g2 : G) (p : P), g1 +ᵥ (g2 +ᵥ p) = g1 + g2 +ᵥ p

/-- An `add_torsor G P` gives a structure to the nonempty type `P`,
acted on by an `add_group G` with a transitive and free action given
by the `+ᵥ` operation and a corresponding subtraction given by the
`-ᵥ` operation. In the case of a vector space, it is an affine
space. -/

class add_torsor (G : outParam (Type u_1)) (P : Type u_2) [outParam (add_group G)] : Type (max u_1 u_2)
where
  vadd : G → P → P
  zero_vadd' : ∀ (p : P), 0 +ᵥ p = p
  vadd_assoc' : ∀ (g1 g2 : G) (p : P), g1 +ᵥ (g2 +ᵥ p) = g1 + g2 +ᵥ p
  vsub : P → P → G
  nonempty : Nonempty P
  vsub_vadd' : ∀ (p1 p2 : P), p1 -ᵥ p2 +ᵥ p2 = p1
  vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g

/-- An `add_group G` is a torsor for itself. -/

protected instance add_group_is_add_torsor (G : Type u_1) [add_group G] : add_torsor G G := sorry

/-- Simplify addition for a torsor for an `add_group G` over
itself. -/

@[simp] theorem vadd_eq_add {G : Type u_1} [add_group G] (g1 : G) (g2 : G) : g1 +ᵥ g2 = g1 + g2 := sorry

/-- Simplify subtraction for a torsor for an `add_group G` over
itself. -/

@[simp] theorem vsub_eq_sub {G : Type u_1} [add_group G] (g1 : G) (g2 : G) : g1 -ᵥ g2 = g1 - g2 := sorry

/-- Adding the zero group element to a point gives the same point. -/

@[simp] theorem zero_vadd (G : Type u_1) {P : Type u_2} [add_monoid G] [A : add_action G P] (p : P) : 0 +ᵥ p = p := sorry

/-- Adding two group elements to a point produces the same result as
adding their sum. -/

theorem vadd_assoc {G : Type u_1} {P : Type u_2} [add_monoid G] [A : add_action G P] (g1 : G) (g2 : G) (p : P) : g1 +ᵥ (g2 +ᵥ p) = g1 + g2 +ᵥ p := sorry

/-- Adding two group elements to a point produces the same result in either
order. -/

theorem vadd_comm (G : Type u_1) {P : Type u_2} [add_comm_monoid G] [A : add_action G P] (p : P) (g1 : G) (g2 : G) : g1 +ᵥ (g2 +ᵥ p) = g2 +ᵥ (g1 +ᵥ p) := sorry

/-- If the same group element added to two points produces equal results,
those points are equal. -/

theorem vadd_left_cancel {G : Type u_1} {P : Type u_2} [add_group G] [A : add_action G P] {p1 : P} {p2 : P} (g : G) (h : g +ᵥ p1 = g +ᵥ p2) : p1 = p2 := sorry

@[simp] theorem vadd_left_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [A : add_action G P] {p₁ : P} {p₂ : P} (g : G) : g +ᵥ p₁ = g +ᵥ p₂ ↔ p₁ = p₂ := sorry

/-- Adding the group element `g` to a point is an injective function. -/

theorem vadd_left_injective {G : Type u_1} (P : Type u_2) [add_group G] [A : add_action G P] (g : G) : function.injective (has_vadd.vadd g) := sorry

/-- Adding the result of subtracting from another point produces that
point. -/

@[simp] theorem vsub_vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p1 : P) (p2 : P) : p1 -ᵥ p2 +ᵥ p2 = p1 := sorry

/-- Adding a group element then subtracting the original point
produces that group element. -/

@[simp] theorem vadd_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (g : G) (p : P) : g +ᵥ p -ᵥ p = g := sorry

/-- If the same point added to two group elements produces equal
results, those group elements are equal. -/

theorem vadd_right_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {g1 : G} {g2 : G} (p : P) (h : g1 +ᵥ p = g2 +ᵥ p) : g1 = g2 := sorry

@[simp] theorem vadd_right_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {g1 : G} {g2 : G} (p : P) : g1 +ᵥ p = g2 +ᵥ p ↔ g1 = g2 := sorry

/-- Adding a group element to the point `p` is an injective
function. -/

theorem vadd_right_injective {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p : P) : function.injective fun (_x : G) => _x +ᵥ p := sorry

/-- Adding a group element to a point, then subtracting another point,
produces the same result as subtracting the points then adding the
group element. -/

theorem vadd_vsub_assoc {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (g : G) (p1 : P) (p2 : P) : g +ᵥ p1 -ᵥ p2 = g + (p1 -ᵥ p2) := sorry

/-- Subtracting a point from itself produces 0. -/

@[simp] theorem vsub_self {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p : P) : p -ᵥ p = 0 := sorry

/-- If subtracting two points produces 0, they are equal. -/

theorem eq_of_vsub_eq_zero {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {p1 : P} {p2 : P} (h : p1 -ᵥ p2 = 0) : p1 = p2 := sorry

/-- Subtracting two points produces 0 if and only if they are
equal. -/

@[simp] theorem vsub_eq_zero_iff_eq {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {p1 : P} {p2 : P} : p1 -ᵥ p2 = 0 ↔ p1 = p2 := sorry

/-- Cancellation adding the results of two subtractions. -/

@[simp] theorem vsub_add_vsub_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p1 : P) (p2 : P) (p3 : P) : p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3 := sorry

/-- Subtracting two points in the reverse order produces the negation
of subtracting them. -/

@[simp] theorem neg_vsub_eq_vsub_rev {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p1 : P) (p2 : P) : -(p1 -ᵥ p2) = p2 -ᵥ p1 := sorry

/-- Subtracting the result of adding a group element produces the same result
as subtracting the points and subtracting that group element. -/

theorem vsub_vadd_eq_vsub_sub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p1 : P) (p2 : P) (g : G) : p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g := sorry

/-- Cancellation subtracting the results of two subtractions. -/

@[simp] theorem vsub_sub_vsub_cancel_right {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p1 : P) (p2 : P) (p3 : P) : p1 -ᵥ p3 - (p2 -ᵥ p3) = p1 -ᵥ p2 := sorry

/-- Convert between an equality with adding a group element to a point
and an equality of a subtraction of two points with a group
element. -/

theorem eq_vadd_iff_vsub_eq {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p1 : P) (g : G) (p2 : P) : p1 = g +ᵥ p2 ↔ p1 -ᵥ p2 = g := sorry

theorem vadd_eq_vadd_iff_neg_add_eq_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {v₁ : G} {v₂ : G} {p₁ : P} {p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂ := sorry

namespace set


protected instance has_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] : has_vsub (set G) (set P) := sorry

@[simp] theorem vsub_empty {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (s : set P) : s -ᵥ ∅ = ∅ := sorry

@[simp] theorem empty_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (s : set P) : ∅ -ᵥ s = ∅ := sorry

@[simp] theorem singleton_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (s : set P) (p : P) : singleton p -ᵥ s = has_vsub.vsub p '' s := sorry

@[simp] theorem vsub_singleton {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (s : set P) (p : P) : s -ᵥ singleton p = (fun (_x : P) => _x -ᵥ p) '' s := sorry

@[simp] theorem singleton_vsub_self {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p : P) : singleton p -ᵥ singleton p = singleton 0 := sorry

/-- `vsub` of a finite set is finite. -/

theorem finite.vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {s : set P} {t : set P} (hs : finite s) (ht : finite t) : finite (s -ᵥ t) := sorry

/-- Each pairwise difference is in the `vsub` set. -/

theorem vsub_mem_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {s : set P} {t : set P} {ps : P} {pt : P} (hs : ps ∈ s) (ht : pt ∈ t) : ps -ᵥ pt ∈ s -ᵥ t := sorry

/-- `s -ᵥ t` is monotone in both arguments. -/

theorem vsub_subset_vsub {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {s : set P} {t : set P} {s' : set P} {t' : set P} (hs : s ⊆ s') (ht : t ⊆ t') : s -ᵥ t ⊆ s' -ᵥ t' := sorry

theorem vsub_self_mono {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {s : set P} {t : set P} (h : s ⊆ t) : s -ᵥ s ⊆ t -ᵥ t := sorry

theorem vsub_subset_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {s : set P} {t : set P} {u : set G} : s -ᵥ t ⊆ u ↔ ∀ (x : P), x ∈ s → ∀ (y : P), y ∈ t → x -ᵥ y ∈ u := sorry

protected instance add_action {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] : add_action (set G) (set P) := sorry

theorem vadd_subset_vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {s : set G} {s' : set G} {t : set P} {t' : set P} (hs : s ⊆ s') (ht : t ⊆ t') : s +ᵥ t ⊆ s' +ᵥ t' := sorry

@[simp] theorem vadd_singleton {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (s : set G) (p : P) : s +ᵥ singleton p = (fun (_x : G) => _x +ᵥ p) '' s := sorry

@[simp] theorem singleton_vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (v : G) (s : set P) : singleton v +ᵥ s = has_vadd.vadd v '' s := sorry

theorem finite.vadd {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {s : set G} {t : set P} (hs : finite s) (ht : finite t) : finite (s +ᵥ t) := sorry

end set


@[simp] theorem vadd_vsub_vadd_cancel_right {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (v₁ : G) (v₂ : G) (p : P) : v₁ +ᵥ p -ᵥ (v₂ +ᵥ p) = v₁ - v₂ := sorry

/-- If the same point subtracted from two points produces equal
results, those points are equal. -/

theorem vsub_left_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {p1 : P} {p2 : P} {p : P} (h : p1 -ᵥ p = p2 -ᵥ p) : p1 = p2 := sorry

/-- The same point subtracted from two points produces equal results
if and only if those points are equal. -/

@[simp] theorem vsub_left_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {p1 : P} {p2 : P} {p : P} : p1 -ᵥ p = p2 -ᵥ p ↔ p1 = p2 := sorry

/-- Subtracting the point `p` is an injective function. -/

theorem vsub_left_injective {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p : P) : function.injective fun (_x : P) => _x -ᵥ p := sorry

/-- If subtracting two points from the same point produces equal
results, those points are equal. -/

theorem vsub_right_cancel {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {p1 : P} {p2 : P} {p : P} (h : p -ᵥ p1 = p -ᵥ p2) : p1 = p2 := sorry

/-- Subtracting two points from the same point produces equal results
if and only if those points are equal. -/

@[simp] theorem vsub_right_cancel_iff {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] {p1 : P} {p2 : P} {p : P} : p -ᵥ p1 = p -ᵥ p2 ↔ p1 = p2 := sorry

/-- Subtracting a point from the point `p` is an injective
function. -/

theorem vsub_right_injective {G : Type u_1} {P : Type u_2} [add_group G] [T : add_torsor G P] (p : P) : function.injective (has_vsub.vsub p) := sorry

/-- Cancellation subtracting the results of two subtractions. -/

@[simp] theorem vsub_sub_vsub_cancel_left {G : Type u_1} {P : Type u_2} [add_comm_group G] [add_torsor G P] (p1 : P) (p2 : P) (p3 : P) : p3 -ᵥ p2 - (p3 -ᵥ p1) = p1 -ᵥ p2 := sorry

@[simp] theorem vadd_vsub_vadd_cancel_left {G : Type u_1} {P : Type u_2} [add_comm_group G] [add_torsor G P] (v : G) (p1 : P) (p2 : P) : v +ᵥ p1 -ᵥ (v +ᵥ p2) = p1 -ᵥ p2 := sorry

theorem vsub_vadd_comm {G : Type u_1} {P : Type u_2} [add_comm_group G] [add_torsor G P] (p1 : P) (p2 : P) (p3 : P) : p1 -ᵥ p2 +ᵥ p3 = p3 -ᵥ p2 +ᵥ p1 := sorry

theorem vadd_eq_vadd_iff_sub_eq_vsub {G : Type u_1} {P : Type u_2} [add_comm_group G] [add_torsor G P] {v₁ : G} {v₂ : G} {p₁ : P} {p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂ := sorry

theorem vsub_sub_vsub_comm {G : Type u_1} {P : Type u_2} [add_comm_group G] [add_torsor G P] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) : p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄) := sorry

namespace prod


protected instance add_torsor {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' P'] : add_torsor (G × G') (P × P') := sorry

@[simp] theorem fst_vadd {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' P'] (v : G × G') (p : P × P') : fst (v +ᵥ p) = fst v +ᵥ fst p := sorry

@[simp] theorem snd_vadd {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' P'] (v : G × G') (p : P × P') : snd (v +ᵥ p) = snd v +ᵥ snd p := sorry

@[simp] theorem mk_vadd_mk {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' P'] (v : G) (v' : G') (p : P) (p' : P') : (v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p') := sorry

@[simp] theorem fst_vsub {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' P'] (p₁ : P × P') (p₂ : P × P') : fst (p₁ -ᵥ p₂) = fst p₁ -ᵥ fst p₂ := sorry

@[simp] theorem snd_vsub {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' P'] (p₁ : P × P') (p₂ : P × P') : snd (p₁ -ᵥ p₂) = snd p₁ -ᵥ snd p₂ := sorry

@[simp] theorem mk_vsub_mk {G : Type u_1} {P : Type u_2} {G' : Type u_3} {P' : Type u_4} [add_group G] [add_group G'] [add_torsor G P] [add_torsor G' P'] (p₁ : P) (p₂ : P) (p₁' : P') (p₂' : P') : (p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂') := sorry

end prod


namespace pi


/-- A product of `add_torsor`s is an `add_torsor`. -/

protected instance add_torsor {I : Type u} {fg : I → Type v} [(i : I) → add_group (fg i)] {fp : I → Type w} [T : (i : I) → add_torsor (fg i) (fp i)] : add_torsor ((i : I) → fg i) ((i : I) → fp i) := sorry

/-- Addition in a product of `add_torsor`s. -/

@[simp] theorem vadd_apply {I : Type u} {fg : I → Type v} [(i : I) → add_group (fg i)] {fp : I → Type w} [T : (i : I) → add_torsor (fg i) (fp i)] (x : (i : I) → fg i) (y : (i : I) → fp i) {i : I} : has_vadd.vadd x y i = x i +ᵥ y i := sorry

end pi


namespace equiv


/-- `v ↦ v +ᵥ p` as an equivalence. -/

def vadd_const {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (p : P) : G ≃ P := sorry

@[simp] theorem coe_vadd_const {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (p : P) : ⇑(vadd_const p) = fun (v : G) => v +ᵥ p := sorry

@[simp] theorem coe_vadd_const_symm {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (p : P) : ⇑(equiv.symm (vadd_const p)) = fun (p' : P) => p' -ᵥ p := sorry

/-- `p' ↦ p -ᵥ p'` as an equivalence. -/

def const_vsub {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (p : P) : P ≃ G := sorry

@[simp] theorem coe_const_vsub {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (p : P) : ⇑(const_vsub p) = has_vsub.vsub p := sorry

@[simp] theorem coe_const_vsub_symm {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (p : P) : ⇑(equiv.symm (const_vsub p)) = fun (v : G) => -v +ᵥ p := sorry

/-- The permutation given by `p ↦ v +ᵥ p`. -/

def const_vadd {G : Type u_1} (P : Type u_2) [add_group G] [add_torsor G P] (v : G) : perm P := sorry

@[simp] theorem coe_const_vadd {G : Type u_1} (P : Type u_2) [add_group G] [add_torsor G P] (v : G) : ⇑(const_vadd P v) = has_vadd.vadd v := sorry

@[simp] theorem const_vadd_zero (G : Type u_1) (P : Type u_2) [add_group G] [add_torsor G P] : const_vadd P 0 = 1 := sorry

@[simp] theorem const_vadd_add {G : Type u_1} (P : Type u_2) [add_group G] [add_torsor G P] (v₁ : G) (v₂ : G) : const_vadd P (v₁ + v₂) = const_vadd P v₁ * const_vadd P v₂ := sorry

/-- `equiv.const_vadd` as a homomorphism from `multiplicative G` to `equiv.perm P` -/

def const_vadd_hom {G : Type u_1} (P : Type u_2) [add_group G] [add_torsor G P] : multiplicative G →* perm P := sorry

/-- Point reflection in `x` as a permutation. -/

def point_reflection {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (x : P) : perm P := sorry

theorem point_reflection_apply {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (x : P) (y : P) : coe_fn (point_reflection x) y = x -ᵥ y +ᵥ x := sorry

@[simp] theorem point_reflection_symm {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (x : P) : equiv.symm (point_reflection x) = point_reflection x := sorry

@[simp] theorem point_reflection_self {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (x : P) : coe_fn (point_reflection x) x = x := sorry

theorem point_reflection_involutive {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] (x : P) : function.involutive ⇑(point_reflection x) := sorry

/-- `x` is the only fixed point of `point_reflection x`. This lemma requires
`x + x = y + y ↔ x = y`. There is no typeclass to use here, so we add it as an explicit argument. -/

theorem point_reflection_fixed_iff_of_injective_bit0 {G : Type u_1} {P : Type u_2} [add_group G] [add_torsor G P] {x : P} {y : P} (h : function.injective bit0) : coe_fn (point_reflection x) y = y ↔ y = x := sorry

theorem injective_point_reflection_left_of_injective_bit0 {G : Type u_1} {P : Type u_2} [add_comm_group G] [add_torsor G P] (h : function.injective bit0) (y : P) : function.injective fun (x : P) => coe_fn (point_reflection x) y := sorry