awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Module.rank R S = 1

Tactic:
rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_algebraMap h]

Premises used: Module.finrank_of_bijective_algebraMap, Module.rank_eq_one_iff_finrank_eq_one
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ #ι = (↑(finrank R R) : Cardinal.{u_2})

Tactic:
have : Cardinal.mk ι = ↑(Module.finrank R R) := (Module.mk_finrank_eq_card_basis b).symm
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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})
⊢ Subsingleton ι ∧ Nonempty ι

Tactic:
simpa [Cardinal.eq_one_iff_unique]

Premises used: Cardinal.eq_one_iff_unique
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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})
⊢ Subsingleton ι ∧ Nonempty ι

Tactic:
have : Subsingleton ι ∧ Nonempty ι := by simpa [Cardinal.eq_one_iff_unique]
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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_1 : #ι = (↑(finrank R R) : Cardinal.{u_2})
this : Subsingleton ι ∧ Nonempty ι
⊢ Unique ι

Tactic:
exact Nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 this)

Premises used: Iff.mpr, Nonempty.some, unique_iff_subsingleton_and_nonempty
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
simp : ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) < ℵ₀
⊢ Module.rank R M < ℵ₀

Tactic:
simp only [Module.rank_def]

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
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) < ℵ₀
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) < ℵ₀

Tactic:
obtain ⟨S, hS⟩ := Module.finite_def.mp ‹_›

Premises used: Module.finite_def, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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 : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) < ℵ₀

Tactic:
(ciSup_le' fun i => linearIndependent_le_span_finset _ i.prop S hS).trans_lt
    natCast_lt_aleph0

Premises used: linearIndependent_le_span_finset, ciSup_le', Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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 : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) < ℵ₀

Tactic:
exact (ciSup_le' fun i => linearIndependent_le_span_finset _ i.prop S hS).trans_lt
    natCast_lt_aleph0

Premises used: linearIndependent_le_span_finset, ciSup_le', Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
refine : #(↑(hs.extend (s := s) (t := t) hst) : Type u_3) < ℵ₀
⊢ Fintype (↑(hs.extend (s := s) (t := t) hst) : Type u_3)

Tactic:
refine Classical.choice (Cardinal.lt_aleph0_iff_fintype.1 ?_)

Premises used: Classical.choice, Iff.mp, Cardinal.lt_aleph0_iff_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
rw : Module.rank R ↥(span R t) < ℵ₀
⊢ #(↑(hs.extend (s := s) (t := t) hst) : Type u_3) < ℵ₀

Tactic:
rw [← rank_span_set (hs.linearIndepOn_extend hst), hs.span_extend_eq_span]

Premises used: rank_span_set, LinearIndepOn.span_extend_eq_span, LinearIndepOn.linearIndepOn_extend
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank R ↥(span R t) < ℵ₀

Tactic:
Module.rank_lt_aleph0 ..

Premises used: Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank R ↥(span R t) < ℵ₀

Tactic:
exact Module.rank_lt_aleph0 ..

Premises used: Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
rw₁ rw₂ : Module.rank R M = Module.rank R M
⊢ (↑(finrank R M) : Cardinal.{v}) = Module.rank R M

Tactic:
rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]

Premises used: Cardinal.cast_toNat_of_lt_aleph0, Module.rank_lt_aleph0, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank R M < ℵ₀

Tactic:
have := Module.rank_lt_aleph0 R M
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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 < ℵ₀
⊢ ¬ℵ₀ ≤ Module.rank R M

Tactic:
rw [← not_le] at this

Premises used: not_le
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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

Tactic:
simp [Module.finrank, this, Module.rank_zero_iff_of_free]

Premises used: Module.rank_zero_iff_of_free, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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 : Subsingleton M
⊢ finrank R M = 0

Tactic:
(finrank_eq_zero_iff_of_free R M).mpr inferInstance

Premises used: Iff.mpr, inferInstance, Module.finrank_eq_zero_iff_of_free
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
rw : Subsingleton M ↔ ¬0 < finrank R M
⊢ 0 < finrank R M ↔ Nontrivial M

Tactic:
rw [← not_subsingleton_iff_nontrivial, ← iff_not_comm]

Premises used: iff_not_comm, not_subsingleton_iff_nontrivial
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Subsingleton M ↔ ¬0 < finrank R M

Tactic:
simp [Module.finrank_eq_zero_iff_of_free]

Premises used: Module.finrank_eq_zero_iff_of_free
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
rw : Module.rank R ↥N < ℵ₀
⊢ (↑(finrank.{u, v} R ↥N) : Cardinal.{v}) = Module.rank R ↥N

Tactic:
rw [finrank, Cardinal.cast_toNat_of_lt_aleph0]

Premises used: Cardinal.cast_toNat_of_lt_aleph0, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank R ↥N < ℵ₀

Tactic:
lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)

Premises used: lt_of_le_of_lt, Submodule.rank_le, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank R ↥N < ℵ₀

Tactic:
exact lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)

