awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
he : Module.rank K ↥u.range = 1
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have he₁ : Nonempty (Basis.{0, u_3, u_2} Unit K ↥u.range)
Tactic: rw [rank_eq_one_iff_finrank_eq_one, finrank_eq_one_iff Unit] at he
Cleared hypotheses: he
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
he : Nonempty (Basis.{0, u_3, u_2} Unit K ↥u.range)
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have neg : ∀ (b : Basis.{0, u_3, u_2} Unit K ↥u.range), ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
Tactic: obtain ⟨b⟩ := he
Cleared hypotheses: he
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
have h : (↑e : V →ₗ[K] V) = (b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V)
Tactic: use (b.coord default) ∘ₗ u.rangeRestrict, b default
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
⊢ (↑e : V →ₗ[K] V) = (b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V)
have h : ∀ (x : V),
  Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V)
    (((b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V) : (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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
⊢ Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V)
    (((b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V) : (a : V) → V) x :
      V)
have h : (LinearMap.id + u : (a : V) → V) x =
  x +
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V) ((b.coord default ∘ₗ u.rangeRestrict : (a : V) → K) x : K)
      (↑((b : (a : Unit) → ↥u.range) default) : V)
Tactic: rw [← hu, LinearMap.transvection.apply, add_comm]
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
⊢ (LinearMap.id + u : (a : V) → V) x =
    x +
      HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V) ((b.coord default ∘ₗ u.rangeRestrict : (a : V) → K) x : K)
        (↑((b : (a : Unit) → ↥u.range) default) : V)
have h : (u : (a : V) → V) x =
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V)
    ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
        default :
      K)
    (↑((b : (a : Unit) → ↥u.range) default) : V)
Tactic: suffices u x = b.repr (u.rangeRestrict x) default • b default by
      simp [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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
⊢ (u : (a : V) → V) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (↑((b : (a : Unit) → ↥u.range) default) : V)
have rw : (u.rangeRestrict : (a : V) → ↥u.range) x =
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
    ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
        default :
      K)
    ((b : (a : Unit) → ↥u.range) default : ↥u.range)
Tactic: rw [← this, ← Submodule.coe_smul, Subtype.coe_inj]
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
⊢ (u.rangeRestrict : (a : V) → ↥u.range) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      ((b : (a : Unit) → ↥u.range) default : ↥u.range)
have nth_rewrite : (Finsupp.linearCombination K (⇑b : (a : Unit) → ↥u.range) : (a : Unit →₀ K) → ↥u.range)
    ((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x)) =
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
    ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
        default :
      K)
    ((b : (a : Unit) → ↥u.range) default : ↥u.range)
Tactic: nth_rewrite 1 [← b.linearCombination_repr (u.rangeRestrict 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
⊢ (Finsupp.linearCombination K (⇑b : (a : Unit) → ↥u.range) : (a : Unit →₀ K) → ↥u.range)
      ((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x)) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      ((b : (a : Unit) → ↥u.range) default : ↥u.range)
have h₀ : ∀ (b_1 : Unit),
  Ne.{u_3 + 1} (α := K)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          b_1 :
        K)
      (0 : K) →
    b_1 ≠ default →
      HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
          ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) :
                (a : Unit) → K)
              b_1 :
            K)
          ((b : (a : Unit) → ↥u.range) b_1 : ↥u.range) =
        0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum_eq_single default]
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
h₀ :
  ∀ (b_1 : Unit),
    Ne.{u_3 + 1} (α := K)
        ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) :
              (a : Unit) → K)
            b_1 :
          K)
        (0 : K) →
      b_1 ≠ default →
        HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
            ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) :
                  (a : Unit) → K)
                b_1 :
              K)
            ((b : (a : Unit) → ↥u.range) b_1 : ↥u.range) =
          0
⊢ (Finsupp.linearCombination K (⇑b : (a : Unit) → ↥u.range) : (a : Unit →₀ K) → ↥u.range)
      ((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x)) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      ((b : (a : Unit) → ↥u.range) default : ↥u.range)
have h₁ : Eq.{u_3 + 1} (α := K)
    ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
        default :
      K)
    (0 : K) →
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range) 0 ((b : (a : Unit) → ↥u.range) default : ↥u.range) = 0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum_eq_single default]
-- 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
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
⊢ (u : (a : V) → V) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (↑((b : (a : Unit) → ↥u.range) default) : V)
have h : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
Tactic: suffices u.rangeRestrict x = u x by
      rw [← this, ← Submodule.coe_smul, Subtype.coe_inj]
      nth_rewrite 1 [← b.linearCombination_repr (u.rangeRestrict x)]
      rw [Finsupp.linearCombination_apply, Finsupp.sum_eq_single default] <;> simp
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have rw : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
  finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
Tactic: rw [mem_dilatransvections_iff_rank, finrank, ← one_toNat,
    toNat_le_iff_le_of_lt_aleph0 (rank_lt_aleph0 K _) one_lt_aleph0]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
rw :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have rw₁ : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
  LE.le (α := ℕ) ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range) : ℕ)
    (1 : ℕ)
Tactic: rw [mem_dilatransvections_iff_rank, finrank, ← one_toNat,
    toNat_le_iff_le_of_lt_aleph0 (rank_lt_aleph0 K _) one_lt_aleph0]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
