awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
      (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)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
have this₁ : Module.Finite R (AdjoinRoot 𝓟.f)
Tactic: have := 𝓟.monic_f.finite_adjoinRoot
-- 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_1 :
  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)
      (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)
this : Module.Finite R (AdjoinRoot 𝓟.f)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
have suffices : Eq.{u_2 + 1} (α := S)
  ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
      ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
    S)
  ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S)
Tactic: suffices algebraMap (AdjoinRoot 𝓟.f) S (.mk _ 𝓟.g) = aeval 𝓟.x 𝓟.g from
      ⟨m, fun k ↦ this ▸ isIntegral_trans (R := R) _ (hm k)⟩
-- 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
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a
have obtain : ∀ (n : ℕ) (hx : ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)),
  Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a
Tactic: obtain ⟨n, hx⟩ : ∃ n, ∀ m, IsIntegral R ((aeval 𝓟.x 𝓟.g) ^ (n + m) • a) := by
    let e := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
    algebraize [(e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) _)).toRingHom]
    have := IsLocalization.isLocalization_of_algEquiv (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g))
      { toRingEquiv := e.symm.toRingEquiv, commutes' := by simp [RingHom.algebraMap_toAlgebra] }
    obtain ⟨⟨_, m, rfl⟩, hm⟩ := IsIntegral.exists_multiple_integral_of_isLocalization
      (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g)) _ hx
    replace hm := fun k : ℕ ↦ (isIntegral_algebraMap (x := AdjoinRoot.mk 𝓟.f 𝓟.g ^ k)).mul hm
    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
    simp_rw [map_pow] at hm
    have := 𝓟.monic_f.finite_adjoinRoot
    suffices algebraMap (AdjoinRoot 𝓟.f) S (.mk _ 𝓟.g) = aeval 𝓟.x 𝓟.g from
      ⟨m, fun k ↦ this ▸ isIntegral_trans (R := R) _ (hm k)⟩
    simp [RingHom.algebraMap_toAlgebra, e, StandardEtalePair.equivAwayAdjoinRoot,
      ← aeval_def, ← aeval_algHom_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_1 : IsIntegral S a
𝓟 : StandardEtalePresentation R S
n : ℕ
hx : ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
𝓟' : 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
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a
have obtain : ∀ (a : B ⊗[R] S)
  (hx : IsIntegral S (A := S ⊗[R] B) ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B))
  (hx :
    ∀ (m : ℕ),
      IsIntegral R
        (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m))
          ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B))),
  Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B)))
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B)
Tactic: obtain ⟨a, rfl⟩ := (Algebra.TensorProduct.comm _ _ _).surjective a
Cleared hypotheses: a, hx_1, hx
-- 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
𝓟 : 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 : B ⊗[R] S
hx_1 : IsIntegral S (A := S ⊗[R] B) ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B)
hx :
  ∀ (m : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B))
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B)))
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B)
have obtain : ∀
  (a :
    Localization.Away (M := AdjoinRoot 𝓟'.f)
      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
  (hx :
    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) a) :
        S ⊗[R] B))
  (hx :
    ∀ (m : ℕ),
      IsIntegral R
        (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m))
          ((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)
                a) :
            S ⊗[R] B))),
  Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (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) a) :
      S ⊗[R] B)
Tactic: obtain ⟨a, rfl⟩ := e.symm.surjective a
Cleared hypotheses: a, hx_1, 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
𝓟 : 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)
have this : Module.Finite R (AdjoinRoot 𝓟.f)
Tactic: have := 𝓟.monic_f.finite_adjoinRoot
-- 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
𝓟 : 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 R (A := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)
have h : 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: convert! (Algebra.IsIntegral.isIntegral (R := R) (AdjoinRoot.mk 𝓟.f 𝓟.g)).map e
-- 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
𝓟 : 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)
have h₁ : ∀ (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: ext
-- 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
𝓟 : 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 (α := 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)
have this₁ : (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]
-- 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
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
have refine : Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
  ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
  (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
Tactic: refine ⟨toIntegralClosure_injective_of_flat, ?_⟩
-- 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
x : S ⊗[R] B
hx : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x
⊢ ∃ (a : TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)),
    (toIntegralClosure R S B : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B))) a =
      Subtype.mk (p := fun (x : S ⊗[R] B) ↦
        Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x) x hx
have simp : Membership.mem (γ := Subalgebra S (S ⊗[R] B))
  (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
      (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
        TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
    Subalgebra S (S ⊗[R] B))
  x
Tactic: simp only [toIntegralClosure, Subtype.ext_iff, AlgHom.coe_codRestrict, ← AlgHom.mem_range]