awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : Eq.{u + 1} (α := (j : ↥s) → ↥L) (∑ i ∈ t, g i • f i) 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
inr :
  Eq (α := K)
    (∑ y ∈ s, ∑ x ∈ t, g x • HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) y : K) ((bK : (a : ιK) → ℕ → K) y x : K))
    0
⊢ Eq.{u + 1} (α := K)
    (∑ x ∈ t,
      ∑ x_1 ∈ s, g x • HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) x_1 : K) ((bK : (a : ιK) → ℕ → K) x_1 x : K))
    0

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : Eq.{u + 1} (α := (j : ↥s) → ↥L) (∑ i ∈ t, g i • f i) 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
⊢ Eq (α := K)
    (∑ y ∈ s, ∑ x ∈ t, g x • HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) y : K) ((bK : (a : ιK) → ℕ → K) y x : K))
    0

Tactic:
Finset.sum_eq_zero fun i hi ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : Eq.{u + 1} (α := (j : ↥s) → ↥L) (∑ i ∈ t, g i • f i) 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
inr :
  ∀ (i : ιK) (hi : i ∈ s),
    Eq.{u + 1} (α := K)
      (∑ x ∈ t, g x • HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K) ((bK : (a : ιK) → ℕ → K) i x : K)) 0
⊢ Eq (α := K)
    (∑ y ∈ s, ∑ x ∈ t, g x • HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) y : K) ((bK : (a : ιK) → ℕ → K) y x : K))
    0

Tactic:
refine Finset.sum_eq_zero fun i hi ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : Eq.{u + 1} (α := (j : ↥s) → ↥L) (∑ i ∈ t, g i • f i) 0
i_1 : ℕ
hi_1 : i_1 ∈ t
hgi : g i_1 ≠ 0
i : ιK
hi : i ∈ s
⊢ Eq (α := K) ((L.subtype : (a : ↥L) → K) ((∑ i ∈ t, g i • f i) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)

Tactic:
replace eq0 := congr_arg L.subtype (congr_fun eq0 ⟨i, hi⟩)
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i_1 : ℕ
hi_1 : i_1 ∈ t
hgi : g i_1 ≠ 0
i : ιK
hi : i ∈ s
eq0 :
  Eq (α := K) ((L.subtype : (a : ↥L) → K) ((∑ i ∈ t, g i • f i) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
⊢ Eq (α := K) (∑ x ∈ t, (L.subtype : (a : ↥L) → K) ((g x • f x) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)

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

Premises used: Finset.sum_apply, map_sum
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i_1 : ℕ
hi_1 : i_1 ∈ t
hgi : g i_1 ≠ 0
i : ιK
hi : i ∈ s
eq0 :
  Eq (α := K) (∑ x ∈ t, (L.subtype : (a : ↥L) → K) ((g x • f x) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
⊢ SMulCommClass (↥L)ᵐᵒᵖ K K

Tactic:
have : SMulCommClass Lᵐᵒᵖ K K := ⟨fun _ _ _ ↦ mul_assoc _ _ _⟩
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this_3 : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i_1 : ℕ
hi_1 : i_1 ∈ t
hgi : g i_1 ≠ 0
i : ιK
hi : i ∈ s
eq0 :
  Eq (α := K) (∑ x ∈ t, (L.subtype : (a : ↥L) → K) ((g x • f x) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
this : SMulCommClass (↥L)ᵐᵒᵖ K K
inr :
  HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K)
      (∑ x ∈ t, HSMul.hSMul (β := K) (g x) ((bK : (a : ιK) → ℕ → K) i x : K)) =
    0
⊢ Eq.{u + 1} (α := K)
    (∑ x ∈ t, g x • HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K) ((bK : (a : ιK) → ℕ → K) i x : K)) 0

Tactic:
simp_rw [smul_comm _ (c i), ← Finset.smul_sum]

Premises used: Finset.smul_sum, SMulCommClass.smul_comm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this_3 : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i_1 : ℕ
hi_1 : i_1 ∈ t
hgi : g i_1 ≠ 0
i : ιK
hi : i ∈ s
eq0 :
  Eq (α := K) (∑ x ∈ t, (L.subtype : (a : ↥L) → K) ((g x • f x) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
this : SMulCommClass (↥L)ᵐᵒᵖ K K
inr :
  HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K)
      ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K) =
    0
inr₁ inr₂ : Eq.{u + 1} (α := K) 0 0
⊢ HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K)
      (∑ x ∈ t, HSMul.hSMul (β := K) (g x) ((bK : (a : ιK) → ℕ → K) i x : K)) =
    0

Tactic:
erw [eq0, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
obtain : ∀ (ιK : Type (max u v)) (bK : Module.Basis ιK K (ι → K)), Module.rank K (ι → K) = #(ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

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

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
obtain : ∀ (e : ℕ ↪ ι), Module.rank 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)

Premises used: Iff.mpr, LE.le.trans_eq, Cardinal.mk, Cardinal.aleph0_le_mk_iff, Cardinal.lift_uzero, Iff.mp, Cardinal.lift_mk_le', Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
⊢ lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))

Tactic:
have := LinearMap.lift_rank_le_of_injective _ <|
    LinearMap.funLeft_injective_of_surjective K K _ (invFun_surjective e.injective)
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))
⊢ lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)

