-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem rank_fun_infinite {ι : Type v} [hι : Infinite ι] : Module.rank K (ι → K) = #(ι → K)

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Infinite ιK

Tactic:
rw [← aleph0_le_mk_iff, bK.mk_eq_rank'']

Result:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K)

Proof state:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
have key := (lift_le.{v}.mpr <| max_aleph0_card_le_rank_fun_nat K).trans this

Result:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : lift.{v, u} (ℵ₀ ⊔ #K) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Proof state:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : lift.{v, u} (ℵ₀ ⊔ #K) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
rw [lift_max, lift_aleph0, max_le_iff] at key

Result:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Proof state:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ lift.{v, u} #K ≤ Module.rank K (ι → K)

Tactic:
exact key.2

Result:
no goals

Proof state:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
have := LinearMap.lift_rank_le_of_injective _ <|
  LinearMap.funLeft_injective_of_surjective K K _ (invFun_surjective e.injective)

Result:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))
⊢ Module.rank K (ι → K) = #(ι → K)

Proof state:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
haveI : Infinite ιK := by
  rw [← aleph0_le_mk_iff, bK.mk_eq_rank'']; exact key.1

Result:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = #(ι → K)

Proof state:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
rw [lift_umax.{u,v}, lift_id'.{u,v}] at this

Result:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K)

Tactic:
exact key.1

Result:
no goals

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ι → K)

Result:
case intro.mk
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Proof state:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
rw [bK.repr.toEquiv.cardinal_eq, mk_finsupp_lift_of_infinite,
    lift_umax.{u,v}, lift_id'.{u,v}, bK.mk_eq_rank'', eq_comm, max_eq_left]

Result:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ lift.{v, u} #K ≤ Module.rank K (ι → K)

Proof state:
case intro.mk
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
obtain ⟨e⟩ := lift_mk_le'.mp ((aleph0_le_mk_iff.mpr hι).trans_eq (lift_uzero #ι).symm)

Result:
case intro.mk.intro
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Basis ιK K (ι → K)
e : ℕ ↪ ι
⊢ Module.rank K (ι → K) = #(ι → K)