awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq :
  (∃ (f : R →ₗ[R] Fin n → R), Injective (α := R) (β := Fin n → R) (⇑f : (a : R) → Fin n → R)) →
    ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
have refine_2 : ∀
  (eq :
    (∃ (f : R →ₗ[R] Fin n.pred.succ → R),
        Injective (α := R) (β := Fin n.pred.succ → R) (⇑f : (a : R) → Fin n.pred.succ → R)) →
      ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)),
  ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)
Tactic: rw [← n.succ_pred_eq_of_pos pos] at eq ⊢
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
⊢ ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)
have rcases : ∀ (t : Set M) (ht_sub : t ⊆ s) (ht_span : Eq (α := Submodule K M) (span K t) (span K s))
  (ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))),
  ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)
Tactic: rcases exists_linearIndependent K s with ⟨t, ht_sub, ht_span, ht_indep⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : Eq (α := Submodule K M) (span K t) (span K s)
ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))
⊢ ∃ (u : Finset M), (↑u : Set M) = t ∧ u.card = finrank.{u_2, u_3} K ↥(span K s)
have rw : #(↑t : Type u_3) = (↑(finrank.{u_2, u_3} K ↥(span K s)) : Cardinal.{u_3})
Tactic: rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : Eq (α := Submodule K M) (span K t) (span K s)
ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))
rw : #(↑t : Type u_3) = (↑(finrank.{u_2, u_3} K ↥(span K s)) : Cardinal.{u_3})
⊢ ∃ (u : Finset M), (↑u : Set M) = t ∧ u.card = finrank.{u_2, u_3} K ↥(span K s)
have rw₁ : #(↑t : Type u_3) = Module.rank K ↥(span K s)
Tactic: rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : Eq (α := Submodule K M) (span K t) (span K s)
ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))
rw : #(↑t : Type u_3) = (↑(finrank.{u_2, u_3} K ↥(span K s)) : Cardinal.{u_3})
rw₁ : #(↑t : Type u_3) = Module.rank K ↥(span K s)
⊢ ∃ (u : Finset M), (↑u : Set M) = t ∧ u.card = finrank.{u_2, u_3} K ↥(span K s)
have rw₂ : #(↑t : Type u_3) = Module.rank K ↥(span K t)
Tactic: rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : Eq (α := Submodule K M) (span K t) (span K s)
ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))
rw : #(↑t : Type u_3) = (↑(finrank.{u_2, u_3} K ↥(span K s)) : Cardinal.{u_3})
rw₁ : #(↑t : Type u_3) = Module.rank K ↥(span K s)
rw₂ : #(↑t : Type u_3) = Module.rank K ↥(span K t)
⊢ ∃ (u : Finset M), (↑u : Set M) = t ∧ u.card = finrank.{u_2, u_3} K ↥(span K s)
have rw₃ : #(↑t : Type u_3) = #(↑t : Type u_3)
Tactic: rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : Eq (α := Submodule K M) (span K t) (span K s)
ht_indep : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ t }) K (Subtype.val (p := fun (x : M) ↦ x ∈ t))
⊢ ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)
have obtain : ∀ (t : Finset M) (ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)) (ht_sub : (↑t : Set M) ⊆ s)
  (ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s))
  (ht_indep :
    LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ (↑t : Set M) }) K
      (Subtype.val (p := fun (x : M) ↦ x ∈ (↑t : Set M)))),
  ∃ (t : Finset M),
    (↑t : Set M) ⊆ s ∧
      t.card = finrank.{u_2, u_3} K ↥(span K s) ∧
        Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s) ∧ LinearIndepOn K id (↑t : Set M)
Tactic: obtain ⟨t, rfl, ht_card⟩ : ∃ u : Finset M, ↑u = t ∧ u.card = finrank K (span K s) := by
    rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