Tactic:
rw [lift_umax.{u, v}, lift_id'.{u, v}] at this
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
⊢ lift.{v, u} (max ℵ₀ #K) ≤ Module.rank K (ι → K)

Tactic:
have key := (lift_le.{v}.mpr <| max_aleph0_card_le_rank_fun_nat K).trans this
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : lift.{v, u} (max ℵ₀ #K) ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)

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

Premises used: max_le_iff, Cardinal.lift_aleph0, Cardinal.lift_max
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.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)
rw : ℵ₀ ≤ Module.rank K (ι → K)
⊢ Infinite ιK

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

Premises used: Cardinal.aleph0_le_mk_iff, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.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:
key.1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.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

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.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:
haveI : Infinite ιK := by
    rw [← aleph0_le_mk_iff, bK.mk_eq_rank'']; exact key.1
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this_1 : 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
rw : lift.{v, u} #K ≤ Module.rank K (ι → 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]

Premises used: Cardinal.mk_finsupp_lift_of_infinite, max_eq_left, Module.Basis.repr, eq_comm, LinearEquiv.toEquiv, Module.Basis.mk_eq_rank'', Equiv.cardinal_eq
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this_1 : 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:
key.2

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this_1 : 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

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
obtain : ∀ (ι : Type u_1) (b : Module.Basis ι K V), Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

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

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_1
b : Module.Basis ι K V
rw : ∀ (h : Infinite ι) (b : Module.Basis ι K V), Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h

Premises used: Cardinal.aleph0_le_mk_iff, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
have : ∀ (e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] (i : ι) → Kᵐᵒᵖ), Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
have e := (b.constr Kᵐᵒᵖ (M' := K)).symm.trans
    (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Kᵐᵒᵖ)
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] (i : ι) → Kᵐᵒᵖ
rw : Module.rank Kᵐᵒᵖ ((i : ι) → Kᵐᵒᵖ) = #((i : ι) → Kᵐᵒᵖ)
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [e.rank_eq, e.toEquiv.cardinal_eq]

Premises used: LinearEquiv.rank_eq, LinearEquiv.toEquiv, Equiv.cardinal_eq
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] (i : ι) → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ ((i : ι) → Kᵐᵒᵖ) = #((i : ι) → Kᵐᵒᵖ)

Tactic:
apply rank_fun_infinite

Premises used: rank_fun_infinite
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
obtain : ∀ (ι : Type u_2) (b : Module.Basis ι K V), Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

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

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_2
b : Module.Basis ι K V
rw : ∀ (h : Infinite ι) (b : Module.Basis ι K V), Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h

Premises used: Cardinal.aleph0_le_mk_iff, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
have : ∀ (e : (V →ₗ[K] K) ≃ₗ[K] ι → K), Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
have e := (b.constr K (M' := K)).symm
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
rw : Module.rank K (ι → K) = #(ι → K)
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [e.rank_eq, e.toEquiv.cardinal_eq]

Premises used: LinearEquiv.rank_eq, LinearEquiv.toEquiv, Equiv.cardinal_eq
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
apply rank_fun_infinite

Premises used: rank_fun_infinite
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
obtain : ∀ (ι : Type v) (b : Module.Basis ι K V), lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

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

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
rw : lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
rw [← b.mk_eq_rank'', rank_dual_eq_card_dual_of_aleph0_le_rank' h,
      ← (b.constr ℕ (M' := K)).toEquiv.cardinal_eq, mk_arrow]

Premises used: rank_dual_eq_card_dual_of_aleph0_le_rank', Cardinal.mk_arrow, Nat, LinearEquiv.toEquiv, Module.Basis.mk_eq_rank'', Equiv.cardinal_eq, Module.Basis.constr
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
hb : 1 < lift.{v, u} #K
⊢ lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι

Tactic:
apply cantor'

Premises used: Cardinal.cantor'
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
hb : Nontrivial K
⊢ 1 < lift.{v, u} #K

Tactic:
rw [one_lt_lift_iff, one_lt_iff_nontrivial]

Premises used: Cardinal.one_lt_iff_nontrivial, Cardinal.one_lt_lift_iff
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ Nontrivial K

Tactic:
infer_instance