awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₁ +ᵥ p₁) -ᵥ p₂ - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
rw₁ : v₁ + (p₁ -ᵥ p₂) - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
rw₂ : v₁ + (p₁ -ᵥ p₂ - v₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
rw₃ rw₄ : v₁ - v₂ + (p₁ -ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
⊢ (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)

Tactic:
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_assoc, ← add_comm_sub]

Premises used: add_sub_assoc, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm_sub
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ - v₂ + (p₁ -ᵥ p₂) = (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂)

Tactic:
vadd_vsub_vadd_comm _ _ _ _ |>.symm

Premises used: vadd_vsub_vadd_comm, Eq.symm
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ : P
rw : p₁ -ᵥ p₂ + (p₃ -ᵥ p₁ - (p₃ -ᵥ p₂)) = 0
⊢ (p₁ -ᵥ p₂) +ᵥ p₃ = (p₃ -ᵥ p₂) +ᵥ p₁

Tactic:
rw [← @vsub_eq_zero_iff_eq G, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂)) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂
rw₁ rw₂ : v₂ - v₁ = p₁ -ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂

Tactic:
rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]

Premises used: vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₄)
rw₂ rw₃ : p₁ -ᵥ p₃ - (p₂ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
⊢ p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)

Tactic:
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]

Premises used: vsub_vadd_comm, vsub_vadd_eq_vsub_sub
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v : G
s t : Set P
h : ∀ (x : G), x ∈ (v +ᵥ s) -ᵥ (v +ᵥ t) ↔ x ∈ s -ᵥ t
⊢ (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t

Tactic:
ext
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v : G
s t : Set P
x : G
⊢ x ∈ (v +ᵥ s) -ᵥ (v +ᵥ t) ↔ x ∈ s -ᵥ t

Tactic:
simp [mem_vsub, mem_vadd_set]

Premises used: Set.mem_vadd_set, Set.mem_vsub
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst : AddGroup G
inst_1 : AddGroup G'
inst_2 : AddTorsor G P
inst_3 : AddTorsor G' P'
v : G × G'
p : P × P'
⊢ (v +ᵥ p).1 = v.1 +ᵥ p.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst : AddGroup G
inst_1 : AddGroup G'
inst_2 : AddTorsor G P
inst_3 : AddTorsor G' P'
v : G × G'
p : P × P'
⊢ (v +ᵥ p).2 = v.2 +ᵥ p.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst : AddGroup G
inst_1 : AddGroup G'
inst_2 : AddTorsor G P
inst_3 : AddTorsor G' P'
v : G
v' : G'
p : P
p' : P'
⊢ (v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst : AddGroup G
inst_1 : AddGroup G'
inst_2 : AddTorsor G P
inst_3 : AddTorsor G' P'
p₁ p₂ : P × P'
⊢ (p₁ -ᵥ p₂).1 = p₁.1 -ᵥ p₂.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst : AddGroup G
inst_1 : AddGroup G'
inst_2 : AddTorsor G P
inst_3 : AddTorsor G' P'
p₁ p₂ : P × P'
⊢ (p₁ -ᵥ p₂).2 = p₁.2 -ᵥ p₂.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst : AddGroup G
inst_1 : AddGroup G'
inst_2 : AddTorsor G P
inst_3 : AddTorsor G' P'
p₁ p₂ : P
p₁' p₂' : P'
⊢ (p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
I : Type u
fg : I → Type v
inst : (i : I) → AddGroup (fg i)
fp : I → Type w
inst_1 : (i : I) → AddTorsor.{v, w} (fg i) (fp i)
p q : (i : I) → fp i
i : I
⊢ (p -ᵥ q) i = p i -ᵥ q i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
I : Type u
fg : I → Type v
inst : (i : I) → AddGroup (fg i)
fp : I → Type w
inst_1 : (i : I) → AddTorsor.{v, w} (fg i) (fp i)
p q : (i : I) → fp i
⊢ p -ᵥ q = fun (i : I) ↦ p i -ᵥ q i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
⊢ constVAdd P 0 = 1

Tactic:
ext <| zero_vadd G

Premises used: Equiv.ext, zero_vadd
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
⊢ constVAdd P (v₁ + v₂) = constVAdd P v₁ * constVAdd P v₂

Tactic:
ext <| add_vadd v₁ v₂

Premises used: AddSemigroupAction.add_vadd, Equiv.ext
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
⊢ -(x -ᵥ (pointReflection x : (a : P) → P) y) = -(y -ᵥ x)

Tactic:
simp
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
⊢ -(y -ᵥ (pointReflection x : (a : P) → P) y) = -HSMul.hSMul (α := ℕ) 2 (y -ᵥ x)

Tactic:
simp [← neg_nsmul]

Premises used: neg_nsmul
-- Module: Mathlib.Algebra.AddTorsor.Basic
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
rw₉ rw₁₀ : y = x ↔ y = x
⊢ (pointReflection x : (a : P) → P) y = 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]

Premises used: neg_eq_iff_add_eq_zero, vsub_eq_zero_iff_eq, Function.Injective.eq_iff, nsmul_zero, eq_comm, neg_vsub_eq_vsub_rev, OfNat.ofNat, eq_vadd_iff_vsub_eq, Equiv.pointReflection_apply, two_nsmul
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂
rwa₉ rwa₁₀ rwa₁₁ 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

Premises used: neg_eq_iff_add_eq_zero, vsub_eq_zero_iff_eq, vadd_eq_vadd_iff_sub_eq_vsub, Function.Injective.eq_iff, nsmul_zero, vsub_sub_vsub_cancel_right, neg_vsub_eq_vsub_rev, OfNat.ofNat, Equiv.pointReflection_apply, two_nsmul
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_3
inst : AddCommGroup G
x : G
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)
⊢ pointReflection x = Equiv.subLeft (HSMul.hSMul (α := ℕ) 2 x)

Tactic:
ext
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_3
inst : AddCommGroup G
x 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:
simp [pointReflection, sub_add_eq_add_sub, two_nsmul]

Premises used: Equiv.pointReflection, sub_add_eq_add_sub, two_nsmul
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
Q : Type u_3
inst : AddGroup G
inst_1 : AddTorsor G P
inst_2 : VAdd G Q
inst_3 : VSub G Q
inst_4 : Nonempty Q
f : Q → P
hf : Injective f
vadd : ∀ (c : G) (x : Q), f (c +ᵥ x) = c +ᵥ f x
vsub : ∀ (x y : Q), x -ᵥ y = f x -ᵥ f y
x y : Q
⊢ f ((x -ᵥ y) +ᵥ y) = f x

Tactic:
simp only [vsub, vadd, vsub_vadd]

Premises used: vsub_vadd
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
Q : Type u_3
inst : AddGroup G
inst_1 : AddTorsor G P
inst_2 : VAdd G Q
inst_3 : VSub G Q
inst_4 : Nonempty Q
f : Q → P
hf : Injective f
vadd : ∀ (c : G) (x : Q), f (c +ᵥ x) = c +ᵥ f x
vsub : ∀ (x y : Q), x -ᵥ y = f x -ᵥ f y
c : G
x : Q
⊢ (c +ᵥ x) -ᵥ x = c

Tactic:
simp [vsub, vadd]
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
Q : Type u_3
inst : AddGroup G
inst_1 : AddTorsor G P
inst_2 : VAdd G Q
inst_3 : VSub G Q
f : P → Q
hf : Surjective f
vadd : ∀ (c : G) (x : P), f (c +ᵥ x) = c +ᵥ f x
vsub : ∀ (x y : P), x -ᵥ y = f x -ᵥ f y
⊢ ∀ (p₁ p₂ : Q), (p₁ -ᵥ p₂) +ᵥ p₂ = p₁

Tactic:
simp [hf.forall, ← vadd, ← vsub]

Premises used: Function.Surjective.forall
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
Q : Type u_3
inst : AddGroup G
inst_1 : AddTorsor G P
inst_2 : VAdd G Q
inst_3 : VSub G Q
f : P → Q
hf : Surjective f
vadd : ∀ (c : G) (x : P), f (c +ᵥ x) = c +ᵥ f x
vsub : ∀ (x y : P), x -ᵥ y = f x -ᵥ f y
⊢ ∀ (g : G) (p : Q), (g +ᵥ p) -ᵥ p = g

Tactic:
simp [hf.forall, ← vadd, ← vsub]

Premises used: Function.Surjective.forall
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
inst : AddGroup G
g₁ g₂ : G
⊢ g₁ -ᵥ g₂ = g₁ - g₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ (p₁ -ᵥ p₂) +ᵥ p₂ = p₁

Tactic:
AddTorsor.vsub_vadd' p₁ p₂

Premises used: AddTorsor.vsub_vadd'
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p : P
⊢ (g +ᵥ p) -ᵥ p = g

Tactic:
AddTorsor.vadd_vsub' g p

Premises used: AddTorsor.vadd_vsub'
-- Module: Mathlib.Algebra.AddTorsor.Defs
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₂
rw₂ rw₃ : g₂ = g₂
⊢ g₁ = g₂

Tactic:
rw [← vadd_vsub g₁ p, h, vadd_vsub]

Premises used: vadd_vsub
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g₁ g₂ : G
p : P
⊢ g₁ +ᵥ p = g₂ +ᵥ p ↔ g₁ = g₂

Tactic:
⟨vadd_right_cancel p, fun h => h ▸ rfl⟩

Premises used: Eq.rec, vadd_right_cancel, Iff.intro, rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (β := P) fun (x : G) ↦ x +ᵥ p

Tactic:
fun _ _ =>
  vadd_right_cancel p

Premises used: vadd_right_cancel, Function.Injective
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
apply : ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
⊢ (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)

Tactic:
apply vadd_right_cancel p₂

Premises used: vadd_right_cancel
-- Module: Mathlib.Algebra.AddTorsor.Defs
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₂
rw₂ rw₃ : g +ᵥ p₁ = g +ᵥ p₁
⊢ ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂

Tactic:
rw [vsub_vadd, add_vadd, vsub_vadd]

Premises used: AddSemigroupAction.add_vadd, vsub_vadd
-- Module: Mathlib.Algebra.AddTorsor.Defs
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := G) 0 0
⊢ p -ᵥ p = 0

