awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
rw :
  max (Cardinal.lift.{max u w, v} #↥(Algebra.adjoin R (Set.range v))) (Cardinal.lift.{max u w, v} ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
rw₁ :
  max (Cardinal.lift.{max v u w, max u w} #(MvPolynomial ι R)) (Cardinal.lift.{max u w, v} ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
rw₂ :
  max (Cardinal.lift.{max v u w, max u w} #(MvPolynomial ι R)) ℵ₀ =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
rw₃ :
  max (Cardinal.lift.{max v u w, max u w} #(MvPolynomial ι R)) (Cardinal.lift.{max u v w, max u w} ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
rw₄ :
  Cardinal.lift.{max (max u v) w, max u w} (max #(MvPolynomial ι R) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
rw₅ rw₆ :
  Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀) = Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
⊢ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)

Tactic:
rw [lift_max, ← Cardinal.lift_mk_eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩, lift_aleph0,
        ← lift_aleph0.{max u v w, max u w}, ← lift_max, lift_umax.{max u w, v}]

Premises used: Iff.mpr, AlgebraicIndependent.aevalEquiv, Cardinal.lift_mk_eq, Nonempty.intro, And.left, Cardinal.lift_aleph0, AlgEquiv.toEquiv, Cardinal.lift_max
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{v, max u w} (max (max (max (Cardinal.lift.{w, u} #R) (Cardinal.lift.{u, w} #ι)) ℵ₀) ℵ₀) =
    max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
inst : CommRing R
K' : Type u
inst_1 : Field K'
inst_2 : Algebra R K'
inst_3 : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
hv : IsTranscendenceBasis R v'
⊢ #K' ≤ max (max #R #ι') ℵ₀

Tactic:
simpa using cardinal_le_max_transcendence_basis v' hv

Premises used: IsAlgClosed.cardinal_le_max_transcendence_basis
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ ℵ₀ < Cardinal.lift.{max u w, v} #K

Tactic:
simpa
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ Cardinal.lift.{max v w, u} #R ≤ ℵ₀

Tactic:
simpa
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ Cardinal.lift.{max u v, w} #ι ≤ ℵ₀

Tactic:
simpa using le_of_lt h

Premises used: le_of_lt
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
rw : Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι
rw₁ : ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)
⊢ max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀ = Cardinal.lift.{max u v, w} #ι

Tactic:
rw [max_eq_left, max_eq_right]

Premises used: max_eq_left, max_eq_right
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ ℵ₀

Tactic:
simpa using hR
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι

Tactic:
exact le_trans (by simpa using hR) this

Premises used: le_trans
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)

Tactic:
le_max_of_le_right this

Premises used: le_max_of_le_right
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)

Tactic:
exact le_max_of_le_right this

Premises used: le_max_of_le_right
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
K : Type v
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsAlgClosed K
ι : Type w
v : ι → K
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this_1 : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
this : Cardinal.lift.{max u w, v} #K = Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{u, max v w} (Cardinal.lift.{w, v} #K) = Cardinal.lift.{u, max v w} (Cardinal.lift.{v, w} #ι)

Tactic:
simpa
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u
inst : CommRing R
K' : Type u
inst_1 : Field K'
inst_2 : Algebra R K'
inst_3 : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
inst_4 : Nontrivial R
hv : IsTranscendenceBasis R v'
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K'
⊢ #K' = #ι'

Tactic:
simpa using cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt v' hv hR hK

Premises used: IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
obtain :
  ∀ (s : Set K)
    (hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))),
    Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨s, hs⟩ := exists_isTranscendenceBasis ℤ K

Premises used: exists_isTranscendenceBasis, Int
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
obtain :
  ∀ (t : Set L)
    (ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))),
    Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨t, ht⟩ := exists_isTranscendenceBasis ℤ L