rw :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
rw₁ :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    LE.le (α := ℕ) ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range) : ℕ)
      (1 : ℕ)
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have rw₂ : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
  LE.le (α := ℕ) ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range) : ℕ)
    ((toNat : (a : Cardinal.{u_2}) → ℕ) 1 : ℕ)
Tactic: rw [mem_dilatransvections_iff_rank, finrank, ← one_toNat,
    toNat_le_iff_le_of_lt_aleph0 (rank_lt_aleph0 K _) one_lt_aleph0]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
rw :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
rw₁ :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    LE.le (α := ℕ) ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range) : ℕ)
      (1 : ℕ)
rw₂ :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    LE.le (α := ℕ) ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range) : ℕ)
      ((toNat : (a : Cardinal.{u_2}) → ℕ) 1 : ℕ)
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
have rw₃ : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔ Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
Tactic: rw [mem_dilatransvections_iff_rank, finrank, ← one_toNat,
    toNat_le_iff_le_of_lt_aleph0 (rank_lt_aleph0 K _) one_lt_aleph0]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
have rw : finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
Tactic: rw [mem_dilatransvections_iff_finrank, ← (quotKerEquivRange _).finrank_eq,
    ← fixedSubmodule_eq_ker]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
rw :
  finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
have rw₁ : finrank.{u_3, u_2} K (V ⧸ ((↑e : V →ₗ[K] V) - LinearMap.id).ker) ≤ 1 ↔
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
Tactic: rw [mem_dilatransvections_iff_finrank, ← (quotKerEquivRange _).finrank_eq,
    ← fixedSubmodule_eq_ker]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
rw :
  finrank.{u_3, u_2} K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
rw₁ :
  finrank.{u_3, u_2} K (V ⧸ ((↑e : V →ₗ[K] V) - LinearMap.id).ker) ≤ 1 ↔
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
have rw₂ : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1 ↔
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
Tactic: rw [mem_dilatransvections_iff_finrank, ← (quotKerEquivRange _).finrank_eq,
    ← fixedSubmodule_eq_ker]
-- 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)) (dilatransvections K V) e ↔
    Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
have rw : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔ Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
Tactic: rw [mem_dilatransvections_iff_rank, ← (quotKerEquivRange _).rank_eq, ← fixedSubmodule_eq_ker]
-- 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
rw :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔ Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
have rw₁ : Module.rank K (V ⧸ ((↑e : V →ₗ[K] V) - LinearMap.id).ker) ≤ 1 ↔ Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
Tactic: rw [mem_dilatransvections_iff_rank, ← (quotKerEquivRange _).rank_eq, ← fixedSubmodule_eq_ker]
-- 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
rw :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔ Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
rw₁ :
  Module.rank K (V ⧸ ((↑e : V →ₗ[K] V) - LinearMap.id).ker) ≤ 1 ↔
    Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
have rw₂ : Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1 ↔ Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
Tactic: rw [mem_dilatransvections_iff_rank, ← (quotKerEquivRange _).rank_eq, ← fixedSubmodule_eq_ker]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e ↔
    Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
have refine_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e →
  ∀ (f : Dual K V) (v : V) (hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)) (he : e = transvection hfv),
    Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
Tactic: refine ⟨fun ⟨f, v, hfv, he⟩ ↦ ?_, fun ⟨he, he'⟩ ↦ ?_⟩
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
refine_1 :
  Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e →
    ∀ (f : Dual K V) (v : V) (hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K))
      (he : e = transvection hfv), Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e ↔
    Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
have refine_2 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1 →
  ∀ (he : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e) (he' : e.fixedReduce = 1),
    Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
Tactic: refine ⟨fun ⟨f, v, hfv, he⟩ ↦ ?_, fun ⟨he, he'⟩ ↦ ?_⟩
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
he : e = transvection hfv
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
have refine_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
he : e = transvection hfv
refine_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
have refine_1₁ : e.fixedReduce = 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
he : e = transvection hfv
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
have refine_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) (transvection hfv)
Tactic: rw [he]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
he : e = transvection hfv
⊢ e.fixedReduce = 1
have refine_1 : ∀ (v_1 : V),
  HSub.hSub (α := V) ((transvection hfv : (a : V) → V) v_1 : V) v_1 ∈ (↑(transvection hfv) : V →ₗ[K] V).fixedSubmodule
Tactic: rw [one_eq_refl, fixedReduce_eq_one, he]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
he : e = transvection hfv
x : V
⊢ HSub.hSub (α := V) ((transvection hfv : (a : V) → V) x : V) x ∈ (↑(transvection hfv) : V →ₗ[K] V).fixedSubmodule
have refine_1 : HSub.hSub (α := V) ((transvection hfv : (a : V) → V) x : V) x ∈ ker f
Tactic: apply ker_le_fixedSubmodule_transvection hfv
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
he : e = transvection hfv
x : V
⊢ HSub.hSub (α := V) ((transvection hfv : (a : V) → V) x : V) x ∈ ker f
have refine_1 : x + HSMul.hSMul.{u_3, u_2, u_2} (α := K) ((f : (a : V) → K) x : K) v - x ∈ ker f
Tactic: rw [transvection.apply]