Cleared hypotheses: t, ht_sub, ht_span, ht_indep
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
⊢ ∃ (f : Fin (finrank.{u_2, u_3} K ↥(span K s)) → M),
    (∀ (i : Fin (finrank.{u_2, u_3} K ↥(span K s))), f i ∈ s) ∧
      Eq (α := Submodule K M) (span K (range f)) (span K s) ∧ LinearIndependent K f
have rcases : ∀ (t : Finset M) (hts : (↑t : Set M) ⊆ s) (ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s))
  (ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)) (ht_indep : LinearIndepOn K id (↑t : Set M)),
  ∃ (f : Fin (finrank.{u_2, u_3} K ↥(span K s)) → M),
    (∀ (i : Fin (finrank.{u_2, u_3} K ↥(span K s))), f i ∈ s) ∧
      Eq (α := Submodule K M) (span K (range f)) (span K s) ∧ LinearIndependent K f
Tactic: rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, hts, ht_card, ht_span, ht_indep⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
⊢ Membership.mem (γ := Submodule K M) (span K s) x ↔
    ∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
have mp : Membership.mem (γ := Submodule K M) (span K s) x →
  ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
mp :
  Membership.mem (γ := Submodule K M) (span K s) x →
    ∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ Membership.mem (γ := Submodule K M) (span K s) x ↔
    ∃ (c : M →₀ K),
      c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
        (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
have mpr : (∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x) →
  Membership.mem (γ := Submodule K M) (span K s) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
⊢ ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
have mp : ∀ (t : Finset M) (ht_sub : (↑t : Set M) ⊆ s) (ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s))
  (ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)) (ht_indep : LinearIndepOn K id (↑t : Set M)),
  ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
Tactic: rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
t : Finset M
ht_sub : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
⊢ ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
have mp : ∀ (c : M →₀ K) (hct : (↑c.support : Set M) ⊆ (↑t : Set M)) (hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x),
  ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
Tactic: rcases mem_span_set.mp (ht_span ▸ h) with ⟨c, hct, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
K : Type u_2
M : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
s : Set M
x : M
inst_3 : Module.Finite.{u_2, u_3} K ↥(span K s)
h : Membership.mem (γ := Submodule K M) (span K s) x
t : Finset M
ht_sub : (↑t : Set M) ⊆ s
ht_card : t.card = finrank.{u_2, u_3} K ↥(span K s)
ht_span : Eq (α := Submodule K M) (span K (↑t : Set M)) (span K s)
ht_indep : LinearIndepOn K id (↑t : Set M)
c : M →₀ K
hct : (↑c.support : Set M) ⊆ (↑t : Set M)
hx : (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
⊢ ∃ (c : M →₀ K),
    c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s) ∧
      (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : K) ↦ r • mi) = x
have mp : c.support.card ≤ finrank.{u_2, u_3} K ↥(span K s)
Tactic: refine ⟨c, ?_, hct.trans ht_sub, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Subsingleton (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Subsingleton M
⊢ Module.rank R M = 0
have rw : LE.le.{u_2 + 1} (α := Cardinal.{u_2})
  (⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2)) ⊥
