-- Mathlib/LinearAlgebra/FreeAlgebra.lean
theorem Algebra.rank_adjoin_le {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S]
    (s : Set S) : Module.rank R (adjoin R s) ≤ max #s ℵ₀

Proof state:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{v, max u v} (Module.rank R (FreeAlgebra R { x // x ∈ s })) ≤ lift.{max u v, v} (#↑s ⊔ ℵ₀)

Tactic:
rw [FreeAlgebra.rank_eq, lift_id'.{v,u}, lift_umax.{v,u}, lift_le, max_comm]

Result:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ ℵ₀ ⊔ #↑s

Proof state:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ #↑s ⊔ ℵ₀

Tactic:
rw [← lift_le.{max u v}]

Result:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{max u v, v} (Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range) ≤ lift.{max u v, v} (#↑s ⊔ ℵ₀)

Proof state:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ #↑s ⊔ ℵ₀

Tactic:
rw [rank_subsingleton]

Result:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ 1 ≤ #↑s ⊔ ℵ₀

Proof state:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ ℵ₀ ⊔ #↑s

Tactic:
exact mk_list_le_max _

Result:
no goals

Proof state:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{max u v, v} (Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range) ≤ lift.{max u v, v} (#↑s ⊔ ℵ₀)

Tactic:
refine (lift_rank_range_le (FreeAlgebra.lift R ((↑) : s → S)).toLinearMap).trans ?_

Result:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{v, max u v} (Module.rank R (FreeAlgebra R { x // x ∈ s })) ≤ lift.{max u v, v} (#↑s ⊔ ℵ₀)

Proof state:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ 1 ≤ #↑s ⊔ ℵ₀

Tactic:
exact one_le_aleph0.trans (le_max_right _ _)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
⊢ Module.rank R ↥(adjoin R s) ≤ #↑s ⊔ ℵ₀

Tactic:
rw [adjoin_eq_range_freeAlgebra_lift]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ #↑s ⊔ ℵ₀

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ #↑s ⊔ ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ #↑s ⊔ ℵ₀

case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ #↑s ⊔ ℵ₀