awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal @P
hPi : ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
this : Eq (α := R →+* S) (algebraMap R S) (comp (algebraMap R S) (id R))
⊢ P (id R)

Tactic:
apply hPi
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget @P
hP' : StableUnderCompositionWithLocalizationAwaySource @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
⊢ Eq (α := Ideal S) (Ideal.map f (Ideal.span s)) (Ideal.map (R := R) f ⊤)

Tactic:
apply_fun Ideal.map f at hs

Premises used: Ideal.map
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget @P
hP' : StableUnderCompositionWithLocalizationAwaySource @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
hs : Eq (α := Ideal S) (Ideal.map f (Ideal.span s)) (Ideal.map (R := R) f ⊤)
⊢ Eq (α := Ideal S) (Ideal.span ((⇑f : (a : R) → S) '' s)) ⊤

Tactic:
rw [Ideal.map_span, Ideal.map_top] at hs

Premises used: Ideal.map_span, Ideal.map_top
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget @P
hP' : StableUnderCompositionWithLocalizationAwaySource @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
hs : Eq (α := Ideal S) (Ideal.span ((⇑f : (a : R) → S) '' s)) ⊤
apply :
  ∀ (r : (↑((⇑f : (a : R) → S) '' s) : Type u)),
    P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
⊢ P f

Tactic:
apply hP _ _ hs
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget @P
hP' : StableUnderCompositionWithLocalizationAwaySource @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
hs : Eq (α := Ideal S) (Ideal.span ((⇑f : (a : R) → S) '' s)) ⊤
r : R
hr : r ∈ s
rw :
  P (S :=
    Localization.Away (M := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x) ((f : (a : R) → S) r)
              ⋯) :
          S) :
        S))
    (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := Submonoid.powers r)
        (Localization.Away (M := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x)
                  ((f : (a : R) → S) r) ⋯) :
              S) :
            S))
        f ⋯)
      (algebraMap R (Localization.Away r)))
rw₁ :
  LE.le (α := Submonoid R) (Submonoid.powers r)
    (Submonoid.comap (N := S) f (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S))
⊢ P (S :=
    Localization.Away (M := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x) ((f : (a : R) → S) r)
              ⋯) :
          S) :
        S))
    (comp
      (algebraMap S
        (Localization.Away (M := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x)
                  ((f : (a : R) → S) r) ⋯) :
              S) :
            S)))
      f)

Tactic:
rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r)
    (T := Submonoid.powers (f r))]

Premises used: IsLocalization.map_comp
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget @P
hP' : StableUnderCompositionWithLocalizationAwaySource @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
hs : Eq (α := Ideal S) (Ideal.span ((⇑f : (a : R) → S) '' s)) ⊤
r : R
hr : r ∈ s
a :
  P (R := Localization.Away r) (S :=
    Localization.Away (M := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x) ((f : (a : R) → S) r)
              ⋯) :
          S) :
        S))
    (IsLocalization.map (M := Submonoid.powers r)
      (Localization.Away (M := S)
        ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x)
                ((f : (a : R) → S) r) ⋯) :
            S) :
          S))
      f ⋯)
⊢ P (S :=
    Localization.Away (M := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x) ((f : (a : R) → S) r)
              ⋯) :
          S) :
        S))
    (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := Submonoid.powers r)
        (Localization.Away (M := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x)
                  ((f : (a : R) → S) r) ⋯) :
              S) :
            S))
        f ⋯)
      (algebraMap R (Localization.Away r)))

Tactic:
apply hP' _ r
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget @P
hP' : StableUnderCompositionWithLocalizationAwaySource @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
hs : Eq (α := Ideal S) (Ideal.span ((⇑f : (a : R) → S) '' s)) ⊤
r : R
hr : r ∈ s
⊢ P (R := Localization.Away r) (S :=
    Localization.Away (M := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x) ((f : (a : R) → S) r)
              ⋯) :
          S) :
        S))
    (IsLocalization.map (M := Submonoid.powers r)
      (Localization.Away (M := S)
        ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x)
                ((f : (a : R) → S) r) ⋯) :
            S) :
          S))
      f ⋯)

Tactic:
hs' ⟨r, hr⟩

Premises used: Subtype.mk, IsLocalization.Away.map
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget @P
hP' : StableUnderCompositionWithLocalizationAwaySource @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
hs : Eq (α := Ideal S) (Ideal.span ((⇑f : (a : R) → S) '' s)) ⊤
r : R
hr : r ∈ s
⊢ P (R := Localization.Away r) (S :=
    Localization.Away (M := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x) ((f : (a : R) → S) r)
              ⋯) :
          S) :
        S))
    (IsLocalization.map (M := Submonoid.powers r)
      (Localization.Away (M := S)
        ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' s) x)
                ((f : (a : R) → S) r) ⋯) :
            S) :
          S))
      f ⋯)

