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

Proof state:
K : Type u
inst✝ : DivisionRing K
⊢ Function.Injective ⇑Finsupp.lcoeFun

Tactic:
exact DFunLike.coe_injective

Result:
no goals

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} #ℕ ≤ lift.{0, u} (Module.rank (↥L)ᵐᵒᵖ ({ x // x ∈ s } → ↥L))
⊢ False

Tactic:
rw [lift_uzero, (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Lᵐᵒᵖ).rank_eq,
    rank_fun'] at this

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)
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

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
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, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : ∑ i ∈ t, g i • f i = 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
⊢ ∑ i ∈ t, g i • (⇑bL ∘ ⇑e) i = 0

Tactic:
clear_value c s

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
eq0 : ∑ i ∈ t, g i • f i = 0
c : ιK →₀ K
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
⊢ ∑ i ∈ t, g i • (⇑bL ∘ ⇑e) i = 0

Proof state:
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

Tactic:
have rep_e := bK.linearCombination_repr (bL ∘ e)

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
rep_e : (Finsupp.linearCombination K ⇑bK) (bK.repr (⇑bL ∘ ⇑e)) = ⇑bL ∘ ⇑e
⊢ False

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 ^ Fintype.card ιL
⊢ ℵ₀ ≤ #↥L

Tactic:
contrapose! card_K

Result:
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 ≤ ℵ₀

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
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, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : ∑ i ∈ t, g i • f i = 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
⊢ False

Tactic:
refine hgi (linearIndependent_iff'.mp (bL.linearIndependent.comp e e.injective) t g ?_ 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
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, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : ∑ i ∈ t, g i • f i = 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
⊢ ∑ i ∈ t, g i • (⇑bL ∘ ⇑e) i = 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)
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
⊢ #K ≤ #↥L

Tactic:
rw [bL.repr.toEquiv.cardinal_eq, mk_finsupp_of_fintype,
    ← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢

Result:
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 ^ Fintype.card ιL
⊢ #↥L ^ Fintype.card ιL ≤ #↥L