awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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 :
  IsIntegral 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))
a₁ : Monic (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))
a₂ :
  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)
⊢ Eq (α := K[X])
    (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)))
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))
have a₃ : 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: refine eq_of_monic_of_associated (minpoly.monic ?_) ?_
    (associated_of_dvd_dvd (minpoly.dvd _ _ ?_) ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
    (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)))
have 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)⁻¹)
Tactic: rw [← Polynomial.scaleRoots_dvd_iff _ _ (r := (algebraMap R K r)⁻¹) (IsUnit.mk0 _ (by simpa)),
      ← scaleRoots_mul, mul_inv_cancel₀ (by simpa), scaleRoots_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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)⁻¹)
have 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)
Tactic: refine minpoly.dvd _ _ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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 ((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)
have 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)
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₀]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
have 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
Tactic: refine (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
⊢ P₁ = 0
have 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))
Tactic: obtain ⟨P, rfl⟩ := mk_surjective P₁
Cleared hypotheses: P₁, hP₁
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
have rw : ((powerBasis' sorry).map (equivAdjoin hx)).gen =
  Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x sorry
Tactic: rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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 ⋯
⊢ (adjoin.powerBasis' hx).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
have rw₁ : Eq.{u_2 + 1} (α := ↥R[x]) ((equivAdjoin hx : (a : AdjoinRoot (minpoly R x)) → ↥R[x]) (powerBasis' sorry).gen : ↥R[x])
  (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x sorry : ↥R[x])
Tactic: rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
⊢ (adjoin.powerBasis' hx).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
have 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 sorry : ↥R[x])
Tactic: rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
⊢ (adjoin.powerBasis' hx).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
have rw₃ : Eq.{u_2 + 1} (α := ↥R[x])
  ((AlgEquiv.ofBijective (Minpoly.toAdjoin R x) sorry : (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 sorry : ↥R[x])
Tactic: rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
⊢ (adjoin.powerBasis' hx).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
have 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 sorry : ↥R[x])
Tactic: rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
⊢ (adjoin.powerBasis' hx).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
have 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 sorry) sorry :
          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 sorry : ↥R[x])
Tactic: rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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])
⊢ (adjoin.powerBasis' hx).gen = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
have rw₆ : Eq (α := ↥R[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x sorry)
  (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x sorry)
Tactic: rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftAlgHom_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ PowerBasis R S
have apply : Eq (α := Subalgebra R S) R[x] ⊤
Tactic: apply PowerBasis.ofAdjoinEqTop' hint
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (goal)
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} #σ)) ℵ₀
have refine_1 : #(FractionRing (MvPolynomial σ F)) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
Tactic: refine ((rank_le_card _ _).trans ?_).antisymm ?_
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (goal)
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} #σ)) ℵ₀
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
have refine_2 : max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Tactic: refine ((rank_le_card _ _).trans ?_).antisymm ?_
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (goal)
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
⊢ #(FractionRing (MvPolynomial σ F)) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
have refine_1 : #(MvPolynomial σ F) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
Tactic: rw [FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (goal)
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} #σ)) ℵ₀
⊢ #(FractionRing (MvPolynomial σ F)) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
have refine_1₁ : max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀
Tactic: rw [FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (hypothesis)
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
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
have hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
Tactic: have hinj := IsFractionRing.injective R K
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (hypothesis)
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
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
have h1 : Module.rank F R ≤ Module.rank F K
Tactic: have h1 := (IsScalarTower.toAlgHom F R K).toLinearMap.rank_le_of_injective hinj
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (hypothesis)
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
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : Module.rank F R ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
have h1₁ : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
Tactic: rw [MvPolynomial.rank_eq_lift, mk_finsupp_nat, lift_max, lift_aleph0, max_le_iff] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (goal)
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
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
have refine_2 : ∀ (i : σ), max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Tactic: obtain ⟨i⟩ := ‹Nonempty σ›
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (hypothesis)
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
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
have hx : Transcendental F (A := K) ((algebraMap R K : (a : R) → K) (MvPolynomial.X i) : K)
Tactic: have hx : Transcendental F (algebraMap R K (MvPolynomial.X i)) :=
    (transcendental_algebraMap_iff hinj).2 (MvPolynomial.transcendental_X F i)