Tactic:
rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]

Premises used: vadd_vsub_assoc, zero_add, VSub.vsub, vadd_vsub
-- Module: Mathlib.Algebra.AddTorsor.Defs
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₂
rw₂ rw₃ : p₂ = p₂
⊢ p₁ = p₂

Tactic:
rw [← vsub_vadd p₁ p₂, h, zero_vadd]

Premises used: zero_vadd, vsub_vadd
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ p₁ -ᵥ p₂ = 0 ↔ p₁ = p₂

Tactic:
Iff.intro eq_of_vsub_eq_zero fun h => h ▸ vsub_self _

Premises used: eq_of_vsub_eq_zero, Eq.rec, Iff.intro, vsub_self
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p q : P
⊢ p -ᵥ q ≠ 0 ↔ p ≠ q

Tactic:
not_congr vsub_eq_zero_iff_eq

Premises used: vsub_eq_zero_iff_eq, not_congr
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
apply : (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
⊢ p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃

Tactic:
apply vadd_right_cancel p₃

Premises used: vadd_right_cancel
-- Module: Mathlib.Algebra.AddTorsor.Defs
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₃
rw₃ rw₄ : p₁ = p₁
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃

Tactic:
rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]

Premises used: AddSemigroupAction.add_vadd, vsub_vadd
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
⊢ -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁

