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
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) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)

Tactic:
codRestrict_apply (range u) u x

Premises used: LinearMap.range, LinearMap.codRestrict_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
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) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)

Tactic:
exact codRestrict_apply (range u) u x

Premises used: LinearMap.range, LinearMap.codRestrict_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
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 : ℕ)
rw₃ rw₄ :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 ↔
    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

Tactic:
rw [mem_dilatransvections_iff_rank, finrank, ← one_toNat,
    toNat_le_iff_le_of_lt_aleph0 (rank_lt_aleph0 K _) one_lt_aleph0]

Premises used: Cardinal.one_lt_aleph0, LinearEquiv.mem_dilatransvections_iff_rank, Cardinal.toNat_le_iff_le_of_lt_aleph0, Module.rank_lt_aleph0, Module.finrank, Cardinal.one_toNat
-- 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
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
rw₂ 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
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ↔
    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]

Premises used: LinearEquiv.mem_dilatransvections_iff_finrank, LinearEquiv.finrank_eq, LinearMap.fixedSubmodule_eq_ker, LinearMap.quotKerEquivRange
-- 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
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
rw₂ rw₃ :
  Module.rank K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 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

Tactic:
rw [mem_dilatransvections_iff_rank, ← (quotKerEquivRange _).rank_eq, ← fixedSubmodule_eq_ker]

Premises used: LinearEquiv.mem_dilatransvections_iff_rank, LinearEquiv.rank_eq, LinearMap.fixedSubmodule_eq_ker, LinearMap.quotKerEquivRange
-- 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
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e ↔
    Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1

Tactic:
⟨fun ⟨f, v, hfv, he⟩ ↦ ?_, fun ⟨he, he'⟩ ↦ ?_⟩

Premises used: _private.0.LinearEquiv.mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one.match_2, LinearEquiv.transvections, _private.0.LinearEquiv.mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one.match_1, Membership.mem, LinearEquiv.dilatransvections, And, Iff.intro, LinearEquiv.fixedReduce, OfNat.ofNat, 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
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
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
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e ↔
    Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1

Tactic:
refine ⟨fun ⟨f, v, hfv, he⟩ ↦ ?_, fun ⟨he, he'⟩ ↦ ?_⟩
-- 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)) (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
refine_1₁ : e.fixedReduce = 1
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1

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)) (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) (transvection hfv)
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e

Tactic:
rw [he]
-- 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)) (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) (transvection hfv)

Tactic:
transvection_mem_dilatransvections hfv

Premises used: LinearEquiv.transvection_mem_dilatransvections
-- 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)) (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) (transvection hfv)

Tactic:
exact transvection_mem_dilatransvections hfv

