awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (↑e.symm : V →ₗ[R] V) = LinearMap.transvection f (-(e.symm : (a : V) → V) v)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have 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)
Tactic: suffices x = e x - f x • v by
    simpa [LinearMap.transvection.apply, ← sub_eq_add_neg, symm_apply_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [eq_comm, sub_eq_iff_eq_add, ← coe_coe, he, LinearMap.transvection.apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have h₁ : (e : (a : V) → V) x = x + 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [eq_comm, sub_eq_iff_eq_add, ← coe_coe, he, LinearMap.transvection.apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [eq_comm, sub_eq_iff_eq_add, ← coe_coe, he, LinearMap.transvection.apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [eq_comm, sub_eq_iff_eq_add, ← coe_coe, he, LinearMap.transvection.apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (LinearMap.transvection f (-h.unit⁻¹ • v) : (a : V) → V) ((LinearMap.transvection f v : (a : V) → V) x : V) = x
have 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
Tactic: nth_rewrite 3 [← one_smul R v]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (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
have 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
Tactic: rw [← LinearMap.comp_apply, Units.smul_def, LinearMap.transvection.comp_smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (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
have 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
Tactic: simp only [Units.val_neg, one_mul, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (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
have suffices : -(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R) = 0
Tactic: suffices (-h.unit⁻¹) + 1 - f v * (h.unit⁻¹) = 0 by simp [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ -(↑h.unit⁻¹ : R) + 1 - HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R) = 0
have rw : 1 = (↑h.unit⁻¹ : R) + HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R)
Tactic: rw [sub_eq_zero, neg_add_eq_iff_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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 = (↑h.unit⁻¹ : R) + HMul.hMul (α := R) ((f : (a : V) → R) v : R) (↑h.unit⁻¹ : R)
have nth_rewrite : 1 = HAdd.hAdd (α := R) (β := R) ((↑1 : R) : R) ((f : (a : V) → R) v : R) * (↑h.unit⁻¹ : R)
Tactic: nth_rewrite 1 [← one_mul (h.unit⁻¹), Units.val_mul, ← add_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (LinearMap.transvection f v : (a : V) → V) ((LinearMap.transvection f (-h.unit⁻¹ • v) : (a : V) → V) x : V) = x
have 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
Tactic: simp only [LinearMap.transvection.apply, add_assoc, add_eq_left,
      Units.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [smul_smul, ← add_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 v = 0
Tactic: rw [this, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have rw₁ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [this, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have 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
Tactic: suffices (f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v)) = 0 by rw [this, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [LinearMap.map_add, LinearMap.map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have 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
Tactic: nth_rewrite 2 [← mul_one (f x)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [mul_assoc, ← mul_add, ← mul_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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
have rw : HMul.hMul (α := R) ((f : (a : V) → R) x : R)
    (1 + ((↑(-h.unit⁻¹) : R) + HMul.hMul (β := R) (↑(-h.unit⁻¹) : R) ((f : (a : V) → R) v : R))) =
  0
Tactic: rw [← add_assoc, add_comm _ 1, add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ HMul.hMul (α := R) ((f : (a : V) → R) x : R)
      (1 + ((↑(-h.unit⁻¹) : R) + HMul.hMul (β := R) (↑(-h.unit⁻¹) : R) ((f : (a : V) → R) v : R))) =
    0
have nth_rewrite : HMul.hMul (α := R) ((f : (a : V) → R) x : R)
    (1 + (↑(-h.unit⁻¹) : R) * HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)) =
  0
Tactic: nth_rewrite 1 [← mul_one (-h.unit⁻¹), Units.val_mul, Units.val_one, ← mul_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V))
      {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e ↔
    Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have mp : Membership.mem (γ := Set (V ≃ₗ[K] V))
    {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e →
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
mp :
  Membership.mem (γ := Set (V ≃ₗ[K] V))
      {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e →
    Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V))
      {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e ↔
    Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have mpr : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 →
  Membership.mem (γ := Set (V ≃ₗ[K] V))
    {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : (↑e : V →ₗ[K] V) = LinearMap.transvection f v
⊢ Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have mp : Module.rank K ↥(K ∙ v) ≤ 1
Tactic: apply le_trans (rank_mono (t := K ∙ v) ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : (↑e : V →ₗ[K] V) = LinearMap.transvection f v
mp : Module.rank K ↥(K ∙ v) ≤ 1
⊢ Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have apply : ((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ K ∙ v
Tactic: apply le_trans (rank_mono (t := K ∙ v) ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
he : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
he₁ :
  let u := (↑e : V →ₗ[K] V) - LinearMap.id;
  Module.rank K ↥u.range ≤ 1
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have hu : let u := (↑e : V →ₗ[K] V) - LinearMap.id;
u = (↑e : V →ₗ[K] V) - LinearMap.id
Tactic: set u := (e : V →ₗ[K] V) - LinearMap.id with hu
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u = (↑e : V →ₗ[K] V) - LinearMap.id
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have hu₁ : u + LinearMap.id = (↑e : V →ₗ[K] V)
Tactic: rw [eq_sub_iff_add_eq] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have pos : ∀ (hr : Module.rank K ↥u.range = 0), ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
Tactic: by_cases hr : Module.rank K (range u) = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
pos : ∀ (hr : Module.rank K ↥u.range = 0), ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have neg : ∀ (hr : ¬Module.rank K ↥u.range = 0), ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
Tactic: by_cases hr : Module.rank K (range u) = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have h : (↑e : V →ₗ[K] V) = LinearMap.transvection 0 0
Tactic: use 0, 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
⊢ (↑e : V →ₗ[K] V) = LinearMap.transvection 0 0
have h : ∀ (x : V), Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V) ((LinearMap.transvection 0 0 : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
x : V
⊢ Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V) ((LinearMap.transvection 0 0 : (a : V) → V) x : V)
have h : Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)
Tactic: suffices u x = 0 by simp [← hu, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
x : V
⊢ Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)
have h : ∀ (hr : Subsingleton.{u_2 + 1} ↥u.range) (x : V), Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)
Tactic: rw [rank_zero_iff] at hr
Cleared hypotheses: hr, x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : ¬Module.rank K ↥u.range = 0
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have hr₁ : 1 ≤ Module.rank K ↥u.range
Tactic: rw [← ne_eq, ← Cardinal.one_le_iff_ne_zero] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have he₁ : Module.rank K ↥u.range = 1
Tactic: replace he : Module.rank K (range u) = 1 := le_antisymm he hr
Cleared hypotheses: he