awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ 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]
-- 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))
this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
rw : P ((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom)
⊢ P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))

Tactic:
rw [this]
-- 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))
this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
x : P (e₂.toRingHom.comp fᵣ)
⊢ P ((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom)

Tactic:
apply hPi.right

Premises used: And.right
-- 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))
this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
x : P fᵣ
⊢ P (e₂.toRingHom.comp fᵣ)

Tactic:
apply hPi.left

Premises used: And.left
-- 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))
this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
⊢ P fᵣ

Tactic:
hf
-- 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))
this : Localization.awayMap f (↑r : R) = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
⊢ P fᵣ

Tactic:
exact hf
-- 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ᵣ) (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))
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ᵣ
⊢ P f

Tactic:
apply hP.ofIsLocalization hPi _ s hs

Premises used: RingHom.OfLocalizationSpan.ofIsLocalization
-- 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ᵣ) (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)
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ᵣ
⊢ ∃ (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
-- 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ᵣ) (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ᵣ 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:
⟨Rᵣ, Sᵣ, inferInstance, inferInstance, inferInstance, inferInstance,
    inferInstance, inferInstance, IsLocalization.Away.map Rᵣ Sᵣ f r, IsLocalization.map_comp _, hf⟩

Premises used: IsLocalization.map_comp, inferInstance, IsLocalization.Away.map, Exists.intro, Subtype.val
-- 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ᵣ) (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ᵣ 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:
exact ⟨Rᵣ, Sᵣ, inferInstance, inferInstance, inferInstance, inferInstance,
    inferInstance, inferInstance, IsLocalization.Away.map Rᵣ Sᵣ f r, IsLocalization.map_comp _, hf⟩
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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)
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)
⊢ 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 : 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)
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)
⊢ P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)

Tactic:
obtain ⟨T, _, _, _, hT⟩ := hT r
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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)
⊢ (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) R (Localization (Submonoid.powers (↑r : S)))
    _ _
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
      (comp (algebraMap S T) f))

Tactic:
hP'.1 _ (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT

Premises used: AlgEquiv.symm, Localization.algEquiv, And.left, Submonoid.powers, AlgEquiv.toRingEquiv, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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 _ _ _ _ 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)))
⊢ P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)

Tactic:
convert! hP'.1 _ (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT

Premises used: AlgEquiv.symm, Localization.algEquiv, And.left, Submonoid.powers, AlgEquiv.toRingEquiv, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {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
hQ : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) _ (Localization.Away (↑r : S)) _ _
      (comp (algebraMap S (Localization.Away (↑r : S))) f)
⊢ P f ∧ Q f

Tactic:
⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {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
hQ : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) _ (Localization.Away (↑r : S)) _ _
      (comp (algebraMap S (Localization.Away (↑r : S))) f)
⊢ P f ∧ Q f

Tactic:
exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {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
hQ : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
⊢ P f ∧ Q f

Tactic:
⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {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
hQ : OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
⊢ P f ∧ Q f

Tactic:
exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