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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have pos : ∀ (he_one : e = 1), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
Tactic: by_cases he_one : e = 1
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
pos : ∀ (he_one : e = 1), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have neg : ∀ (he_one : ¬e = 1), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
Tactic: by_cases he_one : e = 1
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : e = 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have w : Dual K V
Tactic: use 0, 0, by simp, by aesop
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : e = 1
w : Dual K V
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have w₁ : V
Tactic: use 0, 0, by simp, by aesop
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : e = 1
w : Dual K V
w₁ : V
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have w₂ : Eq.{u_3 + 1} (α := K) ((0 : (a : V) → K) 0 : K) (0 : K)
Tactic: use 0, 0, by simp, by aesop
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : e = 1
w : Dual K V
w₁ : V
w₂ : Eq.{u_3 + 1} (α := K) ((0 : (a : V) → K) 0 : K) (0 : K)
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have h : e = transvection (f := 0) (v := 0) sorry
Tactic: use 0, 0, by simp, by aesop
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : ¬e = 1
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
have rwa : ¬(↑e : V →ₗ[K] V).fixedSubmodule = ⊤
Tactic: rwa [ne_eq, LinearEquiv.fixedSubmodule_eq_top_iff]
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : ¬e = 1
rwa : ¬(↑e : V →ₗ[K] V).fixedSubmodule = ⊤
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
have rwa₁ : ¬e = refl K V
Tactic: rwa [ne_eq, LinearEquiv.fixedSubmodule_eq_top_iff]
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : ¬e = 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
Tactic: have hefixed_ne_top : e.fixedSubmodule ≠ ⊤ := by
      rwa [ne_eq, LinearEquiv.fixedSubmodule_eq_top_iff]
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have neg : ∀ (w : V) (hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
Tactic: obtain ⟨w : V, hw : w ∉ e.fixedSubmodule⟩ :=
      SetLike.exists_not_mem_of_ne_top e.fixedSubmodule hefixed_ne_top rfl
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
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
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have neg : ∀ (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 = ⊥), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
Tactic: obtain ⟨f, hfw, hf⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hw inferInstance
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
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 = ⊥
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have neg : ∀ (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 = ⊥), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
Tactic: rw [mem_dilatransvections_iff_finrank_quotient] at he
Cleared hypotheses: he, he', he_one, hefixed_ne_top, w, hw, f, hfw, hf
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
⊢ (↑e : V →ₗ[K] V).fixedSubmodule = ker f
have hle : (↑e : V →ₗ[K] V).fixedSubmodule ≤ ker f
Tactic: apply Submodule.eq_of_le_of_finrank_le
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
hle : (↑e : V →ₗ[K] V).fixedSubmodule ≤ ker f
⊢ (↑e : V →ₗ[K] V).fixedSubmodule = ker f
have hd : finrank.{u_3, u_2} K ↥(ker f) ≤ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
Tactic: apply Submodule.eq_of_le_of_finrank_le
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
x : V
⊢ x ∈ (↑e : V →ₗ[K] V).fixedSubmodule → x ∈ ker f
have hle : x ∈ (↑e : V →ₗ[K] V).fixedSubmodule →
  Membership.mem (α := K) (map f (↑e : V →ₗ[K] V).fixedSubmodule) ((f : (a : V) → K) x : K)
Tactic: rw [mem_ker, ← Submodule.mem_bot K, ← hf]
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
⊢ finrank.{u_3, u_2} K ↥(ker f) ≤ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
have hd : ∀ (he : finrank K V ≤ 1 + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule) (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 = ⊥)
  (this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1),
  finrank.{u_3, u_2} K ↥(ker f) ≤ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
Tactic: rw [← Nat.add_le_add_iff_right, finrank_quotient_add_finrank] at he
Cleared hypotheses: he', he_one, hefixed_ne_top, w, hw, f, hfw, hf, this
-- 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_1 : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he : finrank K V ≤ 1 + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
⊢ finrank.{u_3, u_2} K ↥(ker f) ≤ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
have this₁ : finrank.{u_3, u_2} K (V ⧸ ker f) + finrank.{u_3, u_2} K ↥(ker f) = finrank K V
Tactic: have := (LinearMap.ker f).finrank_quotient_add_finrank
-- 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_1 : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he : finrank K V ≤ 1 + finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
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 = ⊥
this_1 : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
this : finrank.{u_3, u_2} K (V ⧸ ker f) + finrank.{u_3, u_2} K ↥(ker f) = finrank K V
⊢ finrank.{u_3, u_2} K ↥(ker f) ≤ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
have linarith : finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule < finrank.{u_3, u_2} K ↥(ker f) →
  -1 + ((↑(finrank K V) : ℤ) - HAdd.hAdd (α := ℤ) 1 (↑(finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule) : ℤ)) +
          -HSub.hSub (α := ℤ) (↑(finrank.{u_3, u_2} K (V ⧸ ker f)) : ℤ) 1 +
        (HAdd.hAdd (α := ℤ) (↑(finrank.{u_3, u_2} K (V ⧸ ker f)) : ℤ) (↑(finrank.{u_3, u_2} K ↥(ker f)) : ℤ) -
          (↑(finrank K V) : ℤ)) +
      (HAdd.hAdd (α := ℤ) (↑(finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule) : ℤ) 1 -
        (↑(finrank.{u_3, u_2} K ↥(ker f)) : ℤ)) =
    0
Tactic: linarith
-- 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 = ⊥
⊢ (↑e : V →ₗ[K] V).fixedSubmodule = ker f
have suffices : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
Tactic: suffices finrank K (V ⧸ LinearMap.ker f) = 1 by
        apply Submodule.eq_of_le_of_finrank_le
        · intro x
          rw [mem_ker, ← Submodule.mem_bot K, ← hf]
          exact mem_map_of_mem
        rw [← Nat.add_le_add_iff_right, finrank_quotient_add_finrank] at he
        have := (LinearMap.ker f).finrank_quotient_add_finrank
        linarith
-- 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 = ⊥
⊢ finrank.{u_3, u_2} K (V ⧸ ker f) = 1
have rw : finrank K V = 1 + finrank.{u_3, u_2} K ↥(ker f)
Tactic: rw [← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank]
-- 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 = ⊥
⊢ finrank K V = 1 + finrank.{u_3, u_2} K ↥(ker f)
have hf₁ : f ≠ 0
Tactic: rw [← f.finrank_ker_add_one_of_ne_zero, add_comm]
-- 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 = ⊥
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
have hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
Tactic: have hf' : e.fixedSubmodule = LinearMap.ker f := by
      suffices finrank K (V ⧸ LinearMap.ker f) = 1 by
        apply Submodule.eq_of_le_of_finrank_le
        · intro x
          rw [mem_ker, ← Submodule.mem_bot K, ← hf]
          exact mem_map_of_mem
        rw [← Nat.add_le_add_iff_right, finrank_quotient_add_finrank] at he
        have := (LinearMap.ker f).finrank_quotient_add_finrank
        linarith
      rw [← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank]
      rw [← f.finrank_ker_add_one_of_ne_zero, add_comm]
      aesop
-- 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
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
have rw : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 1
Tactic: rw [Submodule.sup_span_singleton_eq_top_iff hw]
-- 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
⊢ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 1
have apply : 1 ≤ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
Tactic: apply le_antisymm 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)) (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
⊢ 1 ≤ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
have h : 0 < finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
Tactic: apply Nat.one_le_of_lt
-- 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
h : 0 < 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)
have a : ℕ
Tactic: apply Nat.one_le_of_lt
-- 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
⊢ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≠ 0
have h : ∀ (hefixed_ne_top : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 0), (↑e : V →ₗ[K] V).fixedSubmodule = ⊤
Tactic: contrapose hefixed_ne_top
Cleared hypotheses: hefixed_ne_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
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
⊢ (↑e : V →ₗ[K] V).fixedSubmodule = ⊤
have h : finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V
Tactic: apply eq_top_of_finrank_eq