awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
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
⊢ finrank.{u_3, u_2} K ↥(ker f) ≤ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule

Tactic:
linarith
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 = ⊥
suffices : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
⊢ (↑e : V →ₗ[K] V).fixedSubmodule = ker f

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
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 = ⊥
rw : finrank K V = 1 + finrank.{u_3, u_2} K ↥(ker f)
⊢ finrank.{u_3, u_2} K (V ⧸ ker f) = 1

Tactic:
rw [← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank]

Premises used: Submodule.finrank_quotient_add_finrank, Nat.add_left_inj
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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₁ : f ≠ 0
⊢ finrank K V = 1 + finrank.{u_3, u_2} K ↥(ker f)

Tactic:
rw [← f.finrank_ker_add_one_of_ne_zero, add_comm]

Premises used: add_comm, Module.Dual.finrank_ker_add_one_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 = ⊥
⊢ f ≠ 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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

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
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
rw : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 1
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤

Tactic:
rw [Submodule.sup_span_singleton_eq_top_iff hw]

Premises used: Submodule.sup_span_singleton_eq_top_iff
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
apply : 1 ≤ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
⊢ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 1

Tactic:
apply le_antisymm he

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
a : ℕ
⊢ 1 ≤ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)

Tactic:
apply Nat.one_le_of_lt

Premises used: Nat.one_le_of_lt
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 :
  ∀ (hefixed_ne_top : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) = 0),
    (↑e : V →ₗ[K] V).fixedSubmodule = ⊤
⊢ finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≠ 0

Tactic:
contrapose hefixed_ne_top
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V
⊢ (↑e : V →ₗ[K] V).fixedSubmodule = ⊤

Tactic:
apply eq_top_of_finrank_eq

Premises used: Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
h₃ h₄ : finrank K V = finrank K V
⊢ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule = finrank K V

Tactic:
rw [← Nat.add_left_cancel_iff, finrank_quotient_add_finrank, hefixed_ne_top, zero_add]

Premises used: Submodule.finrank_quotient_add_finrank, Nat.add_left_cancel_iff, zero_add
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 = ⊤

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]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 = transvection hfv
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e

Tactic:
use f, v, hfv
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 ⊔ K ∙ w ≤ ((↑e : V →ₗ[K] V) - (↑(transvection hfv) : V →ₗ[K] V)).ker
⊢ e = transvection hfv

Tactic:
rw [← LinearEquiv.toLinearMap_inj,
        ← sub_eq_zero, ← LinearMap.ker_eq_top, eq_top_iff, ← eq_top]

Premises used: LinearMap.ker_eq_top, eq_top_iff, LinearEquiv.toLinearMap_inj, sub_eq_zero
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 ∧
    HSub.hSub (α := V) (β := V) ((e : (a : V) → V) w : V) ((LinearMap.transvection f v : (a : V) → V) w : V) = 0
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w ≤ ((↑e : V →ₗ[K] V) - (↑(transvection hfv) : V →ₗ[K] V)).ker

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]

Premises used: LinearMap.mem_ker, sup_le_iff, LinearEquiv.transvection.coe_toLinearMap, LinearMap.sub_apply, Submodule.span_singleton_le_iff_mem, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
h₁ : HSub.hSub (α := V) (β := V) ((e : (a : V) → V) w : V) ((LinearMap.transvection f v : (a : V) → V) w : V) = 0
⊢ (↑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:
constructor
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
this : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
⊢ x ∈ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker

Tactic:
simpa [this, LinearMap.transvection.apply, sub_eq_zero] using hx

Premises used: sub_eq_zero, LinearMap.transvection.apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
⊢ x ∈ ((↑e : V →ₗ[K] V) - LinearMap.transvection f v).ker

Tactic:
suffices f x = 0 by
          simpa [this, LinearMap.transvection.apply, sub_eq_zero] using hx
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
h₁ h₂ h₃ 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)
⊢ Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)

Tactic:
rwa [hf', LinearMap.mem_ker] at hx

Premises used: LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
⊢ HSub.hSub (α := V) (β := V) ((e : (a : V) → V) w : V) ((LinearMap.transvection f v : (a : V) → V) w : V) = 0

Tactic:
simp_all [v, LinearMap.transvection.apply]

Premises used: LinearMap.transvection.apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
neg : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e

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]