Tactic:
neg_eq_of_add_eq_zero_right (vadd_right_cancel p₁ ?_)

Premises used: vadd_right_cancel, neg_eq_of_add_eq_zero_right
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
refine : (p₁ -ᵥ p₂ + (p₂ -ᵥ p₁)) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
⊢ -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁

Tactic:
refine neg_eq_of_add_eq_zero_right (vadd_right_cancel p₁ ?_)

Premises used: vadd_right_cancel, neg_eq_of_add_eq_zero_right
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
rw : (p₁ -ᵥ p₁) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
rw₁ rw₂ : HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₁)) +ᵥ p₁ = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 p₁

Tactic:
rw [vsub_add_vsub_cancel, vsub_self]

Premises used: vsub_add_vsub_cancel, vsub_self
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
g : G
p q : P
rw : g + (p -ᵥ q) = g - (q -ᵥ p)
rw₁ : g + (p -ᵥ q) = g + -(q -ᵥ p)
rw₂ rw₃ : g + (p -ᵥ q) = g + (p -ᵥ q)
⊢ (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)

Tactic:
rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]

Premises used: vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
g : G
rw : p₂ -ᵥ p₁ + (p₁ -ᵥ (g +ᵥ p₂)) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₁ : p₂ -ᵥ (g +ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₂ : -((g +ᵥ p₂) -ᵥ p₂) = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₃ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂ - g)
rw₄ : -g = p₂ -ᵥ p₁ + (p₁ -ᵥ p₂) - g
rw₅ : -g = -(p₁ -ᵥ p₂) + (p₁ -ᵥ p₂) - g
rw₆ : -g = 0 - g
rw₇ rw₈ : -g = -g
⊢ p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g