Premises used: LinearEquiv.transvection_mem_dilatransvections
-- 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)) (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 :
  ∀ (v_1 : V),
    HSub.hSub (α := V) ((transvection hfv : (a : V) → V) v_1 : V) v_1 ∈ (↑(transvection hfv) : V →ₗ[K] V).fixedSubmodule
⊢ e.fixedReduce = 1

Tactic:
rw [one_eq_refl, fixedReduce_eq_one, he]

Premises used: LinearEquiv.fixedReduce_eq_one, LinearEquiv.one_eq_refl
-- 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)) (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
refine_1 : HSub.hSub (α := V) ((transvection hfv : (a : V) → V) x : V) x ∈ ker f
⊢ HSub.hSub (α := V) ((transvection hfv : (a : V) → V) x : V) x ∈ (↑(transvection hfv) : V →ₗ[K] V).fixedSubmodule

Tactic:
apply ker_le_fixedSubmodule_transvection hfv

Premises used: LinearEquiv.ker_le_fixedSubmodule_transvection
-- 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)) (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
refine_1 : x + HSMul.hSMul.{u_3, u_2, u_2} (α := K) ((f : (a : V) → K) x : K) v - x ∈ ker f
⊢ HSub.hSub (α := V) ((transvection hfv : (a : V) → V) x : V) x ∈ ker f

Tactic:
rw [transvection.apply]

Premises used: LinearEquiv.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)) (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
⊢ x + HSMul.hSMul.{u_3, u_2, u_2} (α := K) ((f : (a : V) → K) x : K) v - x ∈ ker f

Tactic:
simp [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 : 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
neg : ∀ (he_one : ¬e = 1), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e

Tactic:
by_cases he_one : e = 1
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : e = 1
⊢ Eq.{u_3 + 1} (α := K) ((0 : (a : V) → K) 0 : K) (0 : K)

Tactic:
simp
-- 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : e = 1
⊢ e = transvection (f := 0) (v := 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_1 : 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)
h : e = transvection (f := 0) (v := 0) ⋯
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e

Tactic:
use 0, 0, by simp, by 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 : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e
he' : e.fixedReduce = 1
he_one : ¬e = 1
rwa : ¬(↑e : V →ₗ[K] V).fixedSubmodule = ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ¬e = refl K V
⊢ (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤

Tactic:
rwa [ne_eq, LinearEquiv.fixedSubmodule_eq_top_iff]

Premises used: LinearEquiv.fixedSubmodule_eq_top_iff, ne_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 : 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 ≠ ⊤

Tactic:
have hefixed_ne_top : e.fixedSubmodule ≠ ⊤ := by
      rwa [ne_eq, LinearEquiv.fixedSubmodule_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 : 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 ≠ ⊤
neg : ∀ (w : V) (hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule), Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e
⊢ 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

Premises used: LinearEquiv.toLinearMap, LinearMap.fixedSubmodule, SetLike.exists_not_mem_of_ne_top, rfl
-- 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 : 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
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
⊢ 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

Premises used: inferInstance, Submodule.exists_dual_map_eq_bot_of_notMem
-- 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 : 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 = ⊥
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
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V)) (transvections K V) e

Tactic:
rw [mem_dilatransvections_iff_finrank_quotient] at he

Premises used: LinearEquiv.mem_dilatransvections_iff_finrank_quotient
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
hle : (↑e : V →ₗ[K] V).fixedSubmodule ≤ ker f
hd : finrank.{u_3, u_2} K ↥(ker f) ≤ finrank.{u_3, u_2} K ↥(↑e : V →ₗ[K] V).fixedSubmodule
⊢ (↑e : V →ₗ[K] V).fixedSubmodule = ker f

Tactic:
apply Submodule.eq_of_le_of_finrank_le

Premises used: Submodule.eq_of_le_of_finrank_le
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
x : V
hle :
  x ∈ (↑e : V →ₗ[K] V).fixedSubmodule →
    Membership.mem (α := K) (map f (↑e : V →ₗ[K] V).fixedSubmodule) ((f : (a : V) → K) x : K)
⊢ x ∈ (↑e : V →ₗ[K] V).fixedSubmodule → x ∈ ker f

Tactic:
rw [mem_ker, ← Submodule.mem_bot K, ← hf]

Premises used: Submodule.mem_bot, 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
x : V
⊢ x ∈ (↑e : V →ₗ[K] V).fixedSubmodule →
    Membership.mem (α := K) (map f (↑e : V →ₗ[K] V).fixedSubmodule) ((f : (a : V) → K) x : K)

Tactic:
mem_map_of_mem

Premises used: Set.Mem, Submodule.mem_map_of_mem
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
x : V
⊢ x ∈ (↑e : V →ₗ[K] V).fixedSubmodule →
    Membership.mem (α := K) (map f (↑e : V →ₗ[K] V).fixedSubmodule) ((f : (a : V) → K) x : K)

Tactic:
exact mem_map_of_mem

Premises used: Submodule.mem_map_of_mem
-- 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 = ⊥
this : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
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
⊢ 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

Premises used: Nat.add_le_add_iff_right, Submodule.finrank_quotient_add_finrank
-- 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 : finrank.{u_3, u_2} K (V ⧸ ker f) = 1
⊢ 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