Premises used: exists_isTranscendenceBasis, Int
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
rwa : ℵ₀ < Cardinal.lift.{u, v} #L
rwa₁ : ℵ₀ < Cardinal.lift.{v, u} #K
rwa₂ rwa₃ rwa₄ rwa₅ : ℵ₀ < #K
⊢ ℵ₀ < #L

Tactic:
rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]

Premises used: Iff.mpr, Cardinal.lift_mk_eq', Cardinal.aleph0_lt_lift
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
⊢ ℵ₀ < #L

Tactic:
have hL : ℵ₀ < #L := by
    rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
rw : Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L
⊢ Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)

Tactic:
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_eq mk_int) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_eq mk_int) hL)]

Premises used: IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt, le_of_eq, Cardinal.mk_int, Cardinal.lift_injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L

Tactic:
Cardinal.lift_mk_eq'.2 hKL

Premises used: Iff.mpr, Cardinal.lift_mk_eq'
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L

Tactic:
exact Cardinal.lift_mk_eq'.2 hKL

Premises used: Iff.mpr, Cardinal.lift_mk_eq'
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)

Tactic:
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
    rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_eq mk_int) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_eq mk_int) hL)]
    exact Cardinal.lift_mk_eq'.2 hKL
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
obtain : ∀ (e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)), Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨e⟩ := Cardinal.lift_mk_eq'.1 this

Premises used: Cardinal.lift_mk_eq', Iff.mp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
⊢ Nonempty (K ≃+* L)

Tactic:
⟨equivOfTranscendenceBasis _ _ e hs ht⟩

Premises used: IsAlgClosed.equivOfTranscendenceBasis, Nonempty.intro
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
⊢ Nonempty (K ≃+* L)

Tactic:
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
obtain :
  ∀ (s : Set K)
    (hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))),
    Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨s, hs⟩ := exists_isTranscendenceBasis (ZMod p) K

Premises used: exists_isTranscendenceBasis, ZMod
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
obtain :
  ∀ (t : Set L)
    (ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))),
    Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨t, ht⟩ := exists_isTranscendenceBasis (ZMod p) L

Premises used: exists_isTranscendenceBasis, ZMod
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
rwa : ℵ₀ < Cardinal.lift.{u, v} #L
rwa₁ : ℵ₀ < Cardinal.lift.{v, u} #K
rwa₂ rwa₃ rwa₄ rwa₅ : ℵ₀ < #K
⊢ ℵ₀ < #L

Tactic:
rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]

Premises used: Iff.mpr, Cardinal.lift_mk_eq', Cardinal.aleph0_lt_lift
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
⊢ ℵ₀ < #L

Tactic:
have hL : ℵ₀ < #L := by
    rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
rw : Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L
⊢ Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)

Tactic:
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_lt (lt_aleph0_of_finite _)) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_lt (lt_aleph0_of_finite _)) hL)]

Premises used: IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt, le_of_lt, Cardinal.lt_aleph0_of_finite, Cardinal.lift_injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L

Tactic:
Cardinal.lift_mk_eq'.2 hKL

Premises used: Iff.mpr, Cardinal.lift_mk_eq'
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L

Tactic:
exact Cardinal.lift_mk_eq'.2 hKL

Premises used: Iff.mpr, Cardinal.lift_mk_eq'
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)

Tactic:
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
    rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_lt (lt_aleph0_of_finite _)) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_lt (lt_aleph0_of_finite _)) hL)]
    exact Cardinal.lift_mk_eq'.2 hKL
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this_2 : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
obtain : ∀ (e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)), Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨e⟩ := Cardinal.lift_mk_eq'.1 this

Premises used: Cardinal.lift_mk_eq', Iff.mp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this_2 : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
⊢ Nonempty (K ≃+* L)

Tactic:
⟨equivOfTranscendenceBasis _ _ e hs ht⟩

Premises used: IsAlgClosed.equivOfTranscendenceBasis, Nonempty.intro
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this_2 : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
⊢ Nonempty (K ≃+* L)

Tactic:
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