Tactic:
rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]

Premises used: add_sub_assoc, vsub_add_vsub_cancel, VSub.vsub, neg_add_cancel, neg_vsub_eq_vsub_rev, vadd_vsub, add_right_inj, zero_sub
-- Module: Mathlib.Algebra.AddTorsor.Defs
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₂
rw₁ rw₂ : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
⊢ p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂

Tactic:
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]

Premises used: vsub_vadd_eq_vsub_sub, vsub_vadd
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ : P
g : G
p₂ : P
⊢ p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g

Tactic:
⟨fun h => h.symm ▸ vadd_vsub _ _, fun h => h ▸ (vsub_vadd _ _).symm⟩

Premises used: Eq.rec, Iff.intro, vsub_vadd, vadd_vsub, Eq.symm
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₁ : v₁ + (p₁ -ᵥ p₂) = v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₂ : -v₁ + (v₁ + (p₁ -ᵥ p₂)) = -v₁ + v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₃ : p₁ -ᵥ p₂ = -v₁ + v₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
rw₄ rw₅ : -v₁ + v₂ = p₁ -ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂

Tactic:
rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]

Premises used: vadd_vsub_assoc, eq_comm, add_right_inj, neg_add_cancel_left, eq_vadd_iff_vsub_eq, Neg.neg
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
rw : (v₁ +ᵥ p) -ᵥ p - v₂ = v₁ - v₂
rw₁ : v₁ + (p -ᵥ p) - v₂ = v₁ - v₂
rw₂ : v₁ + 0 - v₂ = v₁ - v₂
rw₃ rw₄ : v₁ - v₂ = v₁ - v₂
⊢ (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂

Tactic:
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_zero, vsub_self
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
p : P
⊢ Eq (α := (a : G) → P) (⇑(vaddConst p) : (a : G) → P) fun (v : G) ↦ v +ᵥ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
p : P
⊢ Eq (α := (a : P) → G) (⇑(vaddConst p).symm : (a : P) → G) fun (p' : P) ↦ p' -ᵥ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
p p' : P
⊢ (fun (x : G) ↦ -x +ᵥ p) ((fun (x : P) ↦ p -ᵥ x) p') = p'

Tactic:
simp
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
p : P
v : G
⊢ (fun (x : P) ↦ p -ᵥ x) ((fun (x : G) ↦ -x +ᵥ p) v) = v

Tactic:
simp [vsub_vadd_eq_vsub_sub]

Premises used: vsub_vadd_eq_vsub_sub
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
p : P
⊢ Eq (α := (a : P) → G) (⇑(constVSub p) : (a : P) → G) fun (x : P) ↦ p -ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
p : P
⊢ Eq (α := (a : G) → P) (⇑(constVSub p).symm : (a : G) → P) fun (v : G) ↦ -v +ᵥ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
v : G
p : P
⊢ (fun (x : P) ↦ -v +ᵥ x) ((fun (x : P) ↦ v +ᵥ x) p) = p

Tactic:
simp [vadd_vadd]

Premises used: vadd_vadd
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
v : G
p : P
⊢ (fun (x : P) ↦ v +ᵥ x) ((fun (x : P) ↦ -v +ᵥ x) p) = p

Tactic:
simp [vadd_vadd]

Premises used: vadd_vadd
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
v : G
⊢ Eq (α := (a : P) → P) (⇑(constVAdd P v) : (a : P) → P) fun (x : P) ↦ v +ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
⊢ (pointReflection x : (a : P) → P) y = (x -ᵥ y) +ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
⊢ (pointReflection x : (a : P) → P) y -ᵥ x = x -ᵥ y

Tactic:
vadd_vsub ..

Premises used: vadd_vsub
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
⊢ (pointReflection x : (a : P) → P) y -ᵥ y = HSMul.hSMul (α := ℕ) 2 (x -ᵥ y)

Tactic:
simp [pointReflection, two_nsmul, vadd_vsub_assoc]

Premises used: vadd_vsub_assoc, Equiv.pointReflection, two_nsmul
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x : P
⊢ ∀ (x_1 : P),
    Eq (α := P) ((Equiv.symm (pointReflection x) : (a : P) → P) x_1 : P) ((pointReflection x : (a : P) → P) x_1 : P)

Tactic:
simp [pointReflection]

Premises used: Equiv.pointReflection
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x : P
⊢ (pointReflection x : (a : P) → P) x = x

Tactic:
vsub_vadd _ _

Premises used: vsub_vadd
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
x y : P
rw rw₁ : Eq (α := P) ((pointReflection x : (a : P) → P) y : P) ((pointReflection x : (a : P) → P) y : P)
⊢ Eq (α := P) ((pointReflection x : (a : P) → P) y : P) ((Equiv.symm (pointReflection x) : (a : P) → P) y : P)

Tactic:
rw [pointReflection_symm]

Premises used: Equiv.pointReflection_symm
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
inhabit : ∀ (inhabited_h : Inhabited P), Subsingleton G ↔ Subsingleton P
⊢ Subsingleton G ↔ Subsingleton P

Tactic:
inhabit P
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
inhabited_h : Inhabited P
⊢ Subsingleton G ↔ Subsingleton P

Tactic:
(Equiv.vaddConst default).subsingleton_congr

Premises used: Inhabited.default, Equiv.vaddConst, Equiv.subsingleton_congr
-- Module: Mathlib.Algebra.AddTorsor.Defs
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
inhabited_h : Inhabited P
⊢ Subsingleton G ↔ Subsingleton P

Tactic:
exact (Equiv.vaddConst default).subsingleton_congr

Premises used: Inhabited.default, Equiv.vaddConst, Equiv.subsingleton_congr
-- Module: Mathlib.Algebra.AffineMonoid.Embedding
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
inst_1 : AddMonoid.FG M
inst_2 : IsAddTorsionFree M
⊢ Injective (α := M) (β := FreeAbelianGroup (Fin (dim M))) (⇑(embedding M) : (a : M) → FreeAbelianGroup (Fin (dim M)))

Tactic:
simpa [embedding] using mk_left_injective 0

Premises used: AddLocalization.mk_left_injective, AffineAddMonoid.embedding, OfNat.ofNat
-- Module: Mathlib.Algebra.AffineMonoid.Irreducible
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
S : Set M
x : M
hx : Membership.mem (γ := Set M) {p : M | Membership.mem (γ := Submonoid M) (Submonoid.closure S) p ∧ Irreducible p} x
⊢ (fun (x : M) (x_1 : Membership.mem (γ := Submonoid M) (Submonoid.closure S) x) ↦ Irreducible x → x ∈ S) 1 ⋯

Tactic:
simp