awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H :
  ∀ (a : (↑s : Type u)),
    LE.le (α := Submonoid S) (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S)
      (Submonoid.comap (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.powers (rₐ a)) :
        Submonoid S)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦ toAlgebra (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
a : (↑s : Type u)
refine_3 :
  P (R := R') (S := Sₐ a)
    (IsLocalization.map (M := Submonoid.powers r) (P := Localization.Away (↑a : S)) (T := Submonoid.powers (rₐ a))
      (Sₐ a) (comp (algebraMap S (Localization.Away (↑a : S))) f) ⋯)
⊢ P (S := Sₐ a) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₐ a)) (IsLocalization.Away.map R' S' f r))

Tactic:
rw [algebraMap_toAlgebra, IsLocalization.Away.map, IsLocalization.map_comp_map]

Premises used: IsLocalization.map_comp_map, IsLocalization.Away.map, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H :
  ∀ (a : (↑s : Type u)),
    LE.le (α := Submonoid S) (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S)
      (Submonoid.comap (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.powers (rₐ a)) :
        Submonoid S)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦ toAlgebra (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
a : (↑s : Type u)
⊢ P (R := R') (S := Sₐ a)
    (IsLocalization.map (M := Submonoid.powers r) (P := Localization.Away (↑a : S)) (T := Submonoid.powers (rₐ a))
      (Sₐ a) (comp (algebraMap S (Localization.Away (↑a : S))) f) ⋯)

Tactic:
hPl ((algebraMap _ (Localization.Away a.val)).comp f) r R' (Sₐ a) (hs _ a.2)

Premises used: Algebra.algebraMap, Localization.Away, RingHom.comp, IsLocalization.Away.map, Quotient.mk', Subtype.val, OreLocalization.oreDiv, Subtype.property
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H :
  ∀ (a : (↑s : Type u)),
    LE.le (α := Submonoid S) (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S)
      (Submonoid.comap (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.powers (rₐ a)) :
        Submonoid S)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦ toAlgebra (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
a : (↑s : Type u)
⊢ P (R := R') (S := Sₐ a)
    (IsLocalization.map (M := Submonoid.powers r) (P := Localization.Away (↑a : S)) (T := Submonoid.powers (rₐ a))
      (Sₐ a) (comp (algebraMap S (Localization.Away (↑a : S))) f) ⋯)

Tactic:
exact hPl ((algebraMap _ (Localization.Away a.val)).comp f) r R' (Sₐ a) (hs _ a.2)

Premises used: Algebra.algebraMap, Localization.Away, RingHom.comp, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
obtain :
  ∀ (s : Set S) (hsone : Eq (α := Ideal S) (Ideal.span s) ⊤)
    (hs :
      ∀ t ∈ s,
        (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
          (comp (algebraMap S (Localization.Away t)) f)),
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (R := R') (IsLocalization.map S' f ⋯)
⊢ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (R := R') (IsLocalization.map S' f ⋯)

Tactic:
obtain ⟨s, hsone, hs⟩ := hf
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
rw :
  ∃ (ι : Type u) (s : ι → S') (_ : Eq (α := Ideal S') (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S' (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι),
      P (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
⊢ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (R := R') (IsLocalization.map S' f ⋯)

Tactic:
rw [locally_iff_exists hPl.away.respectsIso]

Premises used: RingHom.LocalizationAwayPreserves.respectsIso, RingHom.locally_iff_exists, RingHom.LocalizationPreserves.away
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
⊢ ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a

Tactic:
have hM (a : s) : M.map ((algebraMap S (Localization.Away a.val)).comp f) = Mₐ a :=
    (M.map_map _ _).symm
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
a : (↑s : Type u)
rw : IsLocalization (Mₐ a) (Sₐ a)
⊢ IsLocalization
    (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
    (Sₐ a)

Tactic:
rw [hM]
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
a : (↑s : Type u)
⊢ IsLocalization (Mₐ a) (Sₐ a)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
⊢ ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)

Tactic:
haveI (a : s) :
      IsLocalization (M.map ((algebraMap S (Localization.Away a.val)).comp f)) (Sₐ a) := by
    rw [hM]
    infer_instance
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
⊢ ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)

Tactic:
haveI (a : s) :
      IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) (M.map f)) (Sₐ a) :=
    inferInstanceAs <| IsLocalization (Mₐ a) (Sₐ a)
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
⊢ ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)

Tactic:
haveI (a : s) : IsScalarTower S S' (Sₐ a) :=
    IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (M.map f).le_comap_map).symm
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
⊢ ∃ (ι : Type u) (s : ι → S') (_ : Eq (α := Ideal S') (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S' (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι),
      P (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))

Tactic:
⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ,
      inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩

Premises used: Algebra.algebraMap, inferInstance, Set.Elem, Exists.intro, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
refine_1 :
  Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
refine_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away.{u, u} (R := S')
      ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a) (Sₐ a)
refine_3 :
  ∀ (a : (↑s : Type u)),
    P (R := R') (S := Sₐ a)
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₐ a)) (IsLocalization.map S' f ⋯))
⊢ ∃ (ι : Type u) (s : ι → S') (_ : Eq (α := Ideal S') (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S' (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι),
      P (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))

Tactic:
refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ,
      inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