awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
h : Basis ι R M
rw : finrank R M = (toNat : (a : Cardinal.{w}) → ℕ) #ι
⊢ finrank R M = Nat.card ι
have rw₁ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{v, w} #ι)
Tactic: rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
h : Basis ι R M
rw : finrank R M = (toNat : (a : Cardinal.{w}) → ℕ) #ι
rw₁ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{v, w} #ι)
⊢ finrank R M = Nat.card ι
have rw₂ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{w, v} (Module.rank R M))
Tactic: rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
h : Basis ι R M
rw : finrank R M = (toNat : (a : Cardinal.{w}) → ℕ) #ι
rw₁ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{v, w} #ι)
rw₂ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{w, v} (Module.rank R M))
⊢ finrank R M = Nat.card ι
have rw₃ : finrank R M = (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M)
Tactic: rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
h : Basis ι R M
rw : finrank R M = (toNat : (a : Cardinal.{w}) → ℕ) #ι
rw₁ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{v, w} #ι)
rw₂ : finrank R M = (toNat : (a : Cardinal.{max v w}) → ℕ) (Cardinal.lift.{w, v} (Module.rank R M))
rw₃ : finrank R M = (toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M)
⊢ finrank R M = Nat.card ι
have rw₄ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
  ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
h : Basis ι R M
⊢ (↑(finrank R M) : Cardinal.{w}) = #ι
have intro : ∀ (val : Fintype ι), (↑(finrank R M) : Cardinal.{w}) = #ι
Tactic: cases @nonempty_fintype _ (Module.Finite.finite_basis h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
h : Basis ι R M
val : Fintype ι
⊢ (↑(finrank R M) : Cardinal.{w}) = #ι
have intro : Eq.{w + 2} (α := Cardinal.{w}) (↑(finrank R M) : Cardinal.{w}) (↑(Fintype.card ι) : Cardinal.{w})
Tactic: rw [Cardinal.mk_fintype, finrank_eq_card_basis h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
h : Basis ι R M
val : Fintype ι
intro : Eq.{w + 2} (α := Cardinal.{w}) (↑(finrank R M) : Cardinal.{w}) (↑(Fintype.card ι) : Cardinal.{w})
⊢ (↑(finrank R M) : Cardinal.{w}) = #ι
have intro₁ : Eq.{w + 2} (α := Cardinal.{w}) (↑(Fintype.card ι) : Cardinal.{w}) (↑(Fintype.card ι) : Cardinal.{w})
Tactic: rw [Cardinal.mk_fintype, finrank_eq_card_basis h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
b : Finset ι
h : Basis.{w, u, v} (↥b) R M
⊢ finrank R M = b.card
have rw : Fintype.card.{w} ↥b = b.card
Tactic: rw [finrank_eq_card_basis h, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
b : Finset ι
h : Basis.{w, u, v} (↥b) R M
rw : Fintype.card.{w} ↥b = b.card
⊢ finrank R M = b.card
have rw₁ : b.card = b.card
Tactic: rw [finrank_eq_card_basis h, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
⊢ Module.rank R R = 1
have rw : Cardinal.lift.{u, u} (Module.rank R R) = Cardinal.lift.{u, u} 1
Tactic: rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
rw : Cardinal.lift.{u, u} (Module.rank R R) = Cardinal.lift.{u, u} 1
⊢ Module.rank R R = 1
have rw₁ : Cardinal.lift.{u, u} #PUnit.{u + 1} = Cardinal.lift.{u, u} 1
Tactic: rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
rw : Cardinal.lift.{u, u} (Module.rank R R) = Cardinal.lift.{u, u} 1
rw₁ : Cardinal.lift.{u, u} #PUnit.{u + 1} = Cardinal.lift.{u, u} 1
⊢ Module.rank R R = 1
have rw₂ : Cardinal.lift.{u, u} 1 = Cardinal.lift.{u, u} 1
Tactic: rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
x : M
h : Bijective.{u + 1, v + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
⊢ finrank R M = 1
have rw : finrank R R = 1
Tactic: rw [← (LinearEquiv.ofBijective _ h).finrank_eq, finrank_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
x : M
h : Bijective.{u + 1, v + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
rw : finrank R R = 1
⊢ finrank R M = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← (LinearEquiv.ofBijective _ h).finrank_eq, finrank_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
x : M
h : Bijective.{u + 1, v + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
⊢ Module.rank R M = 1
have rw : finrank R M = 1
Tactic: rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_toSpanSingleton h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
x : M
h : Bijective.{u + 1, v + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
rw : finrank R M = 1
⊢ Module.rank R M = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_toSpanSingleton h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
h : Bijective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ finrank R S = 1
have rw : finrank R R = 1
Tactic: rw [← (AlgEquiv.ofBijective (Algebra.ofId R S) h).toLinearEquiv.finrank_eq, finrank_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
h : Bijective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : finrank R R = 1
⊢ finrank R S = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← (AlgEquiv.ofBijective (Algebra.ofId R S) h).toLinearEquiv.finrank_eq, finrank_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
h : Bijective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R S = 1
have rw : finrank R S = 1
Tactic: rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_algebraMap h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
h : Bijective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : finrank R S = 1
⊢ Module.rank R S = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_algebraMap h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι_1 : Type w
ι' : Type w'
inst_3 : StrongRankCondition R
ι : Type u_2
b : Basis ι R R
⊢ Unique ι
have this : #ι = (↑(finrank R R) : Cardinal.{u_2})
Tactic: have : Cardinal.mk ι = ↑(Module.finrank R R) := (Module.mk_finrank_eq_card_basis b).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι_1 : Type w
ι' : Type w'
inst_3 : StrongRankCondition R
ι : Type u_2
b : Basis ι R R
this : #ι = (↑(finrank R R) : Cardinal.{u_2})
⊢ Unique ι
have this₁ : Subsingleton ι ∧ Nonempty ι
Tactic: have : Subsingleton ι ∧ Nonempty ι := by simpa [Cardinal.eq_one_iff_unique]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
⊢ Module.rank R M < ℵ₀
have simp : ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) < ℵ₀
Tactic: simp only [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) < ℵ₀
have obtain : ∀ (S : Finset M) (hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤),
  ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) < ℵ₀
Tactic: obtain ⟨S, hS⟩ := Module.finite_def.mp ‹_›
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R_1 : Type u
S : Type u_1
M_1 : Type v
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
ι : Type w
ι' : Type w'
inst_3 : StrongRankCondition R_1
R : Type u_2
M : Type u_3
inst_4 : DivisionRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
s t : Set M
inst_7 : Module.Finite.{u_2, u_3} R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ Fintype (↑(hs.extend (s := s) (t := t) hst) : Type u_3)
have refine : #(↑(hs.extend (s := s) (t := t) hst) : Type u_3) < ℵ₀
Tactic: refine Classical.choice (Cardinal.lt_aleph0_iff_fintype.1 ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R_1 : Type u
S : Type u_1
M_1 : Type v
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
ι : Type w
ι' : Type w'
inst_3 : StrongRankCondition R_1
R : Type u_2
M : Type u_3
inst_4 : DivisionRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
s t : Set M
inst_7 : Module.Finite.{u_2, u_3} R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ #(↑(hs.extend (s := s) (t := t) hst) : Type u_3) < ℵ₀
have rw : Module.rank R ↥(span R t) < ℵ₀
Tactic: rw [← rank_span_set (hs.linearIndepOn_extend hst), hs.span_extend_eq_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
⊢ (↑(finrank R M) : Cardinal.{v}) = Module.rank R M
have rw : (↑((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M)) : Cardinal.{v}) = Module.rank R M
Tactic: rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
rw : (↑((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M)) : Cardinal.{v}) = Module.rank R M
⊢ (↑(finrank R M) : Cardinal.{v}) = Module.rank R M
have rw₁ : Module.rank R M = Module.rank R M
Tactic: rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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 : Free R M
inst_5 : Module.Finite R M
⊢ finrank R M = 0 ↔ Subsingleton M
have this : Module.rank R M < ℵ₀
Tactic: have := Module.rank_lt_aleph0 R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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 : Free R M
inst_5 : Module.Finite R M
this : Module.rank R M < ℵ₀
⊢ finrank R M = 0 ↔ Subsingleton M
have this₁ : ¬ℵ₀ ≤ Module.rank R M
Tactic: rw [← not_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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 : Free R M
inst_5 : Module.Finite R M
⊢ 0 < finrank R M ↔ Nontrivial M
have rw : Subsingleton M ↔ ¬0 < finrank R M
Tactic: rw [← not_subsingleton_iff_nontrivial, ← iff_not_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (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
N : Submodule R M
⊢ (↑(finrank.{u, v} R ↥N) : Cardinal.{v}) = Module.rank R ↥N
have rw : Module.rank R ↥N < ℵ₀
Tactic: rw [finrank, Cardinal.cast_toNat_of_lt_aleph0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
S : Type u_2
inst_4 : CommSemiring S
inst_5 : Algebra S R
inst_6 : Module S M
inst_7 : IsScalarTower S R M
L L' : Submodule R M
inst_8 : Module.Finite.{u, v} R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ finrank.{u, v} R ↥L ≤ finrank.{u, v} R ↥L'
have refine : Module.rank R ↥L' < ℵ₀
Tactic: refine finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_isSMulRegular L L' hr h) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
S : Type u_2
inst_4 : CommSemiring S
inst_5 : Algebra S R
inst_6 : Module S M
inst_7 : IsScalarTower S R M
L L' : Submodule R M
inst_8 : Module.Finite.{u, v} R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ Module.rank R ↥L' < ℵ₀
have rw : (↑(finrank.{u, v} R ↥L') : Cardinal.{v}) < ℵ₀
Tactic: rw [← Module.finrank_eq_rank R L']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
S : Type u_1
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
inst_5 : Semiring S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : IsScalarTower R S S
inst_9 : FaithfulSMul R S
inst_10 : IsScalarTower R S M
⊢ finrank S M ≤ finrank R M
have rw : Module.rank S M ≤ Module.rank R M
Tactic: rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
S : Type u_1
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
inst_5 : Semiring S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : IsScalarTower R S S
inst_9 : FaithfulSMul R S
inst_10 : IsScalarTower R S M
rw : Module.rank S M ≤ Module.rank R M
⊢ finrank S M ≤ finrank R M
have hc : Module.rank S M < ℵ₀
Tactic: rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
S : Type u_1
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
inst_5 : Semiring S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : IsScalarTower R S S
inst_9 : FaithfulSMul R S
inst_10 : IsScalarTower R S M
rw : Module.rank S M ≤ Module.rank R M
hc : Module.rank S M < ℵ₀
⊢ finrank S M ≤ finrank R M
have hd : Module.rank R M < ℵ₀
Tactic: rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
        ¬Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
    ¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀
have push : (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
  ∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)
Tactic: push Not
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
    ∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)
have refine : (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) →
  ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R)
    (inj : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)),
    ℵ₀ ≤ Module.rank R (Fin n → R)
Tactic: refine ⟨fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩, fun ⟨n, le⟩ ↦
      ⟨n, le_rank_iff_exists_linearMap.mp (natCast_le_aleph0.trans le)⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h :
  ∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
have have : ∀ (g : (ℕ →₀ R) →ₗ[R] Fin n → R) (hg : Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑g : (a : ℕ →₀ R) → Fin n → R)),
  ℵ₀ ≤ Module.rank R (Fin n → R)
Tactic: have ⟨g, hg⟩ := f.exists_finsupp_nat_of_fin_fun_injective inj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h :
  ∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
g : (ℕ →₀ R) →ₗ[R] Fin n → R
hg : Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑g : (a : ℕ →₀ R) → Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
have h : Module.rank R (Fin n → R) = Cardinal.lift.{0, u} (Module.rank R (Fin n → R))
Tactic: convert! (Finsupp.basisSingleOne.linearIndependent.map_injOn _ hg.injOn).cardinal_lift_le_rank
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ StrongRankCondition R ↔ ∀ n > 0, 0 < finrank R (Fin n → R)
have rw : (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)
Tactic: rw [strongRankCondition_iff_forall_rank_lt_aleph0, ← not_iff_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)
have push : (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, finrank R (Fin n → R) ≤ 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, finrank R (Fin n → R) ≤ 0
have simp_rw : (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
Tactic: simp_rw [finrank, Nat.le_zero, toNat_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
have refine_1 : (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) →
  ∀ (n : ℕ) (le : ℵ₀ ≤ Module.rank R (Fin n → R)),
    Module.rank R (Fin (n + 1) → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin (n + 1) → R)
Tactic: refine ⟨fun ⟨n, le⟩ ↦ ⟨n + 1, n.succ_pos, ?_⟩, fun ⟨n, pos, eq⟩ ↦ ⟨n, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
refine_1 :
  (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) →
    ∀ (n : ℕ) (le : ℵ₀ ≤ Module.rank R (Fin n → R)),
      Module.rank R (Fin (n + 1) → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin (n + 1) → R)
⊢ (∃ (n : ℕ), ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
have refine_2 : (∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)) →
  ∀ (n : ℕ) (pos : n > 0) (eq : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)),
    ℵ₀ ≤ Module.rank R (Fin n → R)
Tactic: refine ⟨fun ⟨n, le⟩ ↦ ⟨n + 1, n.succ_pos, ?_⟩, fun ⟨n, pos, eq⟩ ↦ ⟨n, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
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 : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
have eq₁ : (∃ (f : R →ₗ[R] Fin n → R), Injective (α := R) (β := Fin n → R) (⇑f : (a : R) → Fin n → R)) →
  ℵ₀ ≤ Module.rank R (Fin n → R)
Tactic: rw [or_iff_not_imp_left, ← Ne, ← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at eq
Cleared hypotheses: eq