awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
simp_rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ (x : M), x = 0
simp_rw₁ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ (a = 0 ∨ x = 0)) ↔ ∀ (x : M), x = 0
simp_rw₂ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a = 0 ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
simp_rw₃ : (∀ (x : M), ∃ (a : R), False ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
have simp_rw₄ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
Tactic: simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
    exists_and_right, and_iff_right (exists_ne (0 : R))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
simp_rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ (x : M), x = 0
simp_rw₁ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ (a = 0 ∨ x = 0)) ↔ ∀ (x : M), x = 0
simp_rw₂ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a = 0 ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
simp_rw₃ : (∀ (x : M), ∃ (a : R), False ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
simp_rw₄ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
have simp_rw₅ : (∀ (x : M), (∃ (x : R), x ≠ 0) ∧ x = 0) ↔ ∀ (x : M), x = 0
Tactic: simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
    exists_and_right, and_iff_right (exists_ne (0 : R))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
⊢ 0 < Module.rank R M ↔ ∃ (x : M), x ≠ 0
have contrapose! : Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
⊢ Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0
have rw : Module.rank R M = 0 ↔ ∀ (x : M), x = 0
Tactic: rw [nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h : Module.rank R M = 0
⊢ Module.Finite R M
have inst : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h : Module.rank R M = 0
inst_5 : Nontrivial R
⊢ Module.Finite R M
have h₁ : Subsingleton M
Tactic: rw [rank_zero_iff] at h
Cleared hypotheses: h, inst_5
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥s
eq : s = ⊥
⊢ False
have h₁ : LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 0
Tactic: rw [eq, rank_bot] at h
Cleared hypotheses: h, eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
⊢ Module.Finite R M
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
h_1 : Nontrivial R
⊢ Module.Finite R M
have obtain : ∀ (ι : Type v) (b : Basis ι R M), Module.Finite R M
Tactic: obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
h_1 : Nontrivial R
ι : Type v
b : Basis ι R M
⊢ Module.Finite R M
have this : Finite ι
Tactic: have := mk_lt_aleph0_iff.mp <|
    b.linearIndependent.cardinal_le_rank |>.trans_eq h |>.trans_lt natCast_lt_aleph0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
⊢ Nonempty.{u_1 + 1} (Fintype ι)
have rwa : ∀ (h : lift.{u_1, v} (Module.rank R M) < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
Tactic: rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
rwa : ∀ (h : lift.{u_1, v} (Module.rank R M) < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
⊢ Nonempty.{u_1 + 1} (Fintype ι)
have rwa₁ : ∀ (h : lift.{v, u_1} #ι < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
Tactic: rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
rwa : ∀ (h : lift.{u_1, v} (Module.rank R M) < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₁ : ∀ (h : lift.{v, u_1} #ι < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
⊢ Nonempty.{u_1 + 1} (Fintype ι)
have rwa₂ : ∀ (h : lift.{v, u_1} #ι < ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
Tactic: rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
rwa : ∀ (h : lift.{u_1, v} (Module.rank R M) < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₁ : ∀ (h : lift.{v, u_1} #ι < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₂ : ∀ (h : lift.{v, u_1} #ι < ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
⊢ Nonempty.{u_1 + 1} (Fintype ι)
have rwa₃ : ∀ (h : #ι < ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
Tactic: rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
rwa : ∀ (h : lift.{u_1, v} (Module.rank R M) < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₁ : ∀ (h : lift.{v, u_1} #ι < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₂ : ∀ (h : lift.{v, u_1} #ι < ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₃ : ∀ (h : #ι < ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
⊢ Nonempty.{u_1 + 1} (Fintype ι)
have rwa₄ : ∀ (h : Nonempty.{u_1 + 1} (Fintype ι)), Nonempty.{u_1 + 1} (Fintype ι)
Tactic: rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
⊢ #ι ≤ (↑(finrank R M) : Cardinal.{w})
have rw : lift.{max v w, w} #ι ≤ lift.{max v w, w} (↑(finrank R M) : Cardinal.{w})
Tactic: rw [← lift_le.{max v w}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
b : Finset M
h : LinearIndependent R (M := M) fun (x : ↥b) ↦ (↑x : M)
⊢ b.card ≤ finrank R M
have rw : Fintype.card.{v} ↥b ≤ finrank R M
Tactic: rw [← Fintype.card_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ #ι < ℵ₀
have apply : lift.{v, w} #ι < lift.{v, w} ℵ₀
Tactic: apply Cardinal.lift_lt.1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{v, w} #ι < lift.{v, w} ℵ₀
have hab : lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
hab : lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)
⊢ lift.{v, w} #ι < lift.{v, w} ℵ₀
have hbc : lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
hab : lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)
hbc : lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀
⊢ lift.{v, w} #ι < lift.{v, w} ℵ₀
have b : Cardinal.{max w v}
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀
have hbc : (↑(finrank R M) : Cardinal.{max v w}) < ℵ₀
Tactic: rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have inl : ∀ (h : (↑n : Cardinal.{v}) = Module.rank R M), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
Tactic: rcases hn.eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
inl : ∀ (h : (↑n : Cardinal.{v}) = Module.rank R M), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have inr : ∀ (h : (↑n : Cardinal.{v}) < Module.rank R M), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
Tactic: rcases hn.eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have inl : ∀ (s : Set M) (hs : LinearIndepOn R id s)
  (hs' :
    #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) =
      ⨆ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v)),
  ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
Tactic: obtain ⟨⟨s, hs⟩, hs'⟩ := exists_eq_ciSup_of_not_isSuccLimit
      Cardinal.bddAbove_of_small (h.trans (Module.rank_def R M) ▸ not_isSuccLimit_natCast n)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' :
  #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) =
    ⨆ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have hs'₁ : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
Tactic: rw [← Module.rank_def, ← h] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have this : Finite.{v + 1} (↑s : Type v)
Tactic: have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ natCast_lt_aleph0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
this : Finite.{v + 1} (↑s : Type v)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have inl : ∀ (val : Fintype (↑s : Type v)), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have inr : ∀ (s : Set M) (hs : #(↑s : Type v) = (↑n : Cardinal.{v})) (hs' : LinearIndepOn R id s),
  ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
Tactic: obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
s : Set M
hs : #(↑s : Type v) = (↑n : Cardinal.{v})
hs' : LinearIndepOn R id s
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have this : Finite.{v + 1} (↑s : Type v)
Tactic: have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ natCast_lt_aleph0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
s : Set M
hs : #(↑s : Type v) = (↑n : Cardinal.{v})
hs' : LinearIndepOn R id s
this : Finite.{v + 1} (↑s : Type v)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have inr : ∀ (val : Fintype (↑s : Type v)), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
have pos : ∀ (h : finrank R M = 0),
  ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
Tactic: by_cases h : finrank R M = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
pos :
  ∀ (h : finrank R M = 0),
    ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
have neg : ∀ (h : ¬finrank R M = 0),
  ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
Tactic: by_cases h : finrank R M = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
have pos : ∃ (s : Finset M), s.card = 0 ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
Tactic: rw [le_zero_iff.mp (hn.trans_eq h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ LinearIndependent.{v, u, v} (ι := ↥∅) R (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x))
have h₁ : Eq.{v + 1} (α := M → Prop) (fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x) ∅
Tactic: convert! linearIndependent_empty R M using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
h₁ : Eq.{v + 1} (α := M → Prop) (fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x) ∅
⊢ LinearIndependent.{v, u, v} (ι := ↥∅) R (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x))
have h₂ : ↥∅ = (↑∅ : Type v) →
  Eq.{v + 1} (α := M → Prop) (fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x) fun (x : M) ↦
    Membership.mem (γ := Set M) ∅ x
Tactic: convert! linearIndependent_empty R M using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
i : I
⊢ ∃ v ∈ V (↑i : ι), v ≠ 0
have rw : V (↑i : ι) ≠ ⊥
Tactic: rw [← Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
have hI : ∀ (i : I), ∃ v ∈ V (↑i : ι), v ≠ 0
Tactic: have hI : ∀ i : I, ∃ v ∈ V i, v ≠ (0 : M) := by
    intro i
    rw [← Submodule.ne_bot_iff]
    exact i.prop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
hI : ∀ (i : I), ∃ v ∈ V (↑i : ι), v ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
have choose : ∀ (v : (i : I) → M) (hvV : ∀ (i : I), v i ∈ V (↑i : ι)) (hv : ∀ (i : I), v i ≠ 0),
  lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
Tactic: choose v hvV hv using hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
v : (i : I) → M
hvV : ∀ (i : I), v i ∈ V (↑i : ι)
hv : ∀ (i : I), v i ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
have this : LinearIndependent R v
Tactic: have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{v, w} (↑(finrank R M) : Cardinal.{w})
⊢ #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})
have rwa : ∀ (this : #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})),
  #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})
Tactic: rwa [Cardinal.lift_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})
have suffices : lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{v, w} (↑(finrank R M) : Cardinal.{w})
Tactic: suffices Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{v} (finrank R M : Cardinal.{w}) by
    rwa [Cardinal.lift_le] at this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} (↑(finrank R M) : Cardinal.{v})
have rw : lift.{w, v} (Module.rank R M) = lift.{w, v} (Module.rank R M)
Tactic: rw [finrank_eq_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{v, w} (↑(finrank R M) : Cardinal.{w})
have i : lift.{w, v} (Module.rank R M) = lift.{w, v} (↑(finrank R M) : Cardinal.{v})
Tactic: calc
    Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M) :=
      hp.subtype_ne_bot_le_rank
    _ = Cardinal.lift.{w} (finrank R M : Cardinal.{v}) := by rw [finrank_eq_rank]
    _ = Cardinal.lift.{v} (finrank R M : Cardinal.{w}) := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
i : lift.{w, v} (Module.rank R M) = lift.{w, v} (↑(finrank R M) : Cardinal.{v})
⊢ lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{v, w} (↑(finrank R M) : Cardinal.{w})
have i₁ : lift.{w, v} (↑(finrank R M) : Cardinal.{v}) = lift.{v, w} (↑(finrank R M) : Cardinal.{w})
Tactic: calc
    Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M) :=
      hp.subtype_ne_bot_le_rank
    _ = Cardinal.lift.{w} (finrank R M : Cardinal.{v}) := by rw [finrank_eq_rank]
    _ = Cardinal.lift.{v} (finrank R M : Cardinal.{w}) := by simp