awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) (transvection hfv)

Tactic:
⟨f, v, hfv, rfl⟩

Premises used: Set.Mem, setOf, LinearEquiv.transvections, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Eq.{u_1 + 1} (α := R) ((0 : (a : V) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Eq (α := V ≃ₗ[R] V) (refl R V) (transvection (f := 0) (v := 0) ⋯)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) 1

Tactic:
refl_mem_transvections

Premises used: Set.Mem, LinearEquiv.refl_mem_transvections
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
this :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e

Tactic:
⟨fun h ↦ ?_, this e⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
this :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
refine :
  ∀ (h : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e

Tactic:
refine ⟨fun h ↦ ?_, this e⟩
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
this :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
h : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
rw : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm.symm
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e

Tactic:
rw [← symm_symm e]

Premises used: LinearEquiv.symm_symm
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
this :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
h : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm.symm

Tactic:
this _ h
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
this :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
h : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm.symm

Tactic:
exact this _ h
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
suffices :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e

Tactic:
suffices ∀ e ∈ transvections R V, e.symm ∈ transvections R V by
    refine ⟨fun h ↦ ?_, this e⟩
    rw [← symm_symm e]
    exact this _ h
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
f : Dual R V
v : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
rw : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) (transvection (v := -v) ⋯)
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) (transvection hv).symm

Tactic:
rw [transvection.symm_eq]

Premises used: LinearEquiv.transvection.symm_eq
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
f : Dual R V
v : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) (transvection (v := -v) ⋯)

Tactic:
apply mem_transvections

Premises used: LinearEquiv.mem_transvections
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e⁻¹ ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e

Tactic:
symm_mem_transvections_iff

Premises used: LinearEquiv.symm_mem_transvections_iff, Set.Mem
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Monotone.{0, u_2} (β := Set (V ≃ₗ[R] V)) fun (n : ℕ) ↦ HPow.hPow (α := Set (V ≃ₗ[R] V)) (transvections R V) n

Tactic:
Set.pow_right_monotone one_mem_transvections

Premises used: LinearEquiv.one_mem_transvections, Set.pow_right_monotone
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ (↑(transvection hfv) : V →ₗ[R] V) = LinearMap.transvection f v

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) (transvection hfv)

Tactic:
exact ⟨f, v, by simp⟩
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) (refl R V)

Tactic:
transvections_subset_dilatransvections one_mem_transvections

Premises used: LinearEquiv.one_mem_transvections, LinearEquiv.transvections_subset_dilatransvections
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) (transvection hfv)

Tactic:
transvections_subset_dilatransvections transvection_mem_transvections

Premises used: LinearEquiv.transvections_subset_dilatransvections, LinearEquiv.transvection_mem_transvections
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) 1

Tactic:
refl_mem_dilatransvections

Premises used: Set.Mem, LinearEquiv.refl_mem_dilatransvections
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
this :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e.symm
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e.symm →
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e

Tactic:
simpa using this e.symm

Premises used: LinearEquiv.symm
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
suffices :
  ∀ (e : V ≃ₗ[R] V),
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e →
      Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e.symm
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e.symm ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e

Tactic:
suffices ∀ e ∈ dilatransvections R V, e.symm ∈ dilatransvections R V from
    ⟨by simpa using this e.symm, this e⟩
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e_1 e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
h : (↑e.symm : V →ₗ[R] V) = LinearMap.transvection f (-(e.symm : (a : V) → V) v)
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e.symm

Tactic:
use f, - e.symm v

Premises used: LinearEquiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e_1 e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
h :
  ∀ (x : V),
    Eq (α := V) (((↑e.symm : V →ₗ[R] V) : (a : V) → V) x : V)
      ((LinearMap.transvection f (-(e.symm : (a : V) → V) v) : (a : V) → V) x : V)
⊢ (↑e.symm : V →ₗ[R] V) = LinearMap.transvection f (-(e.symm : (a : V) → V) v)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e_1 e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
x : V
this :
  x = HSub.hSub (α := V) ((e : (a : V) → V) x : V) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v)
⊢ Eq (α := V) (((↑e.symm : V →ₗ[R] V) : (a : V) → V) x : V)
    ((LinearMap.transvection f (-(e.symm : (a : V) → V) v) : (a : V) → V) x : V)

