awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
⊢ Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(AlgHom.restrictScalars R (toIntegralClosure R S B)) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
    (⇑((↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
                (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                  (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
                  ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
            TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
              ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
have h : Eq (α :=
  TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
  (AlgHom.restrictScalars R (toIntegralClosure R S B))
  (↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
        (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
          (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
          ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
    S ⊗[R] ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
⊢ Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (AlgHom.restrictScalars R (toIntegralClosure R S B))
    (↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
          (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
      S ⊗[R] ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)))
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (AlgHom.restrictScalars R (toIntegralClosure R S B))
    (↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
          (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
      S ⊗[R] ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)))
have h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply IsLocalization.algHom_ext M
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
x : ↥(integralClosure R B)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : Eq (α := S ⊗[R] B) (1 ⊗ₜ[R] (↑x : B))
  (↑((IsLocalization.map (R := ↥(integralClosure R B)) (M := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (T := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (RingHom.id ↥(integralClosure R B)) sorry :
          (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
        (1 ⊗ₜ[R] x)) :
    S ⊗[R] B)
Tactic: dsimp [toIntegralClosure]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
x : ↥(integralClosure R B)
⊢ Eq (α := S ⊗[R] B) (1 ⊗ₜ[R] (↑x : B))
    (↑((IsLocalization.map (R := ↥(integralClosure R B)) (M := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
              (T := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
              (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (RingHom.id ↥(integralClosure R B)) ⋯ :
            (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
          (1 ⊗ₜ[R] x)) :
      S ⊗[R] B)
have h : Eq (α := S ⊗[R] B) ((algebraMap B (S ⊗[R] B) : (a : B) → S ⊗[R] B) (↑x : B) : S ⊗[R] B)
  ((↑((algebraMap ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :
            (a : ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
          x) :
      S ⊗[R] B) :
    S ⊗[R] B)
Tactic: simp [← Algebra.TensorProduct.right_algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a
have have : ∀ (𝓟 : StandardEtalePresentation R S),
  Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a
Tactic: have 𝓟 := Classical.ofNonempty (α := StandardEtalePresentation R S)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R]
  Localization.Away (M := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :=
  𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst : Algebra.{u_1, u_2} (AdjoinRoot 𝓟.f) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      ((↑e.symm : Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) →ₐ[R] S).comp
        (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f)
          (Localization.Away (M := AdjoinRoot 𝓟.f)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)))))
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
have this : IsLocalization (R := AdjoinRoot 𝓟.f)
  (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
Tactic: have := IsLocalization.isLocalization_of_algEquiv (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g))
      { toRingEquiv := e.symm.toRingEquiv, commutes' := by simp [RingHom.algebraMap_toAlgebra] }
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R]
  Localization.Away (M := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :=
  𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst : Algebra.{u_1, u_2} (AdjoinRoot 𝓟.f) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      ((↑e.symm : Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) →ₐ[R] S).comp
        (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f)
          (Localization.Away (M := AdjoinRoot 𝓟.f)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
have obtain : ∀ (m : ℕ)
  (hm :
    IsIntegral (AdjoinRoot 𝓟.f)
      (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
          Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
            (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
          ((fun (x : ℕ) ↦
              HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
                x)
            m)
          sorry •
        a)),
  ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
Tactic: obtain ⟨⟨_, m, rfl⟩, hm⟩ := IsIntegral.exists_multiple_integral_of_isLocalization
      (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g)) _ hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R]
  Localization.Away (M := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :=
  𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst : Algebra.{u_1, u_2} (AdjoinRoot 𝓟.f) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      ((↑e.symm : Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) →ₐ[R] S).comp
        (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f)
          (Localization.Away (M := AdjoinRoot 𝓟.f)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  IsIntegral (AdjoinRoot 𝓟.f)
    (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
        Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
          (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
        ((fun (x : ℕ) ↦
            HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) x)
          m)
        ⋯ •
      a)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
have hm₁ : ∀ (k : ℕ),
  IsIntegral (AdjoinRoot 𝓟.f)
    (HMul.hMul (α := S ⊗[R] B)
      ((algebraMap (AdjoinRoot 𝓟.f) (S ⊗[R] B) : (a : AdjoinRoot 𝓟.f) → S ⊗[R] B)
          (HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) k) :
        S ⊗[R] B)
      (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
          Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
            (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
          ((fun (x : ℕ) ↦
              HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
                x)
            m)
          sorry •
        a))
Tactic: replace hm := fun k : ℕ ↦ (isIntegral_algebraMap (x := AdjoinRoot.mk 𝓟.f 𝓟.g ^ k)).mul hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R]
  Localization.Away (M := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :=
  𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst : Algebra.{u_1, u_2} (AdjoinRoot 𝓟.f) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      ((↑e.symm : Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) →ₐ[R] S).comp
        (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f)
          (Localization.Away (M := AdjoinRoot 𝓟.f)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HMul.hMul (α := S ⊗[R] B)
        ((algebraMap (AdjoinRoot 𝓟.f) (S ⊗[R] B) : (a : AdjoinRoot 𝓟.f) → S ⊗[R] B)
            (HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
              k) :
          S ⊗[R] B)
        (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
                  x)
              m)
            ⋯ •
          a))
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
have hm₁ : ∀ (k : ℕ),
  IsIntegral (AdjoinRoot 𝓟.f)
    (HSMul.hSMul (α := S)
      ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
          ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) (𝓟.g ^ (m + k)) : AdjoinRoot 𝓟.f) :
        S)
      a)
Tactic: simp only [Submonoid.smul_def, ← @IsScalarTower.algebraMap_smul (AdjoinRoot 𝓟.f) S,
      ← map_pow, ← Algebra.smul_def, ← mul_smul, ← map_mul, ← pow_add, add_comm _ m] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R]
  Localization.Away (M := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :=
  𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst : Algebra.{u_1, u_2} (AdjoinRoot 𝓟.f) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      ((↑e.symm : Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) →ₐ[R] S).comp
        (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f)
          (Localization.Away (M := AdjoinRoot 𝓟.f)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HSMul.hSMul (α := S)
        ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) (𝓟.g ^ (m + k)) : AdjoinRoot 𝓟.f) :
          S)
        a)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
have hm₁ : ∀ (k : ℕ),
  IsIntegral (AdjoinRoot 𝓟.f)
    (HPow.hPow (α := S)
        ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
          S)
        (m + k) •
      a)
Tactic: simp_rw [map_pow] at hm
Cleared hypotheses: hm