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 : 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))
⊢ P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
have this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
Tactic: have : Localization.awayMap f r.val =
      (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom := by
    apply IsLocalization.ringHom_ext (.powers r.val)
    ext x
    have : fᵣ ((algebraMap R Rᵣ) x) = algebraMap S Sᵣ (f x) := by
      rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
    simp [-AlgEquiv.symm_toRingEquiv, e₂, e₁, Localization.awayMap, IsLocalization.Away.map, this]
-- 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))
this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
⊢ P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
have rw : P ((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom)
Tactic: rw [this]
-- 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))
this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
⊢ P ((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom)
have x : P (e₂.toRingHom.comp fᵣ)
Tactic: apply hPi.right
-- 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ᵣ) (x_4 :
      IsLocalization.Away (↑r : R) Rᵣ) (x_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ),
      P (IsLocalization.Away.map Rᵣ Sᵣ f (↑r : R))
⊢ P f
have apply : ∀ (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ᵣ
Tactic: apply hP.ofIsLocalization hPi _ 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ᵣ) (x_4 :
      IsLocalization.Away (↑r : R) Rᵣ) (x_5 : IsLocalization.Away (R := S) ((f : (a : R) → S) (↑r : R) : S) Sᵣ),
      P (IsLocalization.Away.map Rᵣ Sᵣ f (↑r : R))
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ᵣ
have obtain : ∀ (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ᵣ)
  (hf : P (IsLocalization.Away.map Rᵣ Sᵣ f (↑r : R))),
  ∃ (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ᵣ
Tactic: obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, 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 : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) 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 : S)) _ _
    (comp (algebraMap S (Localization.Away (↑r : S))) f)
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 : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
⊢ P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
have obtain : ∀ (T : Type u) (w : CommRing T) (w_1 : Algebra S T),
  IsLocalization.Away (↑r : S) T →
    ∀ (hT : P (comp (algebraMap S T) f)),
      P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
Tactic: obtain ⟨T, _, _, _, hT⟩ := 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 : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
⊢ P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
have h : Eq (α := R →+* Localization.Away (↑r : S))
  (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
  (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
      (comp (algebraMap S T) f) :
    R →+* Localization (Submonoid.powers (↑r : S)))
Tactic: convert! hP'.1 _ (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT
-- 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.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
⊢ Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (comp (algebraMap S T) f) :
      R →+* Localization (Submonoid.powers (↑r : S)))
have h : Eq (α := R →+* Localization.Away (↑r : S))
  (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
  (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (algebraMap S T))
      f :
    R →+* Localization (Submonoid.powers (↑r : S)))
Tactic: rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]
-- 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.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
h :
  Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (comp
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _
          (RingEquiv.toRingHom
            (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
          (algebraMap S T))
        f :
      R →+* Localization (Submonoid.powers (↑r : S)))
⊢ Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (comp (algebraMap S T) f) :
      R →+* Localization (Submonoid.powers (↑r : S)))
have h₁ : Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
  (comp
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))) :
        T →+* Localization (Submonoid.powers (↑r : S)))
      (algebraMap S T))
    f)
Tactic: rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]
-- 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.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
h :
  Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (comp
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _
          (RingEquiv.toRingHom
            (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
          (algebraMap S T))
        f :
      R →+* Localization (Submonoid.powers (↑r : S)))
h₁ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
⊢ Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (comp (algebraMap S T) f) :
      R →+* Localization (Submonoid.powers (↑r : S)))
have h₂ : Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
  (comp
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T)) :
        T →+* Localization (Submonoid.powers (↑r : S)))
      (algebraMap S T))
    f)
Tactic: rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]
-- 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.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
h :
  Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (comp
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _
          (RingEquiv.toRingHom
            (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
          (algebraMap S T))
        f :
      R →+* Localization (Submonoid.powers (↑r : S)))
h₁ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
h₂ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T)) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
⊢ Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (comp (algebraMap S T) f) :
      R →+* Localization (Submonoid.powers (↑r : S)))
have h₃ : Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
  (comp
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := Submonoid.powers (↑r : S)) (T := Submonoid.powers (↑r : S))
        (Localization (Submonoid.powers (↑r : S))) (id S) sorry)
      (algebraMap S T))
    f)
Tactic: rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]
-- 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.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : 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 S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
h :
  Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (comp
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _
          (RingEquiv.toRingHom
            (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
          (algebraMap S T))
        f :
      R →+* Localization (Submonoid.powers (↑r : S)))
h₁ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
h₂ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T)) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
h₃ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (M := Submonoid.powers (↑r : S)) (T := Submonoid.powers (↑r : S))
          (Localization (Submonoid.powers (↑r : S))) (id S) ⋯)
        (algebraMap S T))
      f)
⊢ Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (comp (algebraMap S T) f) :
      R →+* Localization (Submonoid.powers (↑r : S)))
have h₄ : Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
  (comp (comp (algebraMap S (Localization (Submonoid.powers (↑r : S)))) (id S)) f)
Tactic: rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]