awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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))
⊢ P f
have hs₁ : Eq (α := Ideal S) (Ideal.map f (Ideal.span s)) (Ideal.map (R := R) f ⊤)
Tactic: apply_fun Ideal.map f at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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 ⊤)
⊢ P f
have hs₁ : Eq (α := Ideal S) (Ideal.span ((⇑f : (a : R) → S) '' s)) ⊤
Tactic: rw [Ideal.map_span, Ideal.map_top] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)) ⊤
⊢ P f
have apply : ∀ (r : (↑((⇑f : (a : R) → S) '' s) : Type u)),
  P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
Tactic: apply hP _ _ hs
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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 (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)
have 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)
            sorry) :
        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) sorry) :
            S) :
          S))
      f sorry)
    (algebraMap R (Localization.Away r)))
Tactic: rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r)
    (T := Submonoid.powers (f r))]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)))
⊢ 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)
have rw₁ : LE.le (α := Submonoid R) (Submonoid.powers r)
  (Submonoid.comap (N := S) f (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S))
Tactic: rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r)
    (T := Submonoid.powers (f r))]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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 (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)))
have 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)
            sorry) :
        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)
              sorry) :
          S) :
        S))
    f sorry)
Tactic: apply hP' _ r
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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ᵣ
⊢ P f
have 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))
Tactic: apply hP _ s hs
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)
⊢ P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
have 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))
Tactic: obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, fᵣ, hfᵣ, hf⟩ := hT r
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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))
⊢ Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
have 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))))
Tactic: apply IsLocalization.ringHom_ext (.powers r.val)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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))
⊢ 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))))
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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ᵣ)
have 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ᵣ)
Tactic: rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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ᵣ)
⊢ 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ᵣ)
have 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ᵣ)
Tactic: rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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ᵣ)
⊢ 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ᵣ)
have 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ᵣ)
Tactic: rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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 (α := 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))
have 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ᵣ)
Tactic: have : fᵣ ((algebraMap R Rᵣ) x) = algebraMap S Sᵣ (f x) := by
      rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]