Tactic:
simpa [LinearMap.transvection.apply, ← sub_eq_add_neg, symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq, sub_eq_add_neg, LinearMap.transvection.apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e_1 e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
x : V
h : x = HSub.hSub (α := V) ((e : (a : V) → V) x : V) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v)
⊢ Eq (α := V) (((↑e.symm : V →ₗ[R] V) : (a : V) → V) x : V)
    ((LinearMap.transvection f (-(e.symm : (a : V) → V) v) : (a : V) → V) x : V)

Tactic:
suffices x = e x - f x • v by
    simpa [LinearMap.transvection.apply, ← sub_eq_add_neg, symm_apply_eq]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e_1 e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
x : V
h : HSub.hSub (α := V) ((e : (a : V) → V) x : V) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v) = x
h₁ : (e : (a : V) → V) x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v
h₂ : ((↑e : V →ₗ[R] V) : (a : V) → V) x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v
h₃ : (LinearMap.transvection f v : (a : V) → V) x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v
h₄ h₅ :
  x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v =
    x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v
⊢ x = HSub.hSub (α := V) ((e : (a : V) → V) x : V) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v)

Tactic:
rw [eq_comm, sub_eq_iff_eq_add, ← coe_coe, he, LinearMap.transvection.apply]

Premises used: LinearMap.transvection.apply, eq_comm, sub_eq_iff_eq_add, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e⁻¹ ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e

Tactic:
symm_mem_dilatransvections_iff

Premises used: LinearEquiv.symm_mem_dilatransvections_iff, Set.Mem
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x y : V
⊢ (LinearMap.transvection f v : (a : V) → V) (x + y) =
    HAdd.hAdd (α := V) (β := V) ((LinearMap.transvection f v : (a : V) → V) x : V)
      ((LinearMap.transvection f v : (a : V) → V) y : V)

Tactic:
simp [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
r : R
x : V
⊢ (LinearMap.transvection f v : (a : V) → V) (r • x) =
    HSMul.hSMul (α := R) (β := V) ((RingHom.id R : (a : R) → R) r : R)
      ((LinearMap.transvection f v : (a : V) → V) x : V)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
nth_rewrite :
  (LinearMap.transvection f (-h.unit⁻¹ • v) : (a : V) → V)
      ((LinearMap.transvection f (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 v) : (a : V) → V) x : V) =
    x
⊢ (LinearMap.transvection f (-h.unit⁻¹ • v) : (a : V) → V) ((LinearMap.transvection f v : (a : V) → V) x : V) = x

Tactic:
nth_rewrite 3 [← one_smul R v]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
rw :
  (LinearMap.transvection f
          (((↑(-h.unit⁻¹) : R) + 1 +
              HMul.hMul (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R) * (↑(-h.unit⁻¹) : R)) •
            v) :
        (a : V) → V)
      x =
    x
⊢ (LinearMap.transvection f (-h.unit⁻¹ • v) : (a : V) → V)
      ((LinearMap.transvection f (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 v) : (a : V) → V) x : V) =
    x

Tactic:
rw [← LinearMap.comp_apply, Units.smul_def, LinearMap.transvection.comp_smul_smul]

Premises used: LinearMap.comp_apply, LinearMap.transvection.comp_smul_smul, Units.smul_def
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
simp :
  (LinearMap.transvection f
          ((-(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R)) • v) :
        (a : V) → V)
      x =
    x
⊢ (LinearMap.transvection f
          (((↑(-h.unit⁻¹) : R) + 1 +
              HMul.hMul (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R) * (↑(-h.unit⁻¹) : R)) •
            v) :
        (a : V) → V)
      x =
    x

Tactic:
simp only [Units.val_neg, one_mul, mul_neg, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, Units.val_neg, one_mul, mul_neg
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
this : -(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R) = 0
⊢ (LinearMap.transvection f
          ((-(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R)) • v) :
        (a : V) → V)
      x =
    x

Tactic:
simp [this]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
suffices : -(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R) = 0
⊢ (LinearMap.transvection f
          ((-(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R)) • v) :
        (a : V) → V)
      x =
    x

Tactic:
suffices (-h.unit⁻¹) + 1 - f v * (h.unit⁻¹) = 0 by simp [this]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
rw : 1 = (↑h.unit⁻¹ : R) + HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R)
⊢ -(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R) = 0

Tactic:
rw [sub_eq_zero, neg_add_eq_iff_eq_add]

Premises used: sub_eq_zero, neg_add_eq_iff_eq_add
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
nth_rewrite : 1 = HAdd.hAdd (α := R) (β := R) ((↑1 : R) : R) ((f : (a : V) → R) v : R) * (↑h.unit⁻¹ : R)
⊢ 1 = (↑h.unit⁻¹ : R) + HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R)