Tactic: rw [Module.rank, ← bot_eq_zero, eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
⊢ Module.rank R M ≤ Module.rank R (M ⧸ M')
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
⊢ Module.rank R M ≤ Module.rank R (M ⧸ M')
have rw : ⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2) ≤ Module.rank R (M ⧸ M')
Tactic: rw [Module.rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2) ≤ Module.rank R (M ⧸ M')
have refine : ∀ (x : { s : Set M // LinearIndepOn R id s }) (s : Set M) (hs : LinearIndepOn R id s),
  LinearIndependent R (M := M ⧸ M')
    fun (x : (↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type u_2)) ↦
    (M'.mkQ : (a : M) → M ⧸ M') (↑x : M)
Tactic: refine ciSup_le fun ⟨s, hs⟩ ↦ LinearIndependent.cardinal_le_rank (v := (M'.mkQ ·)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs : LinearIndepOn R id s
⊢ LinearIndependent R (M := M ⧸ M')
    fun (x : (↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type u_2)) ↦
    (M'.mkQ : (a : M) → M ⧸ M') (↑x : M)
have hs₁ : ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
  Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
Tactic: rw [LinearIndepOn, linearIndependent_iff'] at hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
⊢ LinearIndependent R (M := M ⧸ M')
    fun (x : (↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs_1) : Set M) : Type u_2)) ↦
    (M'.mkQ : (a : M) → M ⧸ M') (↑x : M)
have simp_rw : ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R), ∑ x ∈ s_1, g x • (↑x : M) ∈ M' → ∀ i ∈ s_1, g i = 0
Tactic: simp_rw [linearIndependent_iff', ← map_smul, ← map_sum, mkQ_apply, Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset (↑s : Type u_2)
g : (↑s : Type u_2) → R
hg : ∑ x ∈ t, g x • (↑x : M) ∈ M'
i : (↑s : Type u_2)
hi : i ∈ t
⊢ g i = 0
have obtain : ∀ (r : ↥(nonZeroDivisors R)) (hg : HSMul.hSMul (β := M) r (∑ x ∈ t, g x • (↑x : M)) = 0), g i = 0
Tactic: obtain ⟨r, hg⟩ := hN hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset (↑s : Type u_2)
g : (↑s : Type u_2) → R
hg_1 : ∑ x ∈ t, g x • (↑x : M) ∈ M'
i : (↑s : Type u_2)
hi : i ∈ t
r : ↥(nonZeroDivisors R)
hg : HSMul.hSMul (β := M) r (∑ x ∈ t, g x • (↑x : M)) = 0
⊢ g i = 0
have hg₁ : Eq (α := M) (∑ x ∈ t, ((↑r : R) * g x) • (↑x : M)) 0
Tactic: simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ Module.rank R M = 0 ↔ Module.IsTorsion R M
have rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ ⦃x : M⦄, ∃ (a : ↥(nonZeroDivisors R)), a • x = 0
Tactic: rw [Module.IsTorsion, rank_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
⊢ finrank R M = 0 ↔ IsTorsion R M
have rw : finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
Tactic: rw [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Torsion.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
⊢ finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
have norm_cast : finrank R M = 0 ↔ finrank R M = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (p ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
have zero : Eq (α := ι →₀ M ⊗[R] N)
  (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) (0 ⊗ₜ[R] n) :
    ι →₀ M ⊗[R] N)
  (Finsupp.sum 0 fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
Tactic: induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppLeft]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
zero :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (0 ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (p ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
have add : ∀ (f g : ι →₀ M)
  (hf :
    Eq (α := ι →₀ M ⊗[R] N)
      (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
          (f ⊗ₜ[R] n) :
        ι →₀ M ⊗[R] N)
      (f.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N))
  (hg :
    Eq (α := ι →₀ M ⊗[R] N)
      (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
          (g ⊗ₜ[R] n) :
        ι →₀ M ⊗[R] N)
      (g.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)),
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        ((f + g) ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    ((f + g).sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
Tactic: induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppLeft]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
zero :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (0 ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
add :
  ∀ (f g : ι →₀ M)
    (hf :
      Eq (α := ι →₀ M ⊗[R] N)
        (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
            (f ⊗ₜ[R] n) :
          ι →₀ M ⊗[R] N)
        (f.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N))
    (hg :
      Eq (α := ι →₀ M ⊗[R] N)
        (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
            (g ⊗ₜ[R] n) :
          ι →₀ M ⊗[R] N)
        (g.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)),
    Eq (α := ι →₀ M ⊗[R] N)
      (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
          ((f + g) ⊗ₜ[R] n) :
        ι →₀ M ⊗[R] N)
      ((f + g).sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (p ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
have single : ∀ (a : ι) (b : M),
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (Finsupp.single a b ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum (Finsupp.single a b) fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
Tactic: induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppLeft]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
              (p ⊗ₜ[R] n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
have rw : Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
  ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
Tactic: rw [finsuppLeft_apply_tmul, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]