awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq.{u_2 + 1} (α := L)
    ((Polynomial.aeval
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)) :
          (a : K[X]) → L)
        (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r)) :
      L)
    (0 : L)

Tactic:
scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

Premises used: Set.Mem, Polynomial.scaleRoots_aeval_eq_zero, minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq.{u_2 + 1} (α := L)
    ((Polynomial.aeval
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)) :
          (a : K[X]) → L)
        (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r)) :
      L)
    (0 : L)

Tactic:
exact scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

Premises used: Polynomial.scaleRoots_aeval_eq_zero, minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Ne (α := K) (((algebraMap R K : (a : R) → K) r)⁻¹ : K) (0 : K)

Tactic:
simpa
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Ne (α := K) ((algebraMap R K : (a : R) → K) r : K) (0 : K)

Tactic:
simpa
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
a :
  Dvd.dvd (α := K[X]) (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (scaleRoots
      (minpoly K
        (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
          ((algebraMap S L : (a : S) → L) s : L)))
      ((algebraMap R K : (a : R) → K) r)⁻¹)
⊢ Dvd.dvd (α := K[X])
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))
    (minpoly K
      (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
        ((algebraMap S L : (a : S) → L) s : L)))

Tactic:
rw [← Polynomial.scaleRoots_dvd_iff _ _ (r := (algebraMap R K r)⁻¹) (IsUnit.mk0 _ (by simpa)),
      ← scaleRoots_mul, mul_inv_cancel₀ (by simpa), scaleRoots_one]

Premises used: mul_inv_cancel₀, Polynomial.scaleRoots_mul, Polynomial.scaleRoots_dvd_iff, IsUnit.mk0, Polynomial.scaleRoots_one
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Dvd.dvd (α := K[X]) (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (scaleRoots
      (minpoly K
        (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
          ((algebraMap S L : (a : S) → L) s : L)))
      ((algebraMap R K : (a : R) → K) r)⁻¹)

Tactic:
minpoly.dvd _ _ ?_

Premises used: minpoly.dvd
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
a :
  Eq.{u_2 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (scaleRoots
          (minpoly K
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)))
          ((algebraMap R K : (a : R) → K) r)⁻¹) :
      L)
    (0 : L)
⊢ Dvd.dvd (α := K[X]) (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (scaleRoots
      (minpoly K
        (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
          ((algebraMap S L : (a : S) → L) s : L)))
      ((algebraMap R K : (a : R) → K) r)⁻¹)

Tactic:
refine minpoly.dvd _ _ ?_

Premises used: minpoly.dvd
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Ne.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L) (0 : L)

Tactic:
simpa
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
a :
  Eq.{u_2 + 1} (α := L)
    ((Polynomial.aeval
            (HMul.hMul (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r)⁻¹ : L)
              (HMul.hMul (α := L) (β := L)
                (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
                ((algebraMap S L : (a : S) → L) s : L))) :
          (a : K[X]) → L)
        (scaleRoots
          (minpoly K
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)))
          ((algebraMap R K : (a : R) → K) r)⁻¹) :
      L)
    (0 : L)
⊢ Eq.{u_2 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (scaleRoots
          (minpoly K
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)))
          ((algebraMap R K : (a : R) → K) r)⁻¹) :
      L)
    (0 : L)

Tactic:
nth_rw 1 [← inv_mul_cancel_left₀ (b := algebraMap S L s)
      (a := algebraMap K L (algebraMap R K r)) (by simpa), ← map_inv₀]

Premises used: Algebra.algebraMap, inv_mul_cancel_left₀, map_inv₀, DFunLike.coe
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq.{u_2 + 1} (α := L)
    ((Polynomial.aeval
            (HMul.hMul (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r)⁻¹ : L)
              (HMul.hMul (α := L) (β := L)
                (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
                ((algebraMap S L : (a : S) → L) s : L))) :
          (a : K[X]) → L)
        (scaleRoots
          (minpoly K
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)))
          ((algebraMap R K : (a : R) → K) r)⁻¹) :
      L)
    (0 : L)

Tactic:
scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

Premises used: Set.Mem, Polynomial.scaleRoots_aeval_eq_zero, minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq.{u_2 + 1} (α := L)
    ((Polynomial.aeval
            (HMul.hMul (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r)⁻¹ : L)
              (HMul.hMul (α := L) (β := L)
                (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
                ((algebraMap S L : (a : S) → L) s : L))) :
          (a : K[X]) → L)
        (scaleRoots
          (minpoly K
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)))
          ((algebraMap R K : (a : R) → K) r)⁻¹) :
      L)
    (0 : L)

Tactic:
exact scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

Premises used: Polynomial.scaleRoots_aeval_eq_zero, minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
⊢ Injective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly R x)) (β := ↥R[x])
    (⇑(Minpoly.toAdjoin R x) : (a : AdjoinRoot (minpoly R x)) → ↥R[x])

