Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
H :
  ∀ (k : ℕ),
    e (1 ⊗ₜ[R] ((aeval 𝓟.x) 𝓟.g ^ k)) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g))) ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k)
this :
  IsIntegral R
    ((algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g))) ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ n * a))
⊢ ∃ k, IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)

Tactic:
obtain ⟨k, hk⟩ := IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap hfg this

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
H :
  ∀ (k : ℕ),
    e (1 ⊗ₜ[R] ((aeval 𝓟.x) 𝓟.g ^ k)) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g))) ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k)
this :
  IsIntegral R
    ((algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g))) ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ n * a))
k : ℕ
hk : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ n * a))
⊢ ∃ k, IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)