awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
hefixed_ne_top : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 0
⊢ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V
have h : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule =
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
Tactic: rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
hefixed_ne_top : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 0
h :
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule =
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
⊢ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V
have rw : ℕ
Tactic: rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
hefixed_ne_top : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 0
h :
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule =
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
rw : ℕ
⊢ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V
have h₁ : finrank K V = finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
Tactic: rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
hefixed_ne_top : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 0
h :
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule =
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
rw : ℕ
h₁ : finrank K V = finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
⊢ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V
have h₂ : finrank K V = 0 + finrank K V
Tactic: rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
hefixed_ne_top : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 0
h :
  finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule =
    finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
rw : ℕ
h₁ : finrank K V = finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) + finrank K V
h₂ : finrank K V = 0 + finrank K V
⊢ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V
have h₃ : finrank K V = finrank K V
Tactic: rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_add]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
Tactic: have eq_top : e.fixedSubmodule ⊔ Submodule.span K {w} = ⊤ := by
      rw [Submodule.sup_span_singleton_eq_top_iff hw]
      apply le_antisymm he
      apply Nat.one_le_of_lt
      rw [← Nat.ne_zero_iff_zero_lt]
      contrapose hefixed_ne_top
      apply eq_top_of_finrank_eq
      rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have h : e = transvection hfv
Tactic: use f, v, 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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
⊢ e = transvection hfv
have h : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w ≤ ((↑e : V →ₗ[K] V) - (↑(transvection hfv) : V →ₗ[K] V)).ker
Tactic: rw [← LinearEquiv.toLinearMap_inj,
        ← sub_eq_zero, ← LinearMap.ker_eq_top, eq_top_iff, ← eq_top]
-- 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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w ≤ ((↑e : V →ₗ[K] V) - (↑(transvection hfv) : V →ₗ[K] V)).ker
have h : (↑e : V →ₗ[K] V).fixedSubmodule ≤ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker ∧
  HSub.hSub (α := V) (β := V) ((e : (a : V) → V) w : V) ((LinearMap.transvection f v : (a : V) → V) w : V) = 0
Tactic: simp only [LinearEquiv.transvection.coe_toLinearMap,
        sup_le_iff, Submodule.span_singleton_le_iff_mem, LinearMap.mem_ker, LinearMap.sub_apply,
        LinearEquiv.coe_coe]
-- 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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ≤ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker ∧
    HSub.hSub (α := V) (β := V) ((e : (a : V) → V) w : V) ((LinearMap.transvection f v : (a : V) → V) w : V) = 0
have h : (↑e : V →ₗ[K] V).fixedSubmodule ≤ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker
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_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
h : (↑e : V →ₗ[K] V).fixedSubmodule ≤ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ≤ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker ∧
    HSub.hSub (α := V) (β := V) ((e : (a : V) → V) w : V) ((LinearMap.transvection f v : (a : V) → V) w : V) = 0
have h₁ : HSub.hSub (α := V) (β := V) ((e : (a : V) → V) w : V) ((LinearMap.transvection f v : (a : V) → V) w : V) = 0
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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
x : V
hx : x ∈ (↑e : V →ₗ[K] V).fixedSubmodule
⊢ x ∈ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker
have h : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
Tactic: suffices f x = 0 by
          simpa [this, LinearMap.transvection.apply, sub_eq_zero] using hx
-- 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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
x : V
hx : x ∈ (↑e : V →ₗ[K] V).fixedSubmodule
⊢ Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
have h : ∀ (hx : x ∈ ker f), Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
Tactic: rwa [hf', LinearMap.mem_ker] at hx
Cleared hypotheses: hx
-- 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_1 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
x : V
hx : x ∈ (↑e : V →ₗ[K] V).fixedSubmodule
h : ∀ (hx : x ∈ ker f), Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
⊢ Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
have h₁ : ∀ (hx : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)),
  Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
Tactic: rwa [hf', LinearMap.mem_ker] at hx
Cleared hypotheses: hx
-- 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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have neg : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
Tactic: suffices hfv : f v = 0 by
      use f, v, hfv
      rw [← LinearEquiv.toLinearMap_inj,
        ← sub_eq_zero, ← LinearMap.ker_eq_top, eq_top_iff, ← eq_top]
      simp only [LinearEquiv.transvection.coe_toLinearMap,
        sup_le_iff, Submodule.span_singleton_le_iff_mem, LinearMap.mem_ker, LinearMap.sub_apply,
        LinearEquiv.coe_coe]
      constructor
      · intro x hx
        suffices f x = 0 by
          simpa [this, LinearMap.transvection.apply, sub_eq_zero] using hx
        rwa [hf', LinearMap.mem_ker] at hx
      · simp_all [v, LinearMap.transvection.apply]
-- 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
this : HSub.hSub (α := V) ((e : (a : V) → V) w : V) w ∈ ker f
⊢ Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
have this₁ : HSub.hSub (α := K) (β := K) ((f : (a : V) → K) ((e : (a : V) → V) w : V) : K) ((f : (a : V) → K) w : K) = 0
Tactic: simp only [LinearMap.mem_ker, map_sub] at this
Cleared hypotheses: 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
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
⊢ Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
have neg : HSub.hSub (α := V) ((e : (a : V) → V) w : V) w ∈ ker f
Tactic: suffices e w - w ∈ LinearMap.ker f by
      simp only [LinearMap.mem_ker, map_sub] at this
      simp only [v, LinearMap.map_smul, map_sub, this, smul_zero]
-- 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)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
⊢ HSub.hSub (α := V) ((e : (a : V) → V) w : V) w ∈ ker f
have neg : Eq (α := V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
  (((↑e : V →ₗ[K] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
      (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w) :
    V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
  (0 : V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
Tactic: rw [← hf', ← Submodule.ker_mkQ e.fixedSubmodule, LinearMap.mem_ker]
-- 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
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : Dual R V
v : V
⊢ Eq (α := A ⊗[R] V →ₗ[A] A ⊗[R] V) (LinearMap.baseChange A (transvection f v))
    (transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v))
have a : ∀ (x : V),
  Eq (α := A ⊗[R] V)
    ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A (transvection f v)) :
                A →ₗ[A] V →ₗ[R] A ⊗[R] V) :
              (a : A) → V →ₗ[R] A ⊗[R] V)
            1 :
          (a : V) → A ⊗[R] V)
        x :
      A ⊗[R] V)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v)) :
                A →ₗ[A] V →ₗ[R] A ⊗[R] V) :
              (a : A) → V →ₗ[R] A ⊗[R] V)
            1 :
          (a : V) → A ⊗[R] V)
        x :
      A ⊗[R] V)
Tactic: ext
-- 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
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
⊢ Eq.{u_6 + 1} (α := W →ₗ[A] W) ((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W)
    (LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W)
have h : ∀ (w : W),
  Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        w :
      W)
Tactic: ext w