Tactic:
(injective_iff_map_eq_zero _).2 fun P₁ hP₁ => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
refine :
  ∀ (P₁ : AdjoinRoot (minpoly R x))
    (hP₁ :
      Eq.{u_2 + 1} (α := ↥R[x])
        (((Minpoly.toAdjoin R x : AlgHom.{u_1, u_1, u_2} R (AdjoinRoot (minpoly R x)) ↥R[x]) :
              (a : AdjoinRoot (minpoly R x)) → ↥R[x])
            P₁ :
          ↥R[x])
        (0 : ↥R[x])),
    P₁ = 0
⊢ Injective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly R x)) (β := ↥R[x])
    (⇑(Minpoly.toAdjoin R x) : (a : AdjoinRoot (minpoly R x)) → ↥R[x])

Tactic:
refine (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ :
  Eq.{u_2 + 1} (α := ↥R[x])
    (((Minpoly.toAdjoin R x : AlgHom.{u_1, u_1, u_2} R (AdjoinRoot (minpoly R x)) ↥R[x]) :
          (a : AdjoinRoot (minpoly R x)) → ↥R[x])
        P₁ :
      ↥R[x])
    (0 : ↥R[x])
obtain :
  ∀ (P : R[X])
    (hP₁ :
      Eq.{u_2 + 1} (α := ↥R[x])
        (((Minpoly.toAdjoin R x : AlgHom.{u_1, u_1, u_2} R (AdjoinRoot (minpoly R x)) ↥R[x]) :
              (a : AdjoinRoot (minpoly R x)) → ↥R[x])
            ((AdjoinRoot.mk (minpoly R x) : (a : R[X]) → AdjoinRoot (minpoly R x)) P) :
          ↥R[x])
        (0 : ↥R[x])),
    Eq (α := AdjoinRoot (minpoly R x))
      ((AdjoinRoot.mk (minpoly R x) : (a : R[X]) → AdjoinRoot (minpoly R x)) P : AdjoinRoot (minpoly R x))
      (0 : AdjoinRoot (minpoly R x))
⊢ P₁ = 0

Tactic:
obtain ⟨P, rfl⟩ := mk_surjective P₁

Premises used: AdjoinRoot.mk_surjective, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
P : R[X]
hP₁ :
  Eq.{u_2 + 1} (α := ↥R[x])
    (((Minpoly.toAdjoin R x : AlgHom.{u_1, u_1, u_2} R (AdjoinRoot (minpoly R x)) ↥R[x]) :
          (a : AdjoinRoot (minpoly R x)) → ↥R[x])
        ((AdjoinRoot.mk (minpoly R x) : (a : R[X]) → AdjoinRoot (minpoly R x)) P) :
      ↥R[x])
    (0 : ↥R[x])
⊢ Eq (α := AdjoinRoot (minpoly R x))
    ((AdjoinRoot.mk (minpoly R x) : (a : R[X]) → AdjoinRoot (minpoly R x)) P : AdjoinRoot (minpoly R x))
    (0 : AdjoinRoot (minpoly R x))

Tactic:
simpa [← Subalgebra.coe_eq_zero, isIntegrallyClosed_dvd_iff hx, ← aeval_def] using hP₁

Premises used: Polynomial.aeval_def, minpoly.isIntegrallyClosed_dvd_iff, Subalgebra.coe_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
⊢ (↑(equivAdjoin hx) : AdjoinRoot (minpoly R x) →ₐ[R] ↥R[x]) = Minpoly.toAdjoin R x

Tactic:
rfl

Premises used: Subsemiring.mk', AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Subsemiring.closure, Set.Mem, AddCon.liftOn, setOf, AdjoinRoot.Minpoly.toAdjoin, AdjoinRoot.liftAlgHom, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AdjoinRoot.lift, AddCon.Quotient, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
⊢ Eq (α := (a : AdjoinRoot (minpoly R x)) → ↥R[x]) (⇑(equivAdjoin hx) : (a : AdjoinRoot (minpoly R x)) → ↥R[x])
    (⇑(Minpoly.toAdjoin R x) : (a : AdjoinRoot (minpoly R x)) → ↥R[x])

Tactic:
rfl

Premises used: AdjoinRoot, Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
⊢ (adjoin.powerBasis' hx).dim = natDegree (minpoly R x)

Tactic:
rfl

Premises used: WithBot.recBotCoe, Polynomial.natDegree, WithBot.unbotD, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
rw :
  ((powerBasis' ⋯).map (equivAdjoin hx)).gen =
    Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
rw₁ :
  Eq.{u_2 + 1} (α := ↥R[x]) ((equivAdjoin hx : (a : AdjoinRoot (minpoly R x)) → ↥R[x]) (powerBasis' ⋯).gen : ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯ : ↥R[x])
rw₂ :
  Eq.{u_2 + 1} (α := ↥R[x])
    ((equivAdjoin hx : (a : AdjoinRoot (minpoly R x)) → ↥R[x]) (AdjoinRoot.root (minpoly R x)) : ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯ : ↥R[x])
rw₃ :
  Eq.{u_2 + 1} (α := ↥R[x])
    ((AlgEquiv.ofBijective (Minpoly.toAdjoin R x) ⋯ : (a : AdjoinRoot (minpoly R x)) → ↥R[x])
        (AdjoinRoot.root (minpoly R x)) :
      ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯ : ↥R[x])
rw₄ :
  Eq.{u_2 + 1} (α := ↥R[x])
    (((Minpoly.toAdjoin R x : AlgHom.{u_1, u_1, u_2} R (AdjoinRoot (minpoly R x)) ↥R[x]) :
          (a : AdjoinRoot (minpoly R x)) → ↥R[x])
        (AdjoinRoot.root (minpoly R x)) :
      ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯ : ↥R[x])
rw₅ :
  Eq.{u_2 + 1} (α := ↥R[x])
    (((liftAlgHom (minpoly R x) (ofId R ↥R[x])
              (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯) ⋯ :
            AlgHom.{u_1, u_1, u_2} R (AdjoinRoot (minpoly R x)) ↥R[x]) :
          (a : AdjoinRoot (minpoly R x)) → ↥R[x])
        (AdjoinRoot.root (minpoly R x)) :
      ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯ : ↥R[x])
rw₆ rw₇ :
  Eq (α := ↥R[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯)
⊢ (adjoin.powerBasis' hx).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯

Tactic:
rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]

Premises used: AdjoinRoot.powerBasis'_gen, PowerBasis.map_gen, minpoly.equivAdjoin, AlgEquiv.ofBijective_apply, AdjoinRoot.Minpoly.toAdjoin, Algebra.adjoin.powerBasis', AdjoinRoot.liftAlgHom_root
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x_1 x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : Membership.mem (γ := Subalgebra R S) R[x] B.gen
apply : Eq (α := Subalgebra R S) R[x] ⊤
⊢ PowerBasis R S

Tactic:
apply PowerBasis.ofAdjoinEqTop' hint

Premises used: PowerBasis.ofAdjoinEqTop'
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x_1 x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : Membership.mem (γ := Subalgebra R S) R[x] B.gen
⊢ Eq (α := Subalgebra R S) R[x] ⊤

Tactic:
PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx

Premises used: PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x_1 x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : Membership.mem (γ := Subalgebra R S) R[x] B.gen
⊢ Eq (α := Subalgebra R S) R[x] ⊤

Tactic:
exact PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx

Premises used: PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
hx' : Eq (α := Subalgebra R S) R[x] ⊤
⊢ (PowerBasis.ofAdjoinEqTop' hx hx').dim = natDegree (minpoly R x)

Tactic:
rfl

Premises used: WithBot.recBotCoe, Polynomial.natDegree, WithBot.unbotD, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
hx' : Eq (α := Subalgebra R S) R[x] ⊤
⊢ (PowerBasis.ofAdjoinEqTop' hx hx').gen = x

Tactic:
simp [PowerBasis.ofAdjoinEqTop']

Premises used: PowerBasis.ofAdjoinEqTop'
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
K : Type u_3
L : Type u_4
inst_7 : Field K
inst_8 : Field L
inst_9 : Algebra K L
A : Subring K
inst_10 : IsIntegrallyClosed.{u_3} ↥A
inst_11 : IsFractionRing (↥A) K
⊢ IsScalarTower.{u_3, u_4, u_4} (↥A) (↥(integralClosure (↥A) L)) L

Tactic:
IsScalarTower.subalgebra' A L L (integralClosure A L)

Premises used: Set.Mem, Membership.mem, Subtype, integralClosure, IsScalarTower.subalgebra'
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subring K
inst_3 : IsIntegrallyClosed.{u_3} ↥A
inst_4 : IsFractionRing (↥A) K
x : ↥(integralClosure (↥A) L)
⊢ Eq (α := K[X]) (map (R := ↥A) (algebraMap (↥A) K) (minpoly (↥A) x)) (minpoly K (↑x : L))

Tactic:
eq_comm.mpr (isIntegrallyClosed_eq_field_fractions K L (IsIntegralClosure.isIntegral A L x))

Premises used: Iff.mpr, Membership.mem, minpoly.isIntegrallyClosed_eq_field_fractions, Subtype, IsIntegralClosure.isIntegral, eq_comm
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀

Tactic:
((rank_le_card _ _).trans ?_).antisymm ?_

Premises used: LE.le.antisymm, rank_le_card, LE.le.trans
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
refine_1 : #(FractionRing (MvPolynomial σ F)) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
refine_2 : max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀

Tactic:
refine ((rank_le_card _ _).trans ?_).antisymm ?_

Premises used: LE.le.antisymm, rank_le_card, LE.le.trans
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
refine_1 : #(MvPolynomial σ F) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
refine_1₁ refine_1₂ : max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
⊢ #(FractionRing (MvPolynomial σ F)) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀

Tactic:
rw [FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift]

Premises used: FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)

Tactic:
have hinj := IsFractionRing.injective R K