Tactic:
nth_rewrite 1 [← one_mul (h.unit⁻¹), Units.val_mul, ← add_mul]

Premises used: add_mul, Inv.inv, IsUnit.unit, Units.val_mul, one_mul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
⊢ 1 = HAdd.hAdd (α := R) (β := R) ((↑1 : R) : R) ((f : (a : V) → R) v : R) * (↑h.unit⁻¹ : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
simp :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) ((↑(-h.unit⁻¹) : R) • v) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f : (a : V) → R)
            (x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) ((↑(-h.unit⁻¹) : R) • v)) :
          R)
        v =
    0
⊢ (LinearMap.transvection f v : (a : V) → V) ((LinearMap.transvection f (-h.unit⁻¹ • v) : (a : V) → V) x : V) = x

Tactic:
simp only [LinearMap.transvection.apply, add_assoc, add_eq_left,
      Units.smul_def]

Premises used: add_assoc, LinearMap.transvection.apply, add_eq_left, Units.smul_def
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
rw :
  HAdd.hAdd (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
        ((f : (a : V) → R) (x + HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) • v) : R) •
      v =
    0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) ((↑(-h.unit⁻¹) : R) • v) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f : (a : V) → R)
            (x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) ((↑(-h.unit⁻¹) : R) • v)) :
          R)
        v =
    0

Tactic:
rw [smul_smul, ← add_smul]

Premises used: smul_smul, add_smul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
this :
  HAdd.hAdd (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
      ((f : (a : V) → R) (x + HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) • v) : R) =
    0
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := V) 0 0
⊢ HAdd.hAdd (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
        ((f : (a : V) → R) (x + HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) • v) : R) •
      v =
    0

Tactic:
rw [this, zero_smul]

Premises used: zero_smul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
suffices :
  HAdd.hAdd (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
      ((f : (a : V) → R) (x + HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) • v) : R) =
    0
⊢ HAdd.hAdd (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
        ((f : (a : V) → R) (x + HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) • v) : R) •
      v =
    0

Tactic:
suffices (f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v)) = 0 by rw [this, zero_smul]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
rw :
  HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) +
      HAdd.hAdd (α := R) ((f : (a : V) → R) x : R)
        (HMul.hMul (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
          ((f : (a : V) → R) v : R)) =
    0
⊢ HAdd.hAdd (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
      ((f : (a : V) → R) (x + HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) • v) : R) =
    0

Tactic:
rw [LinearMap.map_add, LinearMap.map_smul, smul_eq_mul]

Premises used: LinearMap.map_add, LinearMap.map_smul, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
nth_rewrite :
  HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) +
      (HMul.hMul (α := R) (β := R) ((f : (a : V) → R) x : R) (1 : R) +
        HMul.hMul (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
          ((f : (a : V) → R) v : R)) =
    0
⊢ HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) +
      HAdd.hAdd (α := R) ((f : (a : V) → R) x : R)
        (HMul.hMul (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
          ((f : (a : V) → R) v : R)) =
    0

Tactic:
nth_rewrite 2 [← mul_one (f x)]

Premises used: mul_one, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
rw :
  HMul.hMul (α := R) ((f : (a : V) → R) x : R)
      ((↑(-h.unit⁻¹) : R) + (1 + HMul.hMul (β := R) (↑(-h.unit⁻¹) : R) ((f : (a : V) → R) v : R))) =
    0
⊢ HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R) +
      (HMul.hMul (α := R) (β := R) ((f : (a : V) → R) x : R) (1 : R) +
        HMul.hMul (β := R) (HMul.hMul (α := R) ((f : (a : V) → R) x : R) (↑(-h.unit⁻¹) : R))
          ((f : (a : V) → R) v : R)) =
    0

Tactic:
rw [mul_assoc, ← mul_add, ← mul_add]

Premises used: mul_assoc, mul_add