awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
have rw : -v₁ + v₂ = p₁ -ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
Tactic: rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : -v₁ + v₂ = p₁ -ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
have rw₁ : v₂ - v₁ = p₁ -ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
Tactic: rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ p₄ : P
⊢ p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
have rw : p₁ -ᵥ ((p₃ -ᵥ p₄) +ᵥ p₂) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
Tactic: rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ p₄ : P
rw : p₁ -ᵥ ((p₃ -ᵥ p₄) +ᵥ p₂) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
⊢ p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
have rw₁ : p₁ -ᵥ ((p₂ -ᵥ p₄) +ᵥ p₃) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
Tactic: rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ p₄ : P
rw : p₁ -ᵥ ((p₃ -ᵥ p₄) +ᵥ p₂) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
rw₁ : p₁ -ᵥ ((p₂ -ᵥ p₄) +ᵥ p₃) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
⊢ p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
have rw₂ : p₁ -ᵥ p₃ - (p₂ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
Tactic: rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v : G
s t : Set P
⊢ (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t
have h : ∀ (x : G), x ∈ (v +ᵥ s) -ᵥ (v +ᵥ t) ↔ x ∈ s -ᵥ t
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₃ : -(x -ᵥ y) = x -ᵥ y ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
rw₃ : -(x -ᵥ y) = x -ᵥ y ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₄ : x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
rw₃ : -(x -ᵥ y) = x -ᵥ y ↔ y = x
rw₄ : x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₅ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = 0 ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
rw₃ : -(x -ᵥ y) = x -ᵥ y ↔ y = x
rw₄ : x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x
rw₅ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = 0 ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₆ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = HSMul.hSMul (α := ℕ) (β := G) 2 0 ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
rw₃ : -(x -ᵥ y) = x -ᵥ y ↔ y = x
rw₄ : x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x
rw₅ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = 0 ↔ y = x
rw₆ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = HSMul.hSMul (α := ℕ) (β := G) 2 0 ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₇ : x -ᵥ y = 0 ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
rw₃ : -(x -ᵥ y) = x -ᵥ y ↔ y = x
rw₄ : x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x
rw₅ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = 0 ↔ y = x
rw₆ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = HSMul.hSMul (α := ℕ) (β := G) 2 0 ↔ y = x
rw₇ : x -ᵥ y = 0 ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₈ : x = y ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
rw : (x -ᵥ y) +ᵥ x = y ↔ y = x
rw₁ : y = (x -ᵥ y) +ᵥ x ↔ y = x
rw₂ : y -ᵥ x = x -ᵥ y ↔ y = x
rw₃ : -(x -ᵥ y) = x -ᵥ y ↔ y = x
rw₄ : x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x
rw₅ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = 0 ↔ y = x
rw₆ : HSMul.hSMul (α := ℕ) 2 (x -ᵥ y) = HSMul.hSMul (α := ℕ) (β := G) 2 0 ↔ y = x
rw₇ : x -ᵥ y = 0 ↔ y = x
rw₈ : x = y ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = y ↔ y = x
have rw₉ : y = x ↔ y = x
Tactic: rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
⊢ x₁ = x₂
have rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
⊢ x₁ = x₂
have rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
⊢ x₁ = x₂
have rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
⊢ x₁ = x₂
have rwa₃ : ∀ (hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
rwa₃ : ∀ (hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂), x₁ = x₂
⊢ x₁ = x₂
have rwa₄ : ∀ (hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
rwa₃ : ∀ (hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂), x₁ = x₂
rwa₄ : ∀ (hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂), x₁ = x₂
⊢ x₁ = x₂
have rwa₅ : ∀ (hy : x₁ -ᵥ x₂ + (x₁ -ᵥ x₂) = 0), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
rwa₃ : ∀ (hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂), x₁ = x₂
rwa₄ : ∀ (hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂), x₁ = x₂
rwa₅ : ∀ (hy : x₁ -ᵥ x₂ + (x₁ -ᵥ x₂) = 0), x₁ = x₂
⊢ x₁ = x₂
have rwa₆ : ∀ (hy : HSMul.hSMul (α := ℕ) 2 (x₁ -ᵥ x₂) = 0), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
rwa₃ : ∀ (hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂), x₁ = x₂
rwa₄ : ∀ (hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂), x₁ = x₂
rwa₅ : ∀ (hy : x₁ -ᵥ x₂ + (x₁ -ᵥ x₂) = 0), x₁ = x₂
rwa₆ : ∀ (hy : HSMul.hSMul (α := ℕ) 2 (x₁ -ᵥ x₂) = 0), x₁ = x₂
⊢ x₁ = x₂
have rwa₇ : ∀ (hy : HSMul.hSMul (α := ℕ) 2 (x₁ -ᵥ x₂) = HSMul.hSMul (α := ℕ) (β := G) 2 0), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
rwa₃ : ∀ (hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂), x₁ = x₂
rwa₄ : ∀ (hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂), x₁ = x₂
rwa₅ : ∀ (hy : x₁ -ᵥ x₂ + (x₁ -ᵥ x₂) = 0), x₁ = x₂
rwa₆ : ∀ (hy : HSMul.hSMul (α := ℕ) 2 (x₁ -ᵥ x₂) = 0), x₁ = x₂
rwa₇ : ∀ (hy : HSMul.hSMul (α := ℕ) 2 (x₁ -ᵥ x₂) = HSMul.hSMul (α := ℕ) (β := G) 2 0), x₁ = x₂
⊢ x₁ = x₂
have rwa₈ : ∀ (hy : x₁ -ᵥ x₂ = 0), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
P : Type u_4
inst : AddCommGroup G
inst_1 : AddTorsor G P
h : Injective (β := G) fun (x : G) ↦ HSMul.hSMul (α := ℕ) 2 x
y x₁ x₂ : P
hy : Eq (α := P) ((pointReflection x₁ : (a : P) → P) y : P) ((pointReflection x₂ : (a : P) → P) y : P)
rwa : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂ : (a : P) → P) y), x₁ = x₂
rwa₁ : ∀ (hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂), x₁ = x₂
rwa₂ : ∀ (hy : x₂ -ᵥ y - (x₁ -ᵥ y) = x₁ -ᵥ x₂), x₁ = x₂
rwa₃ : ∀ (hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂), x₁ = x₂
rwa₄ : ∀ (hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂), x₁ = x₂
rwa₅ : ∀ (hy : x₁ -ᵥ x₂ + (x₁ -ᵥ x₂) = 0), x₁ = x₂
rwa₆ : ∀ (hy : HSMul.hSMul (α := ℕ) 2 (x₁ -ᵥ x₂) = 0), x₁ = x₂
rwa₇ : ∀ (hy : HSMul.hSMul (α := ℕ) 2 (x₁ -ᵥ x₂) = HSMul.hSMul (α := ℕ) (β := G) 2 0), x₁ = x₂
rwa₈ : ∀ (hy : x₁ -ᵥ x₂ = 0), x₁ = x₂
⊢ x₁ = x₂
have rwa₉ : ∀ (hy : x₁ = x₂), x₁ = x₂
Tactic: rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_3
inst : AddCommGroup G
x : G
⊢ pointReflection x = Equiv.subLeft (HSMul.hSMul (α := ℕ) 2 x)
have H : ∀ (x_1 : G),
  Eq (α := G) ((pointReflection x : (a : G) → G) x_1 : G)
    ((Equiv.subLeft (HSMul.hSMul (α := ℕ) 2 x) : (a : G) → G) x_1 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g₁ g₂ : G
p : P
h : g₁ +ᵥ p = g₂ +ᵥ p
⊢ g₁ = g₂
have rw : (g₁ +ᵥ p) -ᵥ p = g₂
Tactic: rw [← vadd_vsub g₁ p, h, vadd_vsub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g₁ g₂ : G
p : P
h : g₁ +ᵥ p = g₂ +ᵥ p
rw : (g₁ +ᵥ p) -ᵥ p = g₂
⊢ g₁ = g₂
have rw₁ : (g₂ +ᵥ p) -ᵥ p = g₂
Tactic: rw [← vadd_vsub g₁ p, h, vadd_vsub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g₁ g₂ : G
p : P
h : g₁ +ᵥ p = g₂ +ᵥ p
rw : (g₁ +ᵥ p) -ᵥ p = g₂
rw₁ : (g₂ +ᵥ p) -ᵥ p = g₂
⊢ g₁ = g₂
have rw₂ : g₂ = g₂
Tactic: rw [← vadd_vsub g₁ p, h, vadd_vsub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
⊢ (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)
have apply : ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
Tactic: apply vadd_right_cancel p₂
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
⊢ ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
have rw : g +ᵥ p₁ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
Tactic: rw [vsub_vadd, add_vadd, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
rw : g +ᵥ p₁ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
⊢ ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
have rw₁ : g +ᵥ p₁ = g +ᵥ (p₁ -ᵥ p₂) +ᵥ p₂
Tactic: rw [vsub_vadd, add_vadd, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
rw : g +ᵥ p₁ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
rw₁ : g +ᵥ p₁ = g +ᵥ (p₁ -ᵥ p₂) +ᵥ p₂
⊢ ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
have rw₂ : g +ᵥ p₁ = g +ᵥ p₁
Tactic: rw [vsub_vadd, add_vadd, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
⊢ p -ᵥ p = 0
have rw : 0 + (p -ᵥ p) = 0
Tactic: rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
rw : 0 + (p -ᵥ p) = 0
⊢ p -ᵥ p = 0
have rw₁ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p -ᵥ p = 0
Tactic: rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
rw : 0 + (p -ᵥ p) = 0
rw₁ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p -ᵥ p = 0
⊢ p -ᵥ p = 0
have rw₂ : Eq.{u_1 + 1} (α := G) 0 0
Tactic: rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
h : p₁ -ᵥ p₂ = 0
⊢ p₁ = p₂
have rw : (p₁ -ᵥ p₂) +ᵥ p₂ = p₂
Tactic: rw [← vsub_vadd p₁ p₂, h, zero_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
h : p₁ -ᵥ p₂ = 0
rw : (p₁ -ᵥ p₂) +ᵥ p₂ = p₂
⊢ p₁ = p₂
have rw₁ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₂ = p₂
Tactic: rw [← vsub_vadd p₁ p₂, h, zero_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
h : p₁ -ᵥ p₂ = 0
rw : (p₁ -ᵥ p₂) +ᵥ p₂ = p₂
rw₁ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₂ = p₂
⊢ p₁ = p₂
have rw₂ : p₂ = p₂
Tactic: rw [← vsub_vadd p₁ p₂, h, zero_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃
have apply : (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
Tactic: apply vadd_right_cancel p₃
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
have rw : (p₁ -ᵥ p₂) +ᵥ (p₂ -ᵥ p₃) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
Tactic: rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
rw : (p₁ -ᵥ p₂) +ᵥ (p₂ -ᵥ p₃) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
have rw₁ : (p₁ -ᵥ p₂) +ᵥ p₂ = (p₁ -ᵥ p₃) +ᵥ p₃
Tactic: rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
rw : (p₁ -ᵥ p₂) +ᵥ (p₂ -ᵥ p₃) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
rw₁ : (p₁ -ᵥ p₂) +ᵥ p₂ = (p₁ -ᵥ p₃) +ᵥ p₃
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
have rw₂ : p₁ = (p₁ -ᵥ p₃) +ᵥ p₃
Tactic: rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
rw : (p₁ -ᵥ p₂) +ᵥ (p₂ -ᵥ p₃) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
rw₁ : (p₁ -ᵥ p₂) +ᵥ p₂ = (p₁ -ᵥ p₃) +ᵥ p₃
rw₂ : p₁ = (p₁ -ᵥ p₃) +ᵥ p₃
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
have rw₃ : p₁ = p₁
Tactic: rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁
have refine : (p₁ -ᵥ p₂ + (p₂ -ᵥ p₁)) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
Tactic: refine neg_eq_of_add_eq_zero_right (vadd_right_cancel p₁ ?_)
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Defs (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₁)) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
have rw : (p₁ -ᵥ p₁) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
Tactic: rw [vsub_add_vsub_cancel, vsub_self]