awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S : Type u_1
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Injective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Injective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S : Type u_1
inst : CommRing R
_ : ∀ [inst_1 : CommRing S] (e : R ≃+* S), Function.Injective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
⊢ ∀ [inst_1 : CommRing S] (e : R ≃+* S), Function.Injective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
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:
e.bijective.injective

Premises used: Function.Bijective.injective, RingEquiv.bijective
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
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:
exact e.bijective.injective

Premises used: Function.Bijective.injective, RingEquiv.bijective
-- Module: Mathlib.RingTheory.RingHom.Integral
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 : f.IsIntegral
hg : g.IsIntegral
⊢ (g.comp f).IsIntegral

Tactic:
hf.trans _ _ hg

Premises used: RingHom.IsIntegral.trans
-- Module: Mathlib.RingTheory.RingHom.Integral
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 : f.IsIntegral
hg : g.IsIntegral
⊢ (g.comp f).IsIntegral

Tactic:
exact hf.trans _ _ hg

Premises used: RingHom.IsIntegral.trans
-- Module: Mathlib.RingTheory.RingHom.Integral
Goal:
apply : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsIntegral
⊢ RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral

Tactic:
apply isIntegral_stableUnderComposition.respectsIso

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.isIntegral_stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Integral
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
x : S
rw : e.toRingHom.IsIntegralElem ((e : (a : R) → S) ((e.symm : (a : S) → R) x : R))
⊢ e.toRingHom.IsIntegralElem x

Tactic:
rw [← e.apply_symm_apply x]

Premises used: RingEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.RingHom.Integral
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem ((e : (a : R) → S) ((e.symm : (a : S) → R) x : R))

Tactic:
apply RingHom.isIntegralElem_map

Premises used: RingHom.isIntegralElem_map
-- Module: Mathlib.RingTheory.RingHom.Integral
Goal:
⊢ IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral

Tactic:
IsStableUnderBaseChange.mk isIntegral_respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.isIntegral_respectsIso
-- Module: Mathlib.RingTheory.RingHom.Integral
Goal:
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))
⊢ IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral

Tactic:
refine IsStableUnderBaseChange.mk isIntegral_respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.isIntegral_respectsIso
-- Module: Mathlib.RingTheory.RingHom.Integral
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)
rw : ∀ (int : Algebra.IsIntegral R T), Algebra.IsIntegral S (S ⊗[R] T)
⊢ IsIntegral (A := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
rw [algebraMap_isIntegral_iff] at int ⊢

Premises used: algebraMap_isIntegral_iff
-- Module: Mathlib.RingTheory.RingHom.Integral
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 : Algebra.IsIntegral R T
⊢ Algebra.IsIntegral S (S ⊗[R] T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Integral
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
change :
  Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S) r
⊢ f.IsIntegralElem r

Tactic:
change r ∈ (integralClosure R S).toSubmodule

Premises used: integralClosure, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.Integral
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
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)
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (integralClosure R S) : Submodule R S) r

Tactic:
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ s hs

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem
-- Module: Mathlib.RingTheory.RingHom.Integral
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
⊢ 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
-- Module: Mathlib.RingTheory.RingHom.Integral
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))
⊢ _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)
-- Module: Mathlib.RingTheory.RingHom.Integral
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))
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) ⋯)
            ((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)
⊢ ∃ (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)

Premises used: IsIntegral.exists_multiple_integral_of_isLocalization, Submonoid.powers, rfl
-- Module: Mathlib.RingTheory.RingHom.Integral
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
⊢ ∃ (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

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'

Premises used: Polynomial.hom_eval₂, IsLocalization.map_eq_zero_iff, Submonoid.smul_def, map_mul, Submonoid.powers, IsScalarTower.algebraMap_eq, Algebra.smul_def, DFunLike.coe, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.RingHom.Integral
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
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) ⋯) :
            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)
⊢ ∃ (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'

Premises used: Algebra.algebraMap, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.RingHom.Integral
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
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)
neg :
  ∀ (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)
⊢ ∃ (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

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.RingHom.Integral
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
hp' : ¬1 ≤ p.natDegree
⊢ p.natDegree = 0

Tactic:
lia
-- Module: Mathlib.RingTheory.RingHom.Integral
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
hp' : ¬1 ≤ p.natDegree
⊢ Monic.{u_1} (R := R) 1

Tactic:
obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by lia)

Premises used: Polynomial.eq_one_of_monic_natDegree_zero, rfl
-- Module: Mathlib.RingTheory.RingHom.Integral
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
hp' : ¬1 ≤ p.natDegree
hp₁ : Monic.{u_1} (R := R) 1
⊢ (↑(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)
        1 =
    0

Tactic:
obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by lia)

Premises used: Polynomial.eq_one_of_monic_natDegree_zero, rfl