awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) (0 : K[X])
hdg : HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) →
    ∀ (a : K), rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
have neg : ∀ (a : K),
  (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
Tactic: refine forall_imp fun a => ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) (0 : K[X])
hdg : HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g ≠ 0
a : K
⊢ (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
have pos : ∀ (haf : eval a f = 0),
  (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
Tactic: by_cases haf : f.eval a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) (0 : K[X])
hdg : HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g ≠ 0
a : K
pos :
  ∀ (haf : eval a f = 0),
    (f.IsRoot a → g.IsRoot a) →
      rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
⊢ (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
have neg : ∀ (haf : ¬eval a f = 0),
  (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
Tactic: by_cases haf : f.eval a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) (0 : K[X])
hdg : HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g ≠ 0
a : K
haf : eval a f = 0
⊢ (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
have h0 : 0 < rootMultiplicity a f
Tactic: have h0 : 0 < f.rootMultiplicity a := (rootMultiplicity_pos hf0).2 haf
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) (0 : K[X])
hdg : HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
⊢ (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
have pos : (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g
Tactic: rw [derivative_rootMultiplicity_of_root haf]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
R : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : Field L
inst_4 : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv_1 : AlgebraicIndependent R v
hw_1 : AlgebraicIndependent R w
inst_5 : IsAlgClosed K
inst_6 : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this_1 : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := ⋯
⊢ RingEquiv.{u_3, u_2} ↥(Algebra.adjoin R (Set.range v)) ↥(Algebra.adjoin R (Set.range w))
have refine : MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))
Tactic: refine hv.1.aevalEquiv.symm.toRingEquiv.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
R : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : Field L
inst_4 : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv_1 : AlgebraicIndependent R v
hw_1 : AlgebraicIndependent R w
inst_5 : IsAlgClosed K
inst_6 : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this_1 : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := ⋯
⊢ MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))
have refine_1 : Eq (α := MvPolynomial κ R →ₐ[R] MvPolynomial κ R)
  (AlgHom.comp (B := MvPolynomial ι R) (MvPolynomial.rename (⇑e : (a : ι) → κ))
    (MvPolynomial.rename (⇑e.symm : (a : κ) → ι)))
  (AlgHom.id R (MvPolynomial κ R))
Tactic: refine (AlgEquiv.ofAlgHom (MvPolynomial.rename e)
      (MvPolynomial.rename e.symm) ?_ ?_).toRingEquiv.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
R : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : Field L
inst_4 : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv_1 : AlgebraicIndependent R v
hw_1 : AlgebraicIndependent R w
inst_5 : IsAlgClosed K
inst_6 : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this_1 : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := ⋯
refine_1 :
  Eq (α := MvPolynomial κ R →ₐ[R] MvPolynomial κ R)
    (AlgHom.comp (B := MvPolynomial ι R) (MvPolynomial.rename (⇑e : (a : ι) → κ))
      (MvPolynomial.rename (⇑e.symm : (a : κ) → ι)))
    (AlgHom.id R (MvPolynomial κ R))
⊢ MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))
have refine_2 : Eq (α := MvPolynomial ι R →ₐ[R] MvPolynomial ι R)
  (AlgHom.comp (B := MvPolynomial κ R) (MvPolynomial.rename (⇑e.symm : (a : κ) → ι))
    (MvPolynomial.rename (⇑e : (a : ι) → κ)))
  (AlgHom.id R (MvPolynomial ι R))
Tactic: refine (AlgEquiv.ofAlgHom (MvPolynomial.rename e)
      (MvPolynomial.rename e.symm) ?_ ?_).toRingEquiv.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
R : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : Field L
inst_4 : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv_1 : AlgebraicIndependent R v
hw_1 : AlgebraicIndependent R w
inst_5 : IsAlgClosed K
inst_6 : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this_1 : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := ⋯
refine_1 :
  Eq (α := MvPolynomial κ R →ₐ[R] MvPolynomial κ R)
    (AlgHom.comp (B := MvPolynomial ι R) (MvPolynomial.rename (⇑e : (a : ι) → κ))
      (MvPolynomial.rename (⇑e.symm : (a : κ) → ι)))
    (AlgHom.id R (MvPolynomial κ R))
refine_2 :
  Eq (α := MvPolynomial ι R →ₐ[R] MvPolynomial ι R)
    (AlgHom.comp (B := MvPolynomial κ R) (MvPolynomial.rename (⇑e.symm : (a : κ) → ι))
      (MvPolynomial.rename (⇑e : (a : ι) → κ)))
    (AlgHom.id R (MvPolynomial ι R))
⊢ MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))
have refine_3 : MvPolynomial κ R ≃+* ↥(Algebra.adjoin R (Set.range w))
Tactic: refine (AlgEquiv.ofAlgHom (MvPolynomial.rename e)
      (MvPolynomial.rename e.symm) ?_ ?_).toRingEquiv.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
R : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : Field L
inst_4 : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv_1 : AlgebraicIndependent R v
hw_1 : AlgebraicIndependent R w
inst_5 : IsAlgClosed K
inst_6 : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this_1 : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := ⋯
⊢ Eq (α := MvPolynomial κ R →ₐ[R] MvPolynomial κ R)
    (AlgHom.comp (B := MvPolynomial ι R) (MvPolynomial.rename (⇑e : (a : ι) → κ))
      (MvPolynomial.rename (⇑e.symm : (a : κ) → ι)))
    (AlgHom.id R (MvPolynomial κ R))
have refine_1 : ∀ (i : κ) (m : κ →₀ ℕ),
  Eq.{u_1 + 1} (α := R)
    (MvPolynomial.coeff m
      ((AlgHom.comp (B := MvPolynomial ι R) (MvPolynomial.rename (⇑e : (a : ι) → κ))
            (MvPolynomial.rename (⇑e.symm : (a : κ) → ι)) :
          (a : MvPolynomial κ R) → MvPolynomial κ R)
        (MvPolynomial.X i)))
    (MvPolynomial.coeff m
      ((AlgHom.id R (MvPolynomial κ R) : (a : MvPolynomial κ R) → MvPolynomial κ R) (MvPolynomial.X i)))
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
R : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : Field L
inst_4 : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv_1 : AlgebraicIndependent R v
hw_1 : AlgebraicIndependent R w
inst_5 : IsAlgClosed K
inst_6 : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this_1 : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := ⋯
⊢ Eq (α := MvPolynomial ι R →ₐ[R] MvPolynomial ι R)
    (AlgHom.comp (B := MvPolynomial κ R) (MvPolynomial.rename (⇑e.symm : (a : κ) → ι))
      (MvPolynomial.rename (⇑e : (a : ι) → κ)))
    (AlgHom.id R (MvPolynomial ι R))
have refine_2 : ∀ (i : ι) (m : ι →₀ ℕ),
  Eq.{u_1 + 1} (α := R)
    (MvPolynomial.coeff m
      ((AlgHom.comp (B := MvPolynomial κ R) (MvPolynomial.rename (⇑e.symm : (a : κ) → ι))
            (MvPolynomial.rename (⇑e : (a : ι) → κ)) :
          (a : MvPolynomial ι R) → MvPolynomial ι R)
        (MvPolynomial.X i)))
    (MvPolynomial.coeff m
      ((AlgHom.id R (MvPolynomial ι R) : (a : MvPolynomial ι R) → MvPolynomial ι R) (MvPolynomial.X i)))
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
R : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : Field L
inst_4 : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv_1 : AlgebraicIndependent R v
hw_1 : AlgebraicIndependent R w
inst_5 : IsAlgClosed K
inst_6 : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this_1 : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := ⋯
⊢ K ≃+* L
have have : (e : RingEquiv.{u_3, u_2} ↥(Algebra.adjoin R (Set.range v)) ↥(Algebra.adjoin R (Set.range w))) → K ≃+* L
Tactic: have e : Algebra.adjoin R (Set.range v) ≃+* Algebra.adjoin R (Set.range w) := by
    refine hv.1.aevalEquiv.symm.toRingEquiv.trans ?_
    refine (AlgEquiv.ofAlgHom (MvPolynomial.rename e)
      (MvPolynomial.rename e.symm) ?_ ?_).toRingEquiv.trans ?_
    · ext; simp
    · ext; simp
    exact hw.1.aevalEquiv.toRingEquiv
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
have 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) ℵ₀)
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}]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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) ℵ₀)
⊢ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
have 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) ℵ₀)
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}]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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) ℵ₀)
⊢ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
have rw₂ : max (Cardinal.lift.{max v u w, max u w} #(MvPolynomial ι R)) ℵ₀ =
  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}]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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) ℵ₀)
⊢ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
have 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) ℵ₀)
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}]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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) ℵ₀)
⊢ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
have rw₄ : Cardinal.lift.{max (max u v) w, max u w} (max #(MvPolynomial ι R) ℵ₀) =
  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}]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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) ℵ₀)
⊢ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
have rw₅ : Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀) = 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}]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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 (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀ = Cardinal.lift.{max u v, w} #ι
have rw : Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι
Tactic: rw [max_eq_left, max_eq_right]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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} #ι
⊢ max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀ = Cardinal.lift.{max u v, w} #ι
have rw₁ : ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)
Tactic: rw [max_eq_left, max_eq_right]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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)
⊢ Nonempty (K ≃+* L)
have obtain : ∀ (s : Set K)
  (hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))),
  Nonempty (K ≃+* L)
Tactic: obtain ⟨s, hs⟩ := exists_isTranscendenceBasis ℤ K
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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))
⊢ Nonempty (K ≃+* L)
have obtain : ∀ (t : Set L)
  (ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))),
  Nonempty (K ≃+* L)
Tactic: obtain ⟨t, ht⟩ := exists_isTranscendenceBasis ℤ L
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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
have rwa : ℵ₀ < Cardinal.lift.{u, v} #L
Tactic: rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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
⊢ ℵ₀ < #L
have rwa₁ : ℵ₀ < Cardinal.lift.{v, u} #K
Tactic: rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
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))
⊢ Nonempty (K ≃+* L)
have hL : ℵ₀ < #L
Tactic: have hL : ℵ₀ < #L := by
    rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
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)
have rw : Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L
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)]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
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
⊢ Nonempty (K ≃+* L)
have this : 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