awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e_1 : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
this : Module.Finite R (AdjoinRoot 𝓟.f)
e : AlgHom.{u_1, u_1, u_3} R (AdjoinRoot 𝓟.f) (AdjoinRoot 𝓟'.f) := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
⊢ IsIntegral.{u_1, u_3} R (A := AdjoinRoot 𝓟'.f)
    ((e : (a : AdjoinRoot 𝓟.f) → AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) :
      AdjoinRoot 𝓟'.f)

Tactic:
(Algebra.IsIntegral.isIntegral (R := R) (AdjoinRoot.mk 𝓟.f 𝓟.g)).map e

Premises used: Algebra.IsIntegral.isIntegral, StandardEtalePresentation.P, StandardEtalePair.f, AdjoinRoot.mk, IsIntegral.map, StandardEtalePair.g, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e_1 : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
this : Module.Finite R (AdjoinRoot 𝓟.f)
e : AlgHom.{u_1, u_1, u_3} R (AdjoinRoot 𝓟.f) (AdjoinRoot 𝓟'.f) := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
x : R
⊢ Eq.{u_3 + 1} (α := AdjoinRoot 𝓟'.f)
    (((RingHom.comp ((AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B))) C :
            RingHom.{u_1, u_3} R (AdjoinRoot 𝓟'.f)) :
          (a : R) → AdjoinRoot 𝓟'.f)
        x :
      AdjoinRoot 𝓟'.f)
    (((e.comp (AdjoinRoot.mk 𝓟.f)).comp C : (a : R) → AdjoinRoot 𝓟'.f) x : AdjoinRoot 𝓟'.f)

Tactic:
simp [e]
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e_1 : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
this : Module.Finite R (AdjoinRoot 𝓟.f)
e : AlgHom.{u_1, u_1, u_3} R (AdjoinRoot 𝓟.f) (AdjoinRoot 𝓟'.f) := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
⊢ Eq.{u_3 + 1} (α := AdjoinRoot 𝓟'.f)
    ((((AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) : RingHom.{u_1, u_3} R[X] (AdjoinRoot 𝓟'.f)) :
        (a : R[X]) → AdjoinRoot 𝓟'.f)
      X)
    ((e.comp (AdjoinRoot.mk 𝓟.f) : (a : R[X]) → AdjoinRoot 𝓟'.f) X)

Tactic:
simp [e]
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e_1 : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
this : Module.Finite R (AdjoinRoot 𝓟.f)
e : AlgHom.{u_1, u_1, u_3} R (AdjoinRoot 𝓟.f) (AdjoinRoot 𝓟'.f) := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
⊢ (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) = e.comp (AdjoinRoot.mk 𝓟.f)

Tactic:
have : (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) =
        e.toRingHom.comp (AdjoinRoot.mk _) := by ext <;> simp [e]
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e_1 : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
this_1 : Module.Finite R (AdjoinRoot 𝓟.f)
e : AlgHom.{u_1, u_1, u_3} R (AdjoinRoot 𝓟.f) (AdjoinRoot 𝓟'.f) := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
this : (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) = e.comp (AdjoinRoot.mk 𝓟.f)
⊢ Eq (α := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)
    ((e : (a : AdjoinRoot 𝓟.f) → AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) :
      AdjoinRoot 𝓟'.f)

Tactic:
congr($this 𝓟.g)

Premises used: congrArg, StandardEtalePresentation.P, id, StandardEtalePair.g, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e_1 : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e_1.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
this_1 : Module.Finite R (AdjoinRoot 𝓟.f)
e : AlgHom.{u_1, u_1, u_3} R (AdjoinRoot 𝓟.f) (AdjoinRoot 𝓟'.f) := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
this : (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) = e.comp (AdjoinRoot.mk 𝓟.f)
⊢ Eq (α := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)
    ((e : (a : AdjoinRoot 𝓟.f) → AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) :
      AdjoinRoot 𝓟'.f)

Tactic:
exact congr($this 𝓟.g)
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
⊢ IsIntegral R (A := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)

Tactic:
have hfg : IsIntegral R (AdjoinRoot.mk 𝓟'.f 𝓟'.g) := by
    have := 𝓟.monic_f.finite_adjoinRoot
    let e : AdjoinRoot 𝓟.f →ₐ[R] AdjoinRoot 𝓟'.f :=
      AdjoinRoot.mapAlgHom (Algebra.ofId _ _) _ _ (dvd_refl _)
    convert! (Algebra.IsIntegral.isIntegral (R := R) (AdjoinRoot.mk 𝓟.f 𝓟.g)).map e
    have : (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) =
        e.toRingHom.comp (AdjoinRoot.mk _) := by ext <;> simp [e]
    exact congr($this 𝓟.g)
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
hfg : IsIntegral R (A := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)
g : R[X]
⊢ Eq (α := B ⊗[R] S) ((aeval (1 ⊗ₜ[R] 𝓟.x) : (a : R[X]) → B ⊗[R] S) g : B ⊗[R] S)
    ((aeval 𝓟'.x : (a : R[X]) → B ⊗[R] S) g : B ⊗[R] S)

Tactic:
rfl