awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h1 : finrank R V ≤ 1
⊢ transvection f v = id
have 0 : ∀ (h : finrank R V = 0) (h1 : LE.le (α := ℕ) 0 1), transvection f v = id
Tactic: interval_cases h : finrank R V
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h1 : finrank R V ≤ 1
0 : ∀ (h : finrank R V = 0) (h1 : LE.le (α := ℕ) 0 1), transvection f v = id
⊢ transvection f v = id
have 1 : ∀ (h : finrank R V = 1) (h1 : LE.le (α := ℕ) 1 1), transvection f v = id
Tactic: interval_cases h : finrank R V
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 0
h1 : LE.le (α := ℕ) 0 1
⊢ transvection f v = id
have this : Subsingleton V
Tactic: have : Subsingleton V := (finrank_eq_zero_iff_of_free R V).mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
⊢ transvection f v = id
have 1 : ∀ (x : V), Eq (α := V) ((transvection f v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
⊢ Eq (α := V) ((transvection f v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)
have 1 : HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
Tactic: suffices f x • v = 0 by
      simp [apply, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
have hfv₁ : HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
    ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
  0
Tactic: rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv
Cleared hypotheses: hfv, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv :
  HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
    0
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
have rw : HSMul.hSMul.{u_3, u_4, u_4} (α := R)
    ((f : (a : V) → R)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
          ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i :
            R)
          ((b : (a : Fin (finrank R V)) → V) i : V)) :
      R)
    v =
  0
Tactic: rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv :
  HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
    0
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
rw :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R)
      ((f : (a : V) → R)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                i :
              R)
            ((b : (a : Fin (finrank R V)) → V) i : V)) :
        R)
      v =
    0
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
have rw₁ : HSMul.hSMul.{u_3, u_4, u_4} (α := R)
    ((f : (a : V) → R)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
          ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i :
            R)
          ((b : (a : Fin (finrank R V)) → V) i : V)) :
      R)
    (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V)) =
  0
Tactic: rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv :
  HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
    0
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
rw :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R)
      ((f : (a : V) → R)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                i :
              R)
            ((b : (a : Fin (finrank R V)) → V) i : V)) :
        R)
      v =
    0
rw₁ :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R)
      ((f : (a : V) → R)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                i :
              R)
            ((b : (a : Fin (finrank R V)) → V) i : V)) :
        R)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)) =
    0
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
have rw₂ : HSMul.hSMul (α := R) (β := R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R) •
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V) =
  0
Tactic: rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv :
  HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
    0
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
rw :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R)
      ((f : (a : V) → R)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                i :
              R)
            ((b : (a : Fin (finrank R V)) → V) i : V)) :
        R)
      v =
    0
rw₁ :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R)
      ((f : (a : V) → R)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                i :
              R)
            ((b : (a : Fin (finrank R V)) → V) i : V)) :
        R)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)) =
    0
rw₂ :
  HSMul.hSMul (α := R) (β := R)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R) •
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V) =
    0
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
have rw₃ : HMul.hMul (α := R) (β := R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R) •
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V) =
  0
Tactic: rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
have 1 : ∀ (x : V),
  x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V)
Tactic: suffices ∀ x, x = b.repr x i • (b i) by
      rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv
      rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x_1 : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
⊢ x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V)
have this : x =
  ∑ i : Fin (finrank R V),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V)
Tactic: have : x = ∑ i, b.repr x i • b i := (b.sum_equivFun x).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x_1 : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
this :
  x =
    ∑ i : Fin (finrank R V),
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
⊢ x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V)
have 1 : ∀
  (this :
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)),
  x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V)
