awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
K : Type u_2
A : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field A
inst_3 : Algebra F K
inst_4 : Algebra F A
inst_5 : Algebra.IsAlgebraic F K
L : Type u_4
inst_6 : Field L
inst_7 : Algebra F L
inst_8 : Algebra L A
inst_9 : IsScalarTower F L A
hL : ∀ (x : K), Splits (map (algebraMap F L) (minpoly F x))
f : K →ₐ[F] L
x : K
⊢ Eq.{u_3 + 1} (α := A)
    ((((algHomEquivAlgHomOfSplits A L hL : (a : K →ₐ[F] L) → K →ₐ[F] A) f : K →ₐ[F] A) : (a : K) → A) x : A)
    ((algebraMap L A : (a : L) → A) ((f : (a : K) → L) x : L) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
⟨?_, isRoot_of_isRoot_of_dvd_derivative_mul hf0⟩

Premises used: Polynomial.isRoot_of_isRoot_of_dvd_derivative_mul, Iff.intro
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
refine : (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
refine ⟨?_, isRoot_of_isRoot_of_dvd_derivative_mul hf0⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : CharZero K
f g : K[X]
hf0 : f ≠ 0
pos :
  ∀ (hg0 : g = 0),
    (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g
neg :
  ∀ (hg0 : ¬g = 0),
    (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
by_cases hg0 : g = 0
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
simp [hg0]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
pos :
  ∀ (hdf0 : Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) (0 : K[X])),
    (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g
neg :
  ∀ (hdf0 : ¬Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) (0 : K[X])),
    (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
by_cases hdf0 : derivative f = 0

Premises used: Polynomial.derivative, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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])
pos :
  (∀ (x : K), IsRoot ((C : (a : K) → K[X]) (f.coeff 0)) x → g.IsRoot x) →
    (C : (a : K) → K[X]) (f.coeff 0) ∣
      HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) ((C : (a : K) → K[X]) (f.coeff 0)) : K[X]) g
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
rw [eq_C_of_derivative_eq_zero hdf0]

Premises used: Polynomial.eq_C_of_derivative_eq_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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])
⊢ (∀ (x : K), IsRoot ((C : (a : K) → K[X]) (f.coeff 0)) x → g.IsRoot x) →
    (C : (a : K) → K[X]) (f.coeff 0) ∣
      HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) ((C : (a : K) → K[X]) (f.coeff 0)) : K[X]) g

Tactic:
simp only [derivative_C, zero_mul, dvd_zero, implies_true]

Premises used: dvd_zero, MulZeroClass.zero_mul, Polynomial.derivative_C, implies_true
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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])
⊢ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g ≠ 0

Tactic:
have hdg : f.derivative * g ≠ 0 := mul_ne_zero hdf0 hg0
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
neg :
  (∀ (x : K), f.IsRoot x → g.IsRoot x) →
    ∀ (a : K),
      Multiset.count a f.roots ≤
        Multiset.count a (HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g).roots
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
rw [IsAlgClosed.dvd_iff_roots_le_roots hf0 hdg, Multiset.le_iff_count]

Premises used: Multiset.le_iff_count, IsAlgClosed.dvd_iff_roots_le_roots
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
neg :
  (∀ (x : K), f.IsRoot x → g.IsRoot x) →
    ∀ (a : K),
      Multiset.count a f.roots ≤
        Multiset.count a (HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g).roots
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g

Tactic:
classical rw [IsAlgClosed.dvd_iff_roots_le_roots hf0 hdg, Multiset.le_iff_count]

Premises used: Multiset.le_iff_count, IsAlgClosed.dvd_iff_roots_le_roots
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
neg :
  (∀ (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
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) →
    ∀ (a : K),
      Multiset.count a f.roots ≤
        Multiset.count a (HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) f : K[X]) g).roots

Tactic:
simp only [count_roots, rootMultiplicity_mul hdg]

Premises used: Polynomial.rootMultiplicity_mul, Polynomial.count_roots
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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

Tactic:
forall_imp fun a => ?_

Premises used: forall_imp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
neg :
  ∀ (a : K),
    (f.IsRoot a → g.IsRoot a) →
      rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g
