awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
refine_1 :
  pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap R S)) ≅
    CommRingCat.of (S ⊗[R] S)
⊢ IsPushout.{u, u + 1} (Z := CommRingCat.of (S ⊗[R] S)) (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of S) (P :=
    CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
          S ⊗[R] S →ₐ[R] T ⊗[R] A)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
    (CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))
have refine_2 : pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap S T)))
    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap S A))) ≅
  CommRingCat.of (T ⊗[R] A)
Tactic: refine .of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
refine_1 :
  pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap R S)) ≅
    CommRingCat.of (S ⊗[R] S)
refine_2 :
  pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
      (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap S T)))
      (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap S A))) ≅
    CommRingCat.of (T ⊗[R] A)
⊢ IsPushout.{u, u + 1} (Z := CommRingCat.of (S ⊗[R] S)) (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of S) (P :=
    CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
          S ⊗[R] S →ₐ[R] T ⊗[R] A)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
    (CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))
have refine_3 : pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A) (CommRingCat.ofHom (algebraMap S T))
    (CommRingCat.ofHom (algebraMap S A)) ≅
  CommRingCat.of (T ⊗[S] A)
Tactic: refine .of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ Eq (α :=
    pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap R S)) ⟶
      CommRingCat.of S)
    (pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ Iso.hom (Iso.refl (CommRingCat.of S)))
    (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫ CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
have refine_5 : ∀ (x : (↑(CommRingCat.of S) : Type u)),
  Eq (α := (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ Iso.hom (Iso.refl (CommRingCat.of S)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout sorry)) ≫
                CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ Eq (α := CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A))
    (CategoryStruct.comp (Y :=
      pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
        (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
      (CommRingCat.ofHom (algebraMap S T) ≫
        pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
      (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯))))
    (Iso.hom (Iso.refl (CommRingCat.of S)) ≫
      CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))
have refine_7 : ∀ (x : (↑(CommRingCat.of S) : Type u)),
  Eq (α := (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
              (CommRingCat.ofHom (algebraMap S T) ≫
                pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout sorry)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
    ((CommRingCat.Hom.hom
            (Iso.hom (Iso.refl (CommRingCat.of S)) ≫
              CommRingCat.ofHom
                (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Injective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective (α := S) (β := T) (⇑g : (a : S) → T)
⊢ Function.Injective (α := R) (β := T) (⇑(g.comp f) : (a : R) → T)
have simp : Function.Injective (α := R) (β := T) (Function.comp (β := S) (⇑g : (a : S) → T) (⇑f : (a : R) → S))
Tactic: simp only [RingHom.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Injective (goal)
Goal:
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)
have apply : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  Function.Injective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
Tactic: apply RingHom.injective_stableUnderComposition.respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
⊢ RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral
have apply : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsIntegral
Tactic: apply isIntegral_stableUnderComposition.respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem x
have rw : e.toRingHom.IsIntegralElem ((e : (a : R) → S) ((e.symm : (a : S) → R) x : R))
Tactic: rw [← e.apply_symm_apply x]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral
have refine : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T], IsIntegral (algebraMap R T) → IsIntegral (A := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
Tactic: refine IsStableUnderBaseChange.mk isIntegral_respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
int : IsIntegral (algebraMap R T)
⊢ IsIntegral (A := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have rw : ∀ (int : Algebra.IsIntegral R T), Algebra.IsIntegral S (S ⊗[R] T)
Tactic: rw [algebraMap_isIntegral_iff] at int ⊢
Cleared hypotheses: int
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this : Algebra R S := f.toAlgebra
⊢ f.IsIntegralElem r
have change : Membership.mem (γ := Submodule R S)
  ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S) r
Tactic: change r ∈ (integralClosure R S).toSubmodule
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this : Algebra R S := f.toAlgebra
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S) r
have H₁ : ∀ (r_1 : (↑s : Type u_1)),
  ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑r_1 : R) ^ n • r)
Tactic: apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ s hs
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have this₁ : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
Tactic: haveI : IsScalarTower R (Localization.Away t) (Localization.Away (f t)) := .of_algebraMap_eq'
    (IsLocalization.lift_comp _).symm
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have this₁ : _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
  ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
        (a : S) → Localization.Away ((f : (a : R) → S) t))
      r :
    Localization.Away (M := S) ((f : (a : R) → S) t : S))
Tactic: have : _root_.IsIntegral (Localization.Away t) (algebraMap S (Localization.Away (f t)) r) :=
    H ⟨t, ht⟩ (algebraMap _ _ r)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have H₁ : ∀ (n : ℕ) (p : R[X]) (hp : p.Monic)
  (hp' :
    eval₂ (algebraMap R (Localization.Away (M := S) ((f : (a : R) → S) t : S)))
        (HSMul.hSMul (β := Localization.Away (M := S) ((f : (a : R) → S) t : S))
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
            ((fun (x : ℕ) ↦ t ^ x) n) sorry)
          ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
                (a : S) → Localization.Away ((f : (a : R) → S) t))
              r :
            Localization.Away (M := S) ((f : (a : R) → S) t : S)))
        p =
      0),
  ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
Tactic: obtain ⟨⟨_, n, rfl⟩, p, hp, hp'⟩ := this.exists_multiple_integral_of_isLocalization (.powers t)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ (algebraMap R (Localization.Away (M := S) ((f : (a : R) → S) t : S)))
      (HSMul.hSMul (β := Localization.Away (M := S) ((f : (a : R) → S) t : S))
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
          ((fun (x : ℕ) ↦ t ^ x) n) ⋯)
        ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
              (a : S) → Localization.Away ((f : (a : R) → S) t))
            r :
          Localization.Away (M := S) ((f : (a : R) → S) t : S)))
      p =
    0
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have hp'₁ : ∃ (m : ↥(Submonoid.powers ((f : (a : R) → S) t) : Submonoid S)),
  (↑m : S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) sorry) :
                R) :
            S)
          r)
        p =
    0
Tactic: rw [IsScalarTower.algebraMap_eq R S, Submonoid.smul_def, Algebra.smul_def,
    IsScalarTower.algebraMap_apply R S, ← map_mul, ← hom_eval₂,
    IsLocalization.map_eq_zero_iff (.powers (f t))] at hp'
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  ∃ (m : ↥(Submonoid.powers ((f : (a : R) → S) t) : Submonoid S)),
    (↑m : S) *
        eval₂ (algebraMap R S)
          (HMul.hMul (α := S)
            ((algebraMap R S : (a : R) → S)
                (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                      ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                  R) :
              S)
            r)
          p =
      0
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have H₁ : ∀ (m : ℕ)
  (e :
    (↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
              (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) sorry) :
          S) *
        eval₂ (algebraMap R S)
          (HMul.hMul (α := S)
            ((algebraMap R S : (a : R) → S)
                (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                      ((fun (x : ℕ) ↦ t ^ x) n) sorry) :
                  R) :
              S)
            r)
          p =
      0),
  ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
Tactic: obtain ⟨⟨x, m, (rfl : algebraMap R S t ^ m = x)⟩, e⟩ := hp'
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) t) : Submonoid S) x)
            (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) t : S) m) ⋯) :
        S) *
      eval₂ (algebraMap R S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x)
                    ((fun (x : ℕ) ↦ t ^ x) n) ⋯) :
                R) :
            S)
          r)
        p =
    0
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
have pos : ∀ (hp' : 1 ≤ p.natDegree),
  ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S)
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) t ht) : R) ^ n • r)
Tactic: by_cases hp' : 1 ≤ p.natDegree