awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
refine_2 :
  ∀ (m₂ : R) (hm₂ : m₂ ∈ M) (hm₂s : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m₂ hm₂ • s)),
    ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
      HMul.hMul (β := ↥(integralClosure Rf Sf))
          (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
          ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
                (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
              (↑x.2 : ↥(integralClosure R S)) :
            ↥(integralClosure Rf Sf)) =
        (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          x.1
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1

Tactic:
obtain ⟨⟨m₂, hm₂⟩, hm₂s⟩ := IsIntegral.exists_multiple_integral_of_isLocalization M _ hs

Premises used: IsIntegral.exists_multiple_integral_of_isLocalization
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m₂ hm₂ • s)
⊢ IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)

Tactic:
simp only [Submonoid.smul_def, Algebra.smul_def] at hm₂s

Premises used: Submonoid.smul_def, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
simp :
  IsIntegral R
    (HMul.hMul (β := Sf) (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
      ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf))
⊢ IsIntegral.{u_1, u_6} R (A := Sf) ((algebraMap S Sf : (a : S) → Sf) (m₂ • x) : Sf)

Tactic:
simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← e, ← mul_assoc]

Premises used: mul_assoc, map_mul, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
⊢ IsIntegral R
    (HMul.hMul (β := Sf) (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
      ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf))

Tactic:
hm₂s.mul (.algebraMap (Algebra.IsIntegral.isIntegral _))

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.mul, IsIntegral.algebraMap
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
⊢ IsIntegral R
    (HMul.hMul (β := Sf) (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
      ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf))

Tactic:
exact hm₂s.mul (.algebraMap (Algebra.IsIntegral.isIntegral _))

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.mul, IsIntegral.algebraMap
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
refine_2 :
  ∀ (m₃ : R) (hm₃ : m₃ ∈ M) (hm₃s : IsIntegral R (m₃ • m₂ • x)),
    ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
      HMul.hMul (β := ↥(integralClosure Rf Sf))
          (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
          ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
                (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
              (↑x.2 : ↥(integralClosure R S)) :
            ↥(integralClosure Rf Sf)) =
        (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          x.1
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1

Tactic:
obtain ⟨m₃, hm₃, hm₃s⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (Sₘ := Sf)
      M (x := m₂ • x) <| by
        simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← e, ← mul_assoc]
        exact hm₂s.mul (.algebraMap (Algebra.IsIntegral.isIntegral _))

Premises used: IsLocalization.exists_isIntegral_smul_of_isIntegral_map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
m₃ : R
hm₃ : m₃ ∈ M
hm₃s : IsIntegral R (m₃ • m₂ • x)
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1

Tactic:
⟨⟨⟨_, hm₃s⟩, _, _, mul_mem hm₁ (mul_mem hm₂ hm₃), rfl⟩, ?_⟩

Premises used: Prod.mk, Subtype.mk, And.intro, Exists.intro, rfl, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
m₃ : R
hm₃ : m₃ ∈ M
hm₃s : IsIntegral R (m₃ • m₂ • x)
⊢ HMul.hMul (β := Sf)
      (HMul.hMul (α := Sf) (β := Sf) ((algebraMap S Sf : (a : S) → Sf) x : Sf)
        ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf))
      ((algebraMap R Sf : (a : R) → Sf) m₃ : Sf) =
    HMul.hMul (β := Sf)
      (HMul.hMul (α := Sf) (β := Sf) ((algebraMap R Sf : (a : R) → Sf) m₃ : Sf)
        ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf))
      ((algebraMap S Sf : (a : S) → Sf) x : Sf)

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
a : S
ha : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a
b : S
hb : Membership.mem (γ := Subalgebra R S) (integralClosure R S) b
e :
  Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
      ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
      ↥(integralClosure Rf Sf))
⊢ Eq (α := Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
          ↥(integralClosure Rf Sf)) :
      Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
          ↥(integralClosure Rf Sf)) :
      Sf)

Tactic:
have := congr(algebraMap _ Sf $e)
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
a : S
ha : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a
b : S
hb : Membership.mem (γ := Subalgebra R S) (integralClosure R S) b
e :
  Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
      ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
      ↥(integralClosure Rf Sf))
this :
  Eq (α := Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
          ↥(integralClosure Rf Sf)) :
      Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
          ↥(integralClosure Rf Sf)) :
      Sf)
⊢ Eq.{u_6 + 1} (α := Sf) ((algebraMap S Sf : (a : S) → Sf) a : Sf) ((algebraMap S Sf : (a : S) → Sf) b : Sf)

Tactic:
simpa only [← IsScalarTower.algebraMap_apply] using this

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
a : S
ha : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a
b : S
hb : Membership.mem (γ := Subalgebra R S) (integralClosure R S) b
e :
  Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
      ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
      ↥(integralClosure Rf Sf))
this :
  Eq (α := Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
          ↥(integralClosure Rf Sf)) :
      Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
          ↥(integralClosure Rf Sf)) :
      Sf)
⊢ Eq.{u_6 + 1} (α := Sf) ((algebraMap S Sf : (a : S) → Sf) a : Sf) ((algebraMap S Sf : (a : S) → Sf) b : Sf)

Tactic:
have : algebraMap S Sf a = algebraMap S Sf b := by
      simpa only [← IsScalarTower.algebraMap_apply] using this
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
f : R
inst_11 : Away f Rf
inst_12 : Away.{u_2, u_6} (R := S) ((algebraMap R S : (a : R) → S) f : S) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
⊢ IsLocalization.{u_2, u_6} (R := ↥(integralClosure R S))
    (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) (Submonoid.powers f)) ↥(integralClosure Rf Sf)

Tactic:
IsLocalization.integralClosure (S := S) (Rf := Rf) (Sf := Sf) (.powers f)

Premises used: Submonoid.powers, IsLocalization.integralClosure
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
f : R
inst_11 : Away f Rf
inst_12 : Away.{u_2, u_6} (R := S) ((algebraMap R S : (a : R) → S) f : S) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
h :
  Eq.{u_2 + 1} (α := Submonoid ↥(integralClosure R S))
    (Submonoid.powers ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f) :
      Submonoid ↥(integralClosure R S))
    (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) (Submonoid.powers f) : Submonoid ↥(integralClosure R S))
⊢ Away.{u_2, u_6} (R := ↥(integralClosure R S))
    ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    ↥(integralClosure Rf Sf)

Tactic:
convert! IsLocalization.integralClosure (S := S) (Rf := Rf) (Sf := Sf) (.powers f)

Premises used: Submonoid.powers, IsLocalization.integralClosure