Premises used: lt_of_le_of_lt, Submodule.rank_le, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
M' : Type u_2
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Module.Finite R M'
f : M →ₗ[R] M'
hf : Injective.{v + 1, u_2 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ finrank R M ≤ finrank R M'

Tactic:
finrank_le_finrank_of_rank_le_rank (lift_rank_le_of_injective _ hf) (rank_lt_aleph0 _ _)

Premises used: LinearMap.lift_rank_le_of_injective, Module.finrank_le_finrank_of_rank_le_rank, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
M' : Type u_2
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Module.Finite R M
f : M →ₗ[R] M'
hf : Surjective.{v + 1, u_2 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ finrank R M' ≤ finrank R M

Tactic:
finrank_le_finrank_of_rank_le_rank (lift_rank_le_of_surjective _ hf) (rank_lt_aleph0 _ _)

Premises used: LinearMap.lift_rank_le_of_surjective, Module.finrank_le_finrank_of_rank_le_rank, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
M' : Type u_2
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Module.Finite R M
f : M →ₗ[R] M'
⊢ finrank.{u, u_2} R ↥f.range ≤ finrank R M

Tactic:
finrank_le_finrank_of_rank_le_rank (lift_rank_range_le f) (rank_lt_aleph0 _ _)

Premises used: Module.finrank_le_finrank_of_rank_le_rank, lift_rank_range_le, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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'

Tactic:
finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_isSMulRegular L L' hr h) ?_

Premises used: Iff.mpr, Module.finrank_le_finrank_of_rank_le_rank, rank_le_of_isSMulRegular, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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'
refine : Module.rank R ↥L' < ℵ₀
⊢ finrank.{u, v} R ↥L ≤ finrank.{u, v} R ↥L'

Tactic:
refine finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_isSMulRegular L L' hr h) ?_

Premises used: Iff.mpr, Module.finrank_le_finrank_of_rank_le_rank, rank_le_of_isSMulRegular, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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'
rw : (↑(finrank.{u, v} R ↥L') : Cardinal.{v}) < ℵ₀
⊢ Module.rank R ↥L' < ℵ₀

Tactic:
rw [← Module.finrank_eq_rank R L']

Premises used: Membership.mem, Subtype, Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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') : Cardinal.{v}) < ℵ₀

Tactic:
natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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') : Cardinal.{v}) < ℵ₀

Tactic:
exact natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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 < ℵ₀
hd : Module.rank R M < ℵ₀
⊢ finrank S M ≤ finrank R M

Tactic:
rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]

Premises used: Cardinal.toNat_le_iff_le_of_lt_aleph0, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank S M ≤ Module.rank R M

Tactic:
rank_top_le_rank_of_isScalarTower R S M

Premises used: Module.rank_top_le_rank_of_isScalarTower
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank S M ≤ Module.rank R M

Tactic:
exact rank_top_le_rank_of_isScalarTower R S M

Premises used: Module.rank_top_le_rank_of_isScalarTower
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank S M < ℵ₀

Tactic:
lt_of_le_of_lt (rank_top_le_rank_of_isScalarTower R S M) (Module.rank_lt_aleph0 R M)

Premises used: lt_of_le_of_lt, Module.rank_top_le_rank_of_isScalarTower, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank S M < ℵ₀

Tactic:
exact lt_of_le_of_lt (rank_top_le_rank_of_isScalarTower R S M) (Module.rank_lt_aleph0 R M)

Premises used: lt_of_le_of_lt, Module.rank_top_le_rank_of_isScalarTower, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank R M < ℵ₀

Tactic:
Module.rank_lt_aleph0 _ _

Premises used: Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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
⊢ Module.rank R M < ℵ₀

Tactic:
exact Module.rank_lt_aleph0 _ _

Premises used: Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite R T
⊢ finrank R S ≤ finrank R T

Tactic:
finrank_le_finrank_of_rank_le_rank (lift_rank_bot_le_lift_rank_of_isScalarTower R S T)
    (Module.rank_lt_aleph0 _ _)

Premises used: Module.lift_rank_bot_le_lift_rank_of_isScalarTower, Module.finrank_le_finrank_of_rank_le_rank, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
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)
⊢ (¬∀ (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

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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)

Tactic:
⟨fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩, fun ⟨n, le⟩ ↦
      ⟨n, le_rank_iff_exists_linearMap.mp (natCast_le_aleph0.trans le)⟩⟩

Premises used: Module.le_rank_iff_exists_linearMap, _private.0.strongRankCondition_iff_forall_rank_lt_aleph0.match_2, Exists, Cardinal.aleph0, LE.le, Iff.intro, Exists.intro, Iff.mp, Function.Injective, LE.le.trans, Module.rank, DFunLike.coe, _private.0.strongRankCondition_iff_forall_rank_lt_aleph0.match_1, Cardinal.natCast_le_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
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)
⊢ (∃ (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:
refine ⟨fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩, fun ⟨n, le⟩ ↦
      ⟨n, le_rank_iff_exists_linearMap.mp (natCast_le_aleph0.trans le)⟩⟩
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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)
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)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
have ⟨g, hg⟩ := f.exists_finsupp_nat_of_fin_fun_injective inj
-- Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
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)
⊢ Cardinal.lift.{u, 0} #ℕ ≤ Cardinal.lift.{0, u} (Module.rank R (Fin n → R))

Tactic:
(Finsupp.basisSingleOne.linearIndependent.map_injOn _ hg.injOn).cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, Function.Injective.injOn, Finsupp.basisSingleOne, LinearIndependent.map_injOn, Module.Basis.linearIndependent