-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem max_aleph0_card_le_rank_fun_nat : max ℵ₀ #K ≤ Module.rank K (ℕ → K)

Proof state:
case inr.intro.mk
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
⊢ False

Tactic:
let L := Subfield.closure (Set.range (fun i : ιK × ℕ ↦ bK i.1 i.2))

Result:
case inr.intro.mk
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
⊢ False

Proof state:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
⊢ #↥L < #K

Tactic:
refine (Subfield.cardinalMk_closure_le_max _).trans_lt
  (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)

Result:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
⊢ #(ιK × ℕ) < #K

Proof state:
case inr.intro.mk.intro.mk
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
⊢ False

Tactic:
obtain ⟨e⟩ := lift_mk_le'.mp (card_ιL.trans_eq (lift_uzero #ιL).symm)

Result:
case inr.intro.mk.intro.mk.intro
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
⊢ False

Proof state:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
⊢ False

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

Result:
case inr.intro.mk
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
⊢ False

Proof state:
case inr.intro.mk.intro.mk.intro.intro.intro.intro.intro.intro
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i✝ : ℕ
hi✝ : i✝ ∈ t
hgi : g i✝ ≠ 0
s : Finset ιK
f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
eq0 : ∑ i ∈ t, g i • f i = 0
c : ιK →₀ K
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
i : ιK
hi : i ∈ s
⊢ ∑ x ∈ t, g x • c i • bK i x = 0

Tactic:
replace eq0 := congr_arg L.subtype (congr_fun eq0 ⟨i, hi⟩)

Result:
case inr.intro.mk.intro.mk.intro.intro.intro.intro.intro.intro
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i✝ : ℕ
hi✝ : i✝ ∈ t
hgi : g i✝ ≠ 0
s : Finset ιK
f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
c : ιK →₀ K
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
i : ιK
hi : i ∈ s
eq0 : L.subtype ((∑ i ∈ t, g i • f i) ⟨i, hi⟩) = L.subtype (0 ⟨i, hi⟩)
⊢ ∑ x ∈ t, g x • c i • bK i x = 0

Proof state:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
s : Finset ιK := c.support
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩
h : LinearIndependent (↥L)ᵐᵒᵖ f
this : lift.{u, 0} #ℕ ≤ ↑(Fintype.card { x // x ∈ s })
⊢ False

Tactic:
exact (nat_lt_aleph0 _).not_le this

Result:
no goals

Proof state:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
⊢ ℵ₀ ⊔ #K ≤ Module.rank K (ℕ → K)

Tactic:
refine max_le aleph0_le ?_

Result:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
⊢ #K ≤ Module.rank K (ℕ → K)

Proof state:
case h
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : #↥L < ℵ₀
⊢ #↥L ^ Fintype.card ιL ≤ ℵ₀

Tactic:
exact (power_lt_aleph0 card_K <| nat_lt_aleph0 _).le

Result:
no goals

Proof state:
case inr.intro.mk.intro.mk.intro.intro.intro.intro.intro.intro
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i✝ : ℕ
hi✝ : i✝ ∈ t
hgi : g i✝ ≠ 0
s : Finset ιK
f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
c : ιK →₀ K
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
i : ιK
hi : i ∈ s
eq0 : L.subtype ((∑ i ∈ t, g i • f i) ⟨i, hi⟩) = L.subtype (0 ⟨i, hi⟩)
⊢ ∑ x ∈ t, g x • c i • bK i x = 0

Tactic:
rw [Finset.sum_apply, map_sum] at eq0

Result:
case inr.intro.mk.intro.mk.intro.intro.intro.intro.intro.intro
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i => bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i✝ : ℕ
hi✝ : i✝ ∈ t
hgi : g i✝ ≠ 0
s : Finset ιK
f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
c : ιK →₀ K
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
i : ιK
hi : i ∈ s
eq0 : ∑ x ∈ t, L.subtype ((g x • f x) ⟨i, hi⟩) = L.subtype (0 ⟨i, hi⟩)
⊢ ∑ x ∈ t, g x • c i • bK i x = 0

Proof state:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
⊢ #K ≤ Module.rank K (ℕ → K)

Tactic:
by_contra!

Result:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
⊢ False