Tactic:
exact hs' ⟨r, hr⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
apply :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
⊢ P f

Tactic:
apply hP _ s hs
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
r : (↑s : Type u)
obtain :
  ∀ (Rᵣ Sᵣ : Type u) (w : CommRing Rᵣ) (w_1 : CommRing Sᵣ) (w_2 : Algebra R Rᵣ) (w_3 : Algebra S Sᵣ),
    IsLocalization.Away (↑r : R) Rᵣ →
      IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ →
        ∀ (fᵣ : Rᵣ →+* Sᵣ) (hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f) (hf : P fᵣ),
          P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
⊢ P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))

Tactic:
obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, fᵣ, hfᵣ, hf⟩ := hT r
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
r : (↑s : Type u)
Rᵣ Sᵣ : Type u
w : CommRing Rᵣ
w_1 : CommRing Sᵣ
w_2 : Algebra R Rᵣ
w_3 : Algebra S Sᵣ
w_4 : IsLocalization.Away (↑r : R) Rᵣ
w_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f
hf : P fᵣ
let : P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
⊢ P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))

Tactic:
let e₁ := (Localization.algEquiv (.powers r.val) Rᵣ).toRingEquiv
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
r : (↑s : Type u)
Rᵣ Sᵣ : Type u
w : CommRing Rᵣ
w_1 : CommRing Sᵣ
w_2 : Algebra R Rᵣ
w_3 : Algebra S Sᵣ
w_4 : IsLocalization.Away (↑r : R) Rᵣ
w_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f
hf : P fᵣ
e₁ : Localization (Submonoid.powers (↑r : R)) ≃+* Rᵣ :=
  AlgEquiv.toRingEquiv (Localization.algEquiv (Submonoid.powers (↑r : R)) Rᵣ)
e₂ : Sᵣ ≃+* Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) :=
  AlgEquiv.toRingEquiv (R := S)
    (AlgEquiv.symm
        (IsLocalization.algEquiv (Submonoid.powers ((f : (a : R) → S) (↑r : R)))
          (Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S)) Sᵣ) :
      Sᵣ ≃ₐ[S] Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S))
h :
  Eq (α := R →+* Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    (comp (Localization.awayMap f (↑r : R)) (algebraMap R (Localization.Away (↑r : R))))
    (((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom).comp (algebraMap R (Localization.Away (↑r : R))))
⊢ Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom

Tactic:
apply IsLocalization.ringHom_ext (.powers r.val)

Premises used: Submonoid.powers, Subtype.val, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
r : (↑s : Type u)
Rᵣ Sᵣ : Type u
w : CommRing Rᵣ
w_1 : CommRing Sᵣ
w_2 : Algebra R Rᵣ
w_3 : Algebra S Sᵣ
w_4 : IsLocalization.Away (↑r : R) Rᵣ
w_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f
hf : P fᵣ
e₁ : Localization (Submonoid.powers (↑r : R)) ≃+* Rᵣ :=
  AlgEquiv.toRingEquiv (Localization.algEquiv (Submonoid.powers (↑r : R)) Rᵣ)
e₂ : Sᵣ ≃+* Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) :=
  AlgEquiv.toRingEquiv (R := S)
    (AlgEquiv.symm
        (IsLocalization.algEquiv (Submonoid.powers ((f : (a : R) → S) (↑r : R)))
          (Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S)) Sᵣ) :
      Sᵣ ≃ₐ[S] Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S))