Tactic: rwa [Finset.sum_eq_single_of_mem i (Finset.mem_univ i) (by grind)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
f : Dual R V
v : V
e : V ≃ₗ[R] W
⊢ (↑e : V →ₗ[R] W) ∘ₗ transvection f v ∘ₗ (↑e.symm : W →ₗ[R] V) =
    (f ∘ₗ (↑e.symm : W →ₗ[R] V)).transvection ((e : (a : V) → W) v)
have h : ∀ (x : W),
  Eq (α := W) (((↑e : V →ₗ[R] W) ∘ₗ transvection f v ∘ₗ (↑e.symm : W →ₗ[R] V) : (a : W) → W) x : W)
    (((f ∘ₗ (↑e.symm : W →ₗ[R] V)).transvection ((e : (a : V) → W) v) : (a : W) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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 : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
⊢ (LinearMap.transvection f v : (a : V) → V) ((LinearMap.transvection f (-v) : (a : V) → V) x : V) = x
have h' : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)
Tactic: have h' : f (-v) = 0 := by simp [h]
-- 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 w : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) w : R) (0 : R)
hvw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (v + w) : R) (0 : R)
⊢ transvection hw ≪≫ₗ transvection hv = transvection hvw
have h : ∀ (x : V),
  Eq (α := V) ((transvection hw ≪≫ₗ transvection hv : (a : V) → V) x : V) ((transvection hvw : (a : V) → V) x : V)
Tactic: ext
-- 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 g : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) v : R) (0 : R)
hfg : Eq.{u_1 + 1} (α := R) ((f + g : (a : V) → R) v : R) (0 : R)
⊢ transvection hg ≪≫ₗ transvection hf = transvection hfg
have h : ∀ (x : V),
  Eq (α := V) ((transvection hg ≪≫ₗ transvection hf : (a : V) → V) x : V) ((transvection hfg : (a : V) → V) x : V)
Tactic: ext
-- 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
v : V
hv : Eq.{u_1 + 1} (α := R) ((0 : (a : V) → R) v : R) (0 : R)
⊢ transvection hv = refl R V
have h : ∀ (x : V), Eq (α := V) ((transvection hv : (a : V) → V) x : V) ((refl R V : (a : V) → V) x : V)
Tactic: ext
-- 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
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) 0 : R) (0 : R)
⊢ transvection hf = refl R V
have h : ∀ (x : V), Eq (α := V) ((transvection hf : (a : V) → V) x : V) ((refl R V : (a : V) → V) x : V)
Tactic: ext
-- 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
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hv' : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)
⊢ (transvection hv).symm = transvection hv'
have h : ∀ (x : V), Eq (α := V) (((transvection hv).symm : (a : V) → V) x : V) ((transvection hv' : (a : V) → V) x : V)
Tactic: ext
-- 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
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hf' : Eq.{u_1 + 1} (α := R) ((-f : (a : V) → R) v : R) (0 : R)
⊢ (transvection hf).symm = transvection hf'
have h : ∀ (x : V), Eq (α := V) (((transvection hf).symm : (a : V) → V) x : V) ((transvection hf' : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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)
x : V
hx : x ∈ ker f
⊢ x ∈ (↑(transvection hfv) : V →ₗ[R] V).fixedSubmodule
have hx₁ : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
Tactic: rw [mem_ker] at hx
Cleared hypotheses: hx
-- 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 : 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
have refine : ∀ (h : 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⟩
-- 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 : 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
have rw : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm.symm
Tactic: rw [← symm_symm e]
-- 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 : V ≃ₗ[R] V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e.symm ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e
have 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
Tactic: suffices ∀ e ∈ transvections R V, e.symm ∈ transvections R V by
    refine ⟨fun h ↦ ?_, this e⟩
    rw [← symm_symm e]
    exact this _ h
-- 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 : 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 hv).symm
have rw : Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) (transvection (v := -v) sorry)
Tactic: rw [transvection.symm_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 : V ≃ₗ[R] V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e.symm ↔
    Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e
have 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
Tactic: suffices ∀ e ∈ dilatransvections R V, e.symm ∈ dilatransvections R V from
    ⟨by simpa using this e.symm, this e⟩
-- 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
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e.symm
have h : (↑e.symm : V →ₗ[R] V) = LinearMap.transvection f (-(e.symm : (a : V) → V) v)
Tactic: use f, - e.symm v