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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ eval₂ (algebraMap R S) t q' =
    t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)

Tactic:
simp [φ, q', Polynomial.sum, ← aeval_def, this, mul_left_comm _ (t ^ N), ← Finset.mul_sum]

Premises used: Finset.mul_sum, Polynomial.sum, mul_left_comm, Polynomial.aeval_def, HPow.hPow
-- 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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
simp_rw :
  (q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (α := S) ((φ.toRingHom : (a : R[X]) → S) x2 : S) (t ^ x1)) * t ^ N = 0
simp_rw₁ : eval₂ φ.toRingHom t q * t ^ N = 0
simp_rw₂ : 0 * t ^ N = 0
⊢ (t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)) = 0

Tactic:
simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]

Premises used: MulZeroClass.zero_mul, HPow.hPow, mul_comm, Polynomial.eval₂_eq_sum
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
hx : IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
obtain :
  ∀ (p : R[X]) (hpm : p.Monic) (hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0), IsIntegral R x
⊢ IsIntegral R x

Tactic:
obtain ⟨p, hpm, hp⟩ := hx
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0
⊢ ∃ (a : ℕ), x ^ a * eval₂ (algebraMap R S) x p = 0

Tactic:
simp only [IsScalarTower.algebraMap_eq R S Sₘ, IsLocalization.map_eq_zero_iff (.powers x),
    Subtype.exists, Submonoid.mem_powers_iff, ← hom_eval₂, exists_prop, exists_exists_eq_and] at hp

Premises used: Polynomial.hom_eval₂, IsLocalization.map_eq_zero_iff, Subtype.exists, exists_prop, exists_exists_eq_and, Submonoid.powers, IsScalarTower.algebraMap_eq, Submonoid.mem_powers_iff
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : ∃ (a : ℕ), x ^ a * eval₂ (algebraMap R S) x p = 0
obtain : ∀ (n : ℕ) (hn : x ^ n * eval₂ (algebraMap R S) x p = 0), IsIntegral R x
⊢ IsIntegral R x

Tactic:
obtain ⟨n, hn⟩ := hp
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
p : R[X]
hpm : p.Monic
n : ℕ
hn : x ^ n * eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x (HPow.hPow (α := R[X]) X n * p) = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
p : R[X]
hpm : p.Monic
n : ℕ
hn : x ^ n * eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R x

Tactic:
exact ⟨X ^ n * p, (monic_X_pow n).mul hpm, by simpa⟩
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : Eq.{u_6 + 1} (α := C) ((algebraMap A C : (a : A) → C) x : C) (0 : C)
rw : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) x : C) : L) (0 : L)
rw₁ : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) 0 : L) (0 : L)
rw₂ rw₃ : Eq.{u_5 + 1} (α := L) 0 0
⊢ Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L)

Tactic:
rw [IsScalarTower.algebraMap_apply A C L, h, map_zero]

Premises used: map_zero, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
rw :
  HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    x • z
rw₁ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) x : L) = x • z
rw₂ :
  HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) x : L) =
    HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) x : L) z
rw₃ rw₄ :
  HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) x : L) z =
    HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) x : L) z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((mk' C (x • z) int,
            Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
              ((algebraMap A C : (a : A) → C) x) ⋯) :
          C × ↥(nonZeroDivisors C : Submonoid C)).1

Tactic:
rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]

Premises used: IsIntegralClosure.algebraMap_mk', mul_comm, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
x y : C
h : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) x : L) ((algebraMap C L : (a : C) → L) y : L)
⊢ (↑1 : C) * x = (↑1 : C) * y

Tactic:
simpa using algebraMap_injective C A L h

Premises used: IsIntegralClosure.algebraMap_injective
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
inst : CommRing A
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra A L
inst_5 : IsFractionRing A K
C : Type u_6
inst_6 : CommRing C
inst_7 : IsDomain C
inst_8 : Algebra C L
inst_9 : IsIntegralClosure C A L
inst_10 : Algebra A C
inst_11 : IsScalarTower A C L
inst_12 : IsDomain A
inst_13 : Algebra K L
inst_14 : IsScalarTower A K L
inst_15 : FiniteDimensional K L
⊢ IsFractionRing C L

Tactic:
have : Algebra.IsAlgebraic A L := IsFractionRing.comap_isAlgebraic_iff.mpr
    (inferInstance : Algebra.IsAlgebraic K L)
  isFractionRing_of_algebraic A C
    fun _ hx =>
    IsFractionRing.to_map_eq_zero_iff.mp
      ((map_eq_zero <| algebraMap K L).mp <| (IsScalarTower.algebraMap_apply _ _ _ _).symm.trans hx)

Premises used: Iff.mpr, Algebra.algebraMap, inferInstance, IsFractionRing.to_map_eq_zero_iff, map_eq_zero, IsIntegralClosure.isFractionRing_of_algebraic, Iff.mp, IsFractionRing.comap_isAlgebraic_iff, Eq.symm, IsScalarTower.algebraMap_apply, Eq.trans
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
inst_3 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
⊢ IsFractionRing (↥(integralClosure A L)) L

Tactic:
IsIntegralClosure.isFractionRing_of_algebraic A (integralClosure A L) inj

Premises used: Set.Mem, Membership.mem, Subtype, integralClosure, IsIntegralClosure.isFractionRing_of_algebraic
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
A : Type u_3
K : Type u_4
inst : CommRing A
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDomain A
inst_6 : Algebra A L
inst_7 : Algebra K L
inst_8 : IsScalarTower A K L
inst_9 : FiniteDimensional K L
⊢ IsFractionRing (↥(integralClosure A L)) L

