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)
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)
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
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : ℵ₀ < #↥L ^ Fintype.card ιL
h : ∀ (card_K : #↥L < ℵ₀), #↥L ^ Fintype.card ιL ≤ ℵ₀
⊢ ℵ₀ ≤ #↥L

Tactic:
contrapose! card_K
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank 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)
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
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : #↥L < ℵ₀
⊢ #↥L ^ Fintype.card ιL ≤ ℵ₀

Tactic:
(power_lt_aleph0 card_K natCast_lt_aleph0).le

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, Cardinal.power_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank 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)
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
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : #↥L < ℵ₀
⊢ #↥L ^ Fintype.card ιL ≤ ℵ₀

Tactic:
exact (power_lt_aleph0 card_K natCast_lt_aleph0).le

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, Cardinal.power_lt_aleph0
-- 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 : 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
⊢ ℵ₀ ≤ #ιL

Tactic:
have card_ιL : ℵ₀ ≤ #ιL := by
    contrapose! hLK
    haveI := @Fintype.ofFinite _ (lt_aleph0_iff_finite.mp hLK)
    rw [bL.repr.toEquiv.cardinal_eq, mk_finsupp_of_fintype,
        ← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢
    apply power_nat_le
    contrapose! card_K
    exact (power_lt_aleph0 card_K natCast_lt_aleph0).le
-- 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 : 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
inr : ∀ (e : ℕ ↪ ιL), False
⊢ False

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

Premises used: LE.le.trans_eq, Cardinal.mk, Cardinal.lift_uzero, Iff.mp, Cardinal.lift_mk_le', Eq.symm
-- 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 : 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
⊢ Eq (α := ℕ → K)
    ((Finsupp.linearCombination K (⇑bK : (a : ιK) → ℕ → K) : (a : ιK →₀ K) → ℕ → K)
        ((bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL)) :
          ιK →₀ K) :
      ℕ → K)
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL) : ℕ → K)

Tactic:
have rep_e := bK.linearCombination_repr (bL ∘ e)
-- 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 : 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
rep_e :
  Eq (α := ℕ → K)
    ((Finsupp.linearCombination K (⇑bK : (a : ιK) → ℕ → K) : (a : ιK →₀ K) → ℕ → K)
        ((bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL)) :
          ιK →₀ K) :
      ℕ → K)
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL) : ℕ → K)
⊢ Eq (α := ℕ → K)
    (∑
      a ∈
        Finsupp.support (M := K)
          ((bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))),
      HSMul.hSMul (α := K) (β := ℕ → K)
        ((((bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL)) :
                ιK →₀ K) :
              (a : ιK) → K)
            a :
          K)
        ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum] at rep_e

Premises used: Finsupp.sum, Finsupp.linearCombination_apply
-- 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 : 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
rep_e :
  Eq (α := ℕ → K)
    (∑
      a ∈
        Finsupp.support (M := K)
          ((bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))),
      HSMul.hSMul (α := K) (β := ℕ → K)
        ((((bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL)) :
                ιK →₀ K) :
              (a : ιK) → K)
            a :
          K)
        ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
⊢ let c : ιK →₀ K :=
    (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL));
  Eq (α := ℕ → K)
    (∑ a ∈ c.support, 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))

Tactic:
set c := bK.repr (bL ∘ e)

Premises used: Function.comp, Module.Basis.repr, 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 : 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ c.support, 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))
⊢ let s := c.support;
  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))

Tactic:
set s := c.support

Premises used: Finsupp.support
-- 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 : 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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) ⋯
h : LinearIndependent (↥L)ᵐᵒᵖ f
⊢ lift.{u, 0} #ℕ ≤ lift.{0, u} (Module.rank (↥L)ᵐᵒᵖ ((j : ↥s) → ↥L))

Tactic:
have := h.cardinal_lift_le_rank
-- 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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) ⋯
h : LinearIndependent (↥L)ᵐᵒᵖ f
this : lift.{u, 0} #ℕ ≤ lift.{0, u} (Module.rank (↥L)ᵐᵒᵖ ((j : ↥s) → ↥L))
⊢ lift.{u, 0} #ℕ ≤ (↑(Fintype.card.{u} ↥s) : Cardinal.{u})

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

Premises used: MulOpposite.opLinearEquiv, MulOpposite, Membership.mem, Subtype, LinearEquiv.piCongrRight, Cardinal.lift_uzero, LinearEquiv.rank_eq, rank_fun'
-- 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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) ⋯
h : LinearIndependent (↥L)ᵐᵒᵖ f
this : lift.{u, 0} #ℕ ≤ (↑(Fintype.card.{u} ↥s) : Cardinal.{u})
⊢ False

Tactic:
natCast_lt_aleph0.not_ge this

Premises used: Cardinal.natCast_lt_aleph0, LT.lt.not_ge
-- 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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) ⋯
h : LinearIndependent (↥L)ᵐᵒᵖ f
this : lift.{u, 0} #ℕ ≤ (↑(Fintype.card.{u} ↥s) : Cardinal.{u})
⊢ False

Tactic:
exact natCast_lt_aleph0.not_ge this

Premises used: Cardinal.natCast_lt_aleph0, LT.lt.not_ge
-- 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 : 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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) ⋯
⊢ ¬LinearIndependent (↥L)ᵐᵒᵖ f

Tactic:
have : ¬LinearIndependent Lᵐᵒᵖ f := fun h ↦ by
    have := h.cardinal_lift_le_rank
    rw [lift_uzero, (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Lᵐᵒᵖ).rank_eq,
        rank_fun'] at this
    exact natCast_lt_aleph0.not_ge this
-- 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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
inr :
  ∀ (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), False
⊢ False

Tactic:
obtain ⟨t, g, eq0, i, hi, hgi⟩ := not_linearIndependent_iff.mp this

Premises used: Iff.mp, not_linearIndependent_iff
-- 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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
⊢ False

Tactic:
hgi (linearIndependent_iff'.mp (bL.linearIndependent.comp e e.injective) t g ?_ i hi)

Premises used: linearIndependent_iff', Module.Basis.linearIndependent, Iff.mp, Function.Embedding.injective, DFunLike.coe, LinearIndependent.comp
-- 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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.{u + 1} (α := K)
    (∑ i ∈ t, HSMul.hSMul (β := K) (g i) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL) i)) 0
⊢ False

Tactic:
refine hgi (linearIndependent_iff'.mp (bL.linearIndependent.comp e e.injective) t g ?_ i hi)

Premises used: linearIndependent_iff', Module.Basis.linearIndependent, Iff.mp, Function.Embedding.injective, DFunLike.coe, LinearIndependent.comp
-- 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 := (bK.repr : (a : ℕ → K) → ιK →₀ K) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
s : Finset ιK := c.support
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 :
  ∀ (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))),
    let 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.{u + 1} (α := K)
        (∑ i ∈ t, HSMul.hSMul (β := K) (g i) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL) i)) 0
⊢ Eq.{u + 1} (α := K)
    (∑ i ∈ t, HSMul.hSMul (β := K) (g i) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL) i)) 0

Tactic:
clear_value c s
-- 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.{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
⊢ Eq.{u + 1} (α := K)
    (∑ i ∈ t, HSMul.hSMul (β := K) (g i) (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL) i)) 0

Tactic:
simp_rw [← rep_e, Finset.sum_apply, Pi.smul_apply, Finset.smul_sum]

Premises used: Finset.sum_apply, Finset.smul_sum, Pi.smul_apply