h :
  ∀ (x : R),
    Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
      ((comp (Localization.awayMap f (↑r : R)) (algebraMap R (Localization.Away (↑r : R))) :
            (a : R) → Localization.Away ((f : (a : R) → S) (↑r : R)))
          x :
        Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
      ((((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom).comp (algebraMap R (Localization.Away (↑r : R))) :
            (a : R) → Localization.Away ((f : (a : R) → S) (↑r : R)))
          x :
        Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
⊢ Eq (α := R →+* Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    (comp (Localization.awayMap f (↑r : R)) (algebraMap R (Localization.Away (↑r : R))))
    (((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom).comp (algebraMap R (Localization.Away (↑r : R))))

Tactic:
ext x
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
r : (↑s : Type u)
Rᵣ Sᵣ : Type u
w : CommRing Rᵣ
w_1 : CommRing Sᵣ
w_2 : Algebra R Rᵣ
w_3 : Algebra S Sᵣ
w_4 : IsLocalization.Away (↑r : R) Rᵣ
w_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f
hf : P fᵣ
e₁ : Localization (Submonoid.powers (↑r : R)) ≃+* Rᵣ :=
  AlgEquiv.toRingEquiv (Localization.algEquiv (Submonoid.powers (↑r : R)) Rᵣ)
e₂ : Sᵣ ≃+* Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) :=
  AlgEquiv.toRingEquiv (R := S)
    (AlgEquiv.symm
        (IsLocalization.algEquiv (Submonoid.powers ((f : (a : R) → S) (↑r : R)))
          (Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S)) Sᵣ) :
      Sᵣ ≃ₐ[S] Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S))
x : R
rw :
  Eq (α := Sᵣ) ((fᵣ.comp (algebraMap R Rᵣ) : (a : R) → Sᵣ) x : Sᵣ)
    ((algebraMap S Sᵣ : (a : S) → Sᵣ) ((f : (a : R) → S) x : S) : Sᵣ)
rw₁ :
  Eq (α := Sᵣ) ((comp (algebraMap S Sᵣ) f : (a : R) → Sᵣ) x : Sᵣ)
    ((algebraMap S Sᵣ : (a : S) → Sᵣ) ((f : (a : R) → S) x : S) : Sᵣ)
rw₂ rw₃ :
  Eq (α := Sᵣ) ((algebraMap S Sᵣ : (a : S) → Sᵣ) ((f : (a : R) → S) x : S) : Sᵣ)
    ((algebraMap S Sᵣ : (a : S) → Sᵣ) ((f : (a : R) → S) x : S) : Sᵣ)
⊢ Eq (α := Sᵣ) ((fᵣ : (a : Rᵣ) → Sᵣ) ((algebraMap R Rᵣ : (a : R) → Rᵣ) x : Rᵣ) : Sᵣ)
    ((algebraMap S Sᵣ : (a : S) → Sᵣ) ((f : (a : R) → S) x : S) : Sᵣ)

Tactic:
rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
r : (↑s : Type u)
Rᵣ Sᵣ : Type u
w : CommRing Rᵣ
w_1 : CommRing Sᵣ
w_2 : Algebra R Rᵣ
w_3 : Algebra S Sᵣ
w_4 : IsLocalization.Away (↑r : R) Rᵣ
w_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f
hf : P fᵣ
e₁ : Localization (Submonoid.powers (↑r : R)) ≃+* Rᵣ :=
  AlgEquiv.toRingEquiv (Localization.algEquiv (Submonoid.powers (↑r : R)) Rᵣ)
e₂ : Sᵣ ≃+* Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) :=
  AlgEquiv.toRingEquiv (R := S)
    (AlgEquiv.symm
        (IsLocalization.algEquiv (Submonoid.powers ((f : (a : R) → S) (↑r : R)))
          (Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S)) Sᵣ) :
      Sᵣ ≃ₐ[S] Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S))
x : R
⊢ Eq (α := Sᵣ) ((fᵣ : (a : Rᵣ) → Sᵣ) ((algebraMap R Rᵣ : (a : R) → Rᵣ) x : Rᵣ) : Sᵣ)
    ((algebraMap S Sᵣ : (a : S) → Sᵣ) ((f : (a : R) → S) x : S) : Sᵣ)

Tactic:
have : fᵣ ((algebraMap R Rᵣ) x) = algebraMap S Sᵣ (f x) := by
      rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso.{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
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ :
      IsLocalization.Away (↑r : R) Rᵣ) (_ : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ) (fᵣ :
      Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f), P fᵣ
r : (↑s : Type u)
Rᵣ Sᵣ : Type u
w : CommRing Rᵣ
w_1 : CommRing Sᵣ
w_2 : Algebra R Rᵣ
w_3 : Algebra S Sᵣ
w_4 : IsLocalization.Away (↑r : R) Rᵣ
w_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = comp (algebraMap S Sᵣ) f
hf : P fᵣ
e₁ : Localization (Submonoid.powers (↑r : R)) ≃+* Rᵣ :=
  AlgEquiv.toRingEquiv (Localization.algEquiv (Submonoid.powers (↑r : R)) Rᵣ)
e₂ : Sᵣ ≃+* Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) :=
  AlgEquiv.toRingEquiv (R := S)
    (AlgEquiv.symm
        (IsLocalization.algEquiv (Submonoid.powers ((f : (a : R) → S) (↑r : R)))
          (Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S)) Sᵣ) :
      Sᵣ ≃ₐ[S] Localization (M := S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S))
x : R
this :
  Eq (α := Sᵣ) ((fᵣ : (a : Rᵣ) → Sᵣ) ((algebraMap R Rᵣ : (a : R) → Rᵣ) x : Rᵣ) : Sᵣ)
    ((algebraMap S Sᵣ : (a : S) → Sᵣ) ((f : (a : R) → S) x : S) : Sᵣ)
⊢ Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((comp (Localization.awayMap f (↑r : R)) (algebraMap R (Localization.Away (↑r : R))) :
          (a : R) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        x :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom).comp (algebraMap R (Localization.Away (↑r : R))) :
          (a : R) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        x :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))

Tactic:
simp [-AlgEquiv.symm_toRingEquiv, e₂, e₁, Localization.awayMap, IsLocalization.Away.map, this]

Premises used: IsLocalization.Away.map, Localization.awayMap, AlgEquiv.symm_toRingEquiv