⊢ (∀ (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

Tactic:
refine forall_imp fun a => ?_

Premises used: forall_imp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
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
⊢ (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

Premises used: Polynomial.eval
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ 0 < rootMultiplicity a f

Tactic:
have h0 : 0 < f.rootMultiplicity a := (rootMultiplicity_pos hf0).2 haf
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
pos : (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g
⊢ (f.IsRoot a → g.IsRoot a) →
    rootMultiplicity a f ≤ rootMultiplicity a ((derivative : (a : K[X]) → K[X]) f) + rootMultiplicity a g

Tactic:
rw [derivative_rootMultiplicity_of_root haf]

Premises used: Polynomial.derivative_rootMultiplicity_of_root
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
h : f.IsRoot a → g.IsRoot a
⊢ rootMultiplicity a f = rootMultiplicity a f - 1 + 1

Tactic:
(Nat.sub_add_cancel (Nat.succ_le_iff.1 h0)).symm

Premises used: Nat.sub_add_cancel, Iff.mp, Eq.symm, Nat.succ_le_iff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
h : f.IsRoot a → g.IsRoot a
⊢ rootMultiplicity a f - 1 + 1 ≤ rootMultiplicity a f - 1 + rootMultiplicity a g

Tactic:
add_le_add le_rfl (Nat.succ_le_iff.1
        ((rootMultiplicity_pos hg0).2 (h haf)))

Premises used: Iff.mpr, le_rfl, add_le_add, Polynomial.rootMultiplicity_pos, Iff.mp, Nat.succ_le_iff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
h : f.IsRoot a → g.IsRoot a
⊢ rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g

Tactic:
calc rootMultiplicity a f
        = rootMultiplicity a f - 1 + 1 := (Nat.sub_add_cancel (Nat.succ_le_iff.1 h0)).symm
      _ ≤ rootMultiplicity a f - 1 + rootMultiplicity a g := add_le_add le_rfl (Nat.succ_le_iff.1
        ((rootMultiplicity_pos hg0).2 (h haf)))

Premises used: le_rfl, add_le_add, Nat.sub_add_cancel, Iff.mp, Polynomial.rootMultiplicity, Eq.symm, Nat.succ_le_iff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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

Tactic:
simp [haf, rootMultiplicity_eq_zero haf]

Premises used: Polynomial.rootMultiplicity_eq_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
ι : Type u_4
v : ι → K
inst_3 : IsAlgClosed K
hv : IsTranscendenceBasis R v
this : Nontrivial R := ⋯
⊢ IsAlgClosed K

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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 : MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))
⊢ RingEquiv.{u_3, u_2} ↥(Algebra.adjoin R (Set.range v)) ↥(Algebra.adjoin R (Set.range w))

Tactic:
refine hv.1.aevalEquiv.symm.toRingEquiv.trans ?_

Premises used: AlgEquiv.symm, AlgebraicIndependent.aevalEquiv, And.left, AlgEquiv.toRingEquiv, RingEquiv.trans
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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))
refine_3 : MvPolynomial κ R ≃+* ↥(Algebra.adjoin R (Set.range w))
⊢ MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))

Tactic:
refine (AlgEquiv.ofAlgHom (MvPolynomial.rename e)
      (MvPolynomial.rename e.symm) ?_ ?_).toRingEquiv.trans ?_

Premises used: MvPolynomial.rename, AlgEquiv.toRingEquiv, AlgEquiv.ofAlgHom, RingEquiv.trans, Equiv.symm, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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 :
  ∀ (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)))
⊢ 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:
ext
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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 := ⋯
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:
simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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_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)))
⊢ 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:
ext
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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 := ⋯
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:
simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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))

Tactic:
exact hw.1.aevalEquiv.toRingEquiv

Premises used: AlgebraicIndependent.aevalEquiv, And.left, AlgEquiv.toRingEquiv
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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 := ⋯
have : (e : RingEquiv.{u_3, u_2} ↥(Algebra.adjoin R (Set.range v)) ↥(Algebra.adjoin R (Set.range w))) → K ≃+* L
⊢ 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
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
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_1 : ι ≃ κ
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 := ⋯
e : RingEquiv.{u_3, u_2} ↥(Algebra.adjoin R (Set.range v)) ↥(Algebra.adjoin R (Set.range w))
⊢ K ≃+* L

Tactic:
exact IsAlgClosure.equivOfEquiv K L e

Premises used: IsAlgClosure.equivOfEquiv
-- 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
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := ⋯
⊢ Cardinal.lift.{max u w, v} #K ≤ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀)

Tactic:
simpa using Algebra.IsAlgebraic.cardinalMk_le_max (Algebra.adjoin R (Set.range v)) K

Premises used: Algebra.IsAlgebraic.cardinalMk_le_max, Algebra.adjoin, Membership.mem, Subtype, Set.range