awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(Insert.insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (Insert.insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
insert : (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ Insert.insert i (↑s : Set ι), (f i_1).ker
⊢ (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker
have insert₁ : (f i).ker ⊔ (s.noncommProd f sorry).ker = (f i).ker ⊔ ⨆ x ∈ (↑s : Set ι), (f x).ker
Tactic: simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(Insert.insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (Insert.insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
insert : (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ Insert.insert i (↑s : Set ι), (f i_1).ker
insert₁ : (f i).ker ⊔ (s.noncommProd f ⋯).ker = (f i).ker ⊔ ⨆ x ∈ (↑s : Set ι), (f x).ker
⊢ (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker
have insert₂ : (f i).ker ⊔ (s.noncommProd f sorry).ker = (f i).ker ⊔ ⨆ x ∈ s, (f x).ker
Tactic: simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Disjoint (f i).ker (s.noncommProd f ⋯).ker
have h₁ : Disjoint (f i).ker (((insert i s).erase i).sup fun (i : ι) ↦ (f i).ker)
Tactic: replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
s : Finset ι
comm : (↑s : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker
⊢ (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
have empty : ∀ (comm : (↑∅ : Set ι).Pairwise (Commute on f))
  (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) ∅ fun (i : ι) ↦ (f i).ker),
  (Finset.noncommProd ∅ f comm).ker = ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), (f i).ker
Tactic: induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
        ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h
Cleared hypotheses: s, comm, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
s : Finset ι
comm : (↑s : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker
empty :
  ∀ (comm : (↑∅ : Set ι).Pairwise (Commute on f))
    (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) ∅ fun (i : ι) ↦ (f i).ker),
    (Finset.noncommProd ∅ f comm).ker = ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), (f i).ker
⊢ (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih :
    ∀ (comm : (↑s : Set ι).Pairwise (Commute on f))
      (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker),
      (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker)
  (comm : (↑(insert i s) : Set ι).Pairwise (Commute on f))
  (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (insert i s) fun (i : ι) ↦ (f i).ker),
  ((insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker
Tactic: induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
        ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h
Cleared hypotheses: s, comm, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
s : Finset ι
comm : (↑s : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker
⊢ (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
have empty : ∀ (comm : (↑∅ : Set ι).Pairwise (Commute on f))
  (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) ∅ fun (i : ι) ↦ (f i).ker),
  (Finset.noncommProd ∅ f comm).ker = ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), (f i).ker
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
        ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h
Cleared hypotheses: s, comm, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
s : Finset ι
comm : (↑s : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker
empty :
  ∀ (comm : (↑∅ : Set ι).Pairwise (Commute on f))
    (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) ∅ fun (i : ι) ↦ (f i).ker),
    (Finset.noncommProd ∅ f comm).ker = ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), (f i).ker
⊢ (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih :
    ∀ (comm : (↑s : Set ι).Pairwise (Commute on f))
      (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker),
      (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker)
  (comm : (↑(insert i s) : Set ι).Pairwise (Commute on f))
  (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (insert i s) fun (i : ι) ↦ (f i).ker),
  ((insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
        ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h
Cleared hypotheses: s, comm, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f ↔ f.ker = ⊥
have mp : IsUnit f → f.ker = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
mp : IsUnit f → f.ker = ⊥
⊢ IsUnit f ↔ f.ker = ⊥
have mpr : f.ker = ⊥ → IsUnit f
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : f.ker = ⊥
⊢ IsUnit f
have h_inj₁ : Injective (α := V) (β := V) (⇑f : (a : V) → V)
Tactic: rw [ker_eq_bot] at h_inj
Cleared hypotheses: h_inj
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f ↔ f.range = ⊤
have rw : f.ker = ⊥ ↔ f.range = ⊤
Tactic: rw [isUnit_iff_ker_eq_bot, ker_eq_bot_iff_range_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
rw : f.ker = ⊥ ↔ f.range = ⊤
⊢ IsUnit f ↔ f.range = ⊤
have rw₁ : f.range = ⊤ ↔ f.range = ⊤
Tactic: rw [isUnit_iff_ker_eq_bot, ker_eq_bot_iff_range_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
H : x ≠ 0
⊢ ∃ (y : K), x * y = 1
have this : Surjective (α := K) (β := K) (⇑(LinearMap.mulLeft F x) : (a : K) → K)
Tactic: have : Function.Surjective (LinearMap.mulLeft F x) :=
    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K_1 : Type u
V : Type v
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
hx : x ≠ 0
⊢ (x * if H : x = 0 then 0 else Classical.choose (p := fun (x_1 : K) ↦ x * x_1 = 1) ⋯) = 1
have rw : x * Classical.choose (p := fun (x_1 : K) ↦ x * x_1 = 1) sorry = 1
Tactic: rw [dif_neg hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ finrank.{u, v} K ↥(K ∙ v) = 1
have a : finrank.{u, v} K ↥(K ∙ v) ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
a : finrank.{u, v} K ↥(K ∙ v) ≤ 1
⊢ finrank.{u, v} K ↥(K ∙ v) = 1
have a₁ : 1 ≤ finrank.{u, v} K ↥(K ∙ v)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank.{u, v} K ↥(K ∙ v)
have a : Nontrivial.{v} ↥(K ∙ v)
Tactic: rw [Nat.succ_le_iff, finrank_pos_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ Nontrivial.{v} ↥(K ∙ v)
have h : Ne (α := ↥(K ∙ v)) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule K V) (K ∙ v) x) v sorry) 0
Tactic: use ⟨v, mem_span_singleton_self v⟩, 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ Ne (α := ↥(K ∙ v)) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule K V) (K ∙ v) x) v ⋯) 0
have h : (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule K V) (K ∙ v) x) v sorry) : V) ≠ (↑0 : V)
Tactic: apply Subtype.coe_ne_coe.mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
⊢ IsAtom S ↔ finrank.{u, v} K ↥S = 1
have refine_1 : ∀ (hS : IsAtom S), finrank.{u, v} K ↥S = 1
Tactic: refine ⟨fun hS ↦ ?_, fun hS ↦ ⟨by aesop, fun T hT ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
refine_1 : ∀ (hS : IsAtom S), finrank.{u, v} K ↥S = 1
⊢ IsAtom S ↔ finrank.{u, v} K ↥S = 1
have refine_2 : ∀ (hS : finrank.{u, v} K ↥S = 1) (T : Submodule K V) (hT : T < S), T = ⊥
Tactic: refine ⟨fun hS ↦ ?_, fun hS ↦ ⟨by aesop, fun T hT ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
⊢ finrank.{u, v} K ↥S = 1
have refine_1 : ∀ (v : V) (hv : v ∈ S) (hv_ne : v ≠ 0), finrank.{u, v} K ↥S = 1
Tactic: obtain ⟨v : V, hv : v ∈ S, hv_ne : v ≠ 0⟩ := S.ne_bot_iff.mp hS.ne_bot
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v = S
⊢ finrank.{u, v} K ↥S = 1
have rw : finrank.{u, v} K ↥(K ∙ v) = 1
Tactic: rw [← this, finrank_span_singleton hv_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v = S
rw : finrank.{u, v} K ↥(K ∙ v) = 1
⊢ finrank.{u, v} K ↥S = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← this, finrank_span_singleton hv_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ finrank.{u, v} K ↥S = 1
have refine_1 : K ∙ v = S
Tactic: suffices K ∙ v = S by rw [← this, finrank_span_singleton hv_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ Ne (α := Submodule K V) (K ∙ v) ⊥
have rw : ∃ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v) x ∧ x ≠ 0
Tactic: rw [Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ K ∙ v = S
have this : Ne (α := Submodule K V) (K ∙ v) ⊥
Tactic: have : K ∙ v ≠ ⊥ := by
      rw [Submodule.ne_bot_iff]
      exact ⟨v, mem_span_singleton_self v, hv_ne⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : Ne (α := Submodule K V) (K ∙ v) ⊥
⊢ K ∙ v = S
have refine_1 : K ∙ v ≤ S
Tactic: rwa [← hS.le_iff_eq this, span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : Ne (α := Submodule K V) (K ∙ v) ⊥
refine_1 : K ∙ v ≤ S
⊢ K ∙ v = S
have refine_1₁ : {v} ⊆ (↑S : Set V)
Tactic: rwa [← hS.le_iff_eq this, span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : Ne (α := Submodule K V) (K ∙ v) ⊥
refine_1 : K ∙ v ≤ S
refine_1₁ : {v} ⊆ (↑S : Set V)
⊢ K ∙ v = S
have refine_1₂ : v ∈ (↑S : Set V)
Tactic: rwa [← hS.le_iff_eq this, span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
⊢ T = ⊥
have this : FiniteDimensional.{u, v} K ↥S
Tactic: have : FiniteDimensional K S := .of_finrank_eq_succ hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this : FiniteDimensional.{u, v} K ↥S
⊢ T = ⊥
have this₁ : FiniteDimensional.{u, v} K ↥T
Tactic: have : FiniteDimensional K T := .of_injective (inclusion hT.le) (inclusion_injective hT.le)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this_1 : FiniteDimensional.{u, v} K ↥S
this : FiniteDimensional.{u, v} K ↥T
⊢ T = ⊥
have refine_2 : finrank.{u, v} K ↥T = 0
Tactic: rw [← finrank_eq_zero (R := K)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this_1 : FiniteDimensional.{u, v} K ↥S
this : FiniteDimensional.{u, v} K ↥T
⊢ finrank.{u, v} K ↥T = 0
have refine_2 : ∀ (h : ¬finrank.{u, v} K ↥T = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ Eq (α := Submodule K V) (K ∙ x) ⊤
have this : FiniteDimensional K V
Tactic: have : FiniteDimensional K V := .of_finrank_eq_succ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ Eq (α := Submodule K V) (K ∙ x) ⊤
have h₁ : finrank.{u, v} K ↥(K ∙ x) = finrank K V
Tactic: apply eq_top_of_finrank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank.{u, v} K ↥(K ∙ x) = finrank K V
have h₁ : finrank.{u, v} K ↥(K ∙ x) = 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ ∃ (c : K), c • x = y
have this : Eq (α := Submodule K V) (K ∙ x) ⊤
Tactic: have : Submodule.span K {x} = ⊤ := by
    have : FiniteDimensional K V := .of_finrank_eq_succ h
    apply eq_top_of_finrank_eq
    rw [h]
    exact finrank_span_singleton hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : Eq (α := Submodule K V) (K ∙ x) ⊤
⊢ Membership.mem (γ := Submodule K V) (K ∙ x) y
have rw : Membership.mem (γ := Submodule K V) ⊤ y
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : Eq (α := Submodule K V) (K ∙ x) ⊤
⊢ ∃ (c : K), c • x = y
have this₁ : Membership.mem (γ := Submodule K V) (K ∙ x) y
Tactic: have : y ∈ Submodule.span K {x} := by rw [this]; exact mem_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
nz : v ≠ 0
⊢ finrank K V = 1 ↔ ∀ (w : V), ∃ (c : K), c • v = w
have rw : Eq (α := Submodule K V) (K ∙ v) ⊤ ↔ ∀ (w : V), ∃ (c : K), c • v = w
Tactic: rw [finrank_eq_one_iff_of_nonzero v nz]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Type u_1
A : Type u_2
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : AddCommGroup W
inst_6 : Module K W
inst_7 : Module A W
inst_8 : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
⊢ Surjective.{v + 1, u_1 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
have change : Surjective.{v + 1, u_1 + 1} (α := V) (β := W)
  (⇑((↑K :
          {S : Type u_2} →
            {M : Type v} →
              {M₂ : Type u_1} →
                [inst : Semiring K] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module K M] →
                          [inst_13 : Module K M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
        f) :
    (a : V) → W)
Tactic: change Surjective (f.restrictScalars K)