Tactic:
IsIntegralClosure.isFractionRing_of_finite_extension A K L (integralClosure A L)

Premises used: IsIntegralClosure.isFractionRing_of_finite_extension, Set.Mem, Membership.mem, Subtype, 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
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)
⊢ IsLocalization.{u_2, u_6} (R := ↥(integralClosure R S)) (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)
    ↥(integralClosure Rf Sf)

Tactic:
⟨⟨?_, ?_, ?_⟩⟩

Premises used: IsLocalization'.mk, Submonoid.IsLocalizationMap.mk
-- 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)
refine_1 :
  ∀ (y : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    IsUnit.{u_6} (M := ↥(integralClosure Rf Sf))
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          (↑y : ↥(integralClosure R S)) :
        ↥(integralClosure Rf Sf))
refine_2 :
  ∀ (z : ↥(integralClosure Rf Sf)),
    ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
      HMul.hMul (β := ↥(integralClosure Rf Sf)) z
          ((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
refine_3 :
  ∀ {x y : ↥(integralClosure R S)},
    Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            x :
          ↥(integralClosure Rf Sf))
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            y :
          ↥(integralClosure Rf Sf)) →
      ∃ (c : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
        (↑c : ↥(integralClosure R S)) * x = (↑c : ↥(integralClosure R S)) * y
⊢ IsLocalization.{u_2, u_6} (R := ↥(integralClosure R S)) (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)
    ↥(integralClosure Rf Sf)

Tactic:
refine ⟨⟨?_, ?_, ?_⟩⟩
-- 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)
f : R
hf : f ∈ (↑M : Set R)
⊢ IsUnit.{u_6} (M := ↥(integralClosure Rf Sf))
    ((algebraMap Rf ↥(integralClosure Rf Sf) : (a : Rf) → ↥(integralClosure Rf Sf))
        ((algebraMap R Rf : (a : R) → Rf) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) f hf) : R)) :
      ↥(integralClosure Rf Sf))

Tactic:
(IsLocalization.map_units (S := Rf) ⟨f, hf⟩).map (algebraMap Rf (integralClosure Rf Sf))

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Subtype.mk, integralClosure, IsLocalization.map_units, IsUnit.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)
f : R
hf : f ∈ (↑M : Set R)
h :
  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 : ↥(integralClosure R S)) ↦
              Membership.mem (γ := Submonoid ↥(integralClosure R S))
                (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
              ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f) ⋯) :
          ↥(integralClosure R S)) :
      ↥(integralClosure Rf Sf))
    ((algebraMap Rf ↥(integralClosure Rf Sf) : (a : Rf) → ↥(integralClosure Rf Sf))
        ((algebraMap R Rf : (a : R) → Rf) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) f hf) : R)) :
      ↥(integralClosure Rf Sf))
⊢ IsUnit.{u_6} (M := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (↑(Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
              Membership.mem (γ := Submonoid ↥(integralClosure R S))
                (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
              ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f) ⋯) :
          ↥(integralClosure R S)) :
      ↥(integralClosure Rf Sf))

Tactic:
convert!
      (IsLocalization.map_units (S := Rf) ⟨f, hf⟩).map (algebraMap Rf (integralClosure Rf Sf))

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Subtype.mk, integralClosure, IsLocalization.map_units, IsUnit.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)
f : R
hf : f ∈ (↑M : Set R)
⊢ 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 : ↥(integralClosure R S)) ↦
              Membership.mem (γ := Submonoid ↥(integralClosure R S))
                (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
              ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f) ⋯) :
          ↥(integralClosure R S)) :
      ↥(integralClosure Rf Sf))
    ((algebraMap Rf ↥(integralClosure Rf Sf) : (a : Rf) → ↥(integralClosure Rf Sf))
        ((algebraMap R Rf : (a : R) → Rf) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) f hf) : R)) :
      ↥(integralClosure Rf Sf))

Tactic:
simp [← IsScalarTower.algebraMap_apply]

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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
refine_2 :
  ∀ (x : S) (m₁ : R) (hm₁ : m₁ ∈ (↑M : Set R))
    (e :
      HMul.hMul (β := Sf) s
          ((algebraMap S Sf : (a : S) → Sf)
              ((↑(x,
                        Subtype.mk (p := fun (x : S) ↦
                          Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                          ((algebraMap R S : (a : R) → S) m₁) ⋯).2 :
                  S) :
                S) :
            Sf) =
        (algebraMap S Sf : (a : S) → Sf)
          ((x,
                Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                  ((algebraMap R S : (a : R) → S) m₁) ⋯) :
              S × ↥(Algebra.algebraMapSubmonoid S M)).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
⊢ ∃ (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 ⟨⟨x, _, m₁, hm₁, rfl⟩, e⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid S M) s

Premises used: IsLocalization.surj, Algebra.algebraMapSubmonoid, rfl
-- 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 S Sf : (a : S) → Sf)
          ((↑(x,
                    Subtype.mk (p := fun (x : S) ↦
                      Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                      ((algebraMap R S : (a : R) → S) m₁) ⋯).2 :
              S) :
            S) :
        Sf) =
    (algebraMap S Sf : (a : S) → Sf)
      ((x,
            Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
              ((algebraMap R S : (a : R) → S) m₁) ⋯) :
          S × ↥(Algebra.algebraMapSubmonoid S M)).1
⊢ HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x

Tactic:
simp only [← IsScalarTower.algebraMap_apply] at e

Premises used: IsScalarTower.algebraMap_apply