awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
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
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ P (S :=
    (fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
        (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
          | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
          Type u))
      (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
    (comp
      (@comp _ (Localization.Away (↑a : S)) _ _ Semiring.toNonAssocSemiring _
        (algebraMap (Localization.Away (↑a : S)) (Localization.Away (↑b : Localization.Away (↑a : S))))
        (algebraMap S (Localization.Away (↑a : S))))
      f)

Tactic:
apply ht _ _ b.property

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦
      (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
    (e.toRingHom.comp f)

Tactic:
⟨e '' s, ?_, ?_⟩

Premises used: RingHom.Locally, Exists.intro, Set.image, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
refine_1 : Eq (α := Ideal T) (Ideal.span ((⇑e : (a : S) → T) '' s)) ⊤
refine_2 :
  ∀ (t : T),
    Membership.mem (γ := Set T) ((⇑e : (a : S) → T) '' s) t →
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
        (comp (algebraMap T (Localization.Away t)) (e.toRingHom.comp f))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
refine ⟨e '' s, ?_, ?_⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
refine_1 : Eq (α := Ideal T) (Ideal.map e (Ideal.span s)) ⊤
refine_1₁ : Eq (α := Ideal T) (Ideal.map (R := S) e ⊤) ⊤
refine_1₂ refine_1₃ : Eq.{u + 1} (α := Ideal T) ⊤ ⊤
⊢ Eq (α := Ideal T) (Ideal.span ((⇑e : (a : S) → T) '' s)) ⊤

Tactic:
rw [← Ideal.map_span, hsone, Ideal.map_top]

Premises used: Ideal.map_span, Ideal.map_top
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
refine_2 :
  P (S := Localization.Away (M := T) ((e : (a : S) → T) a : T))
    (comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) (e.toRingHom.comp f))
⊢ P (S := Localization.Away (M := T) ((e : (a : S) → T) a : T))
    (comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) (e.toRingHom.comp f))

Tactic:
let e' : Localization.Away a ≃+* Localization.Away (e a) :=
        IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a)
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
a₁ :
  ∀ (x : S),
    Eq (α := Localization.Away (M := T) ((e : (a : S) → T) a : T))
      ((comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom :
            (a_1 : S) → Localization.Away ((e : (a : S) → T) a))
          x :
        Localization.Away (M := T) ((e : (a : S) → T) a : T))
      ((e'.toRingHom.comp (algebraMap S (Localization.Away a)) : (a_1 : S) → Localization.Away ((e : (a : S) → T) a))
          x :
        Localization.Away (M := T) ((e : (a : S) → T) a : T))
⊢ comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))

Tactic:
ext x
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x_1 : CommRing R
x_2 : CommRing S
x_3 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
x : S
⊢ Eq (α := Localization.Away (M := T) ((e : (a : S) → T) a : T))
    ((comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom :
          (a_1 : S) → Localization.Away ((e : (a : S) → T) a))
        x :
      Localization.Away (M := T) ((e : (a : S) → T) a : T))
    ((e'.toRingHom.comp (algebraMap S (Localization.Away a)) : (a_1 : S) → Localization.Away ((e : (a : S) → T) a)) x :
      Localization.Away (M := T) ((e : (a : S) → T) a : T))

Tactic:
simp [e']
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
⊢ comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))

Tactic:
have : (algebraMap T (Localization.Away (e a))).comp e.toRingHom =
          e'.toRingHom.comp (algebraMap S (Localization.Away a)) := by
        ext x
        simp [e']
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
this :
  comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))
refine_2 : P (e'.toRingHom.comp (comp (algebraMap S (Localization.Away a)) f))
⊢ P (S := Localization.Away (M := T) ((e : (a : S) → T) a : T))
    (comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) (e.toRingHom.comp f))

Tactic:
rw [← RingHom.comp_assoc, this, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
this :
  comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))
refine_2 : P (S := Localization.Away a) (comp (algebraMap S (Localization.Away a)) f)
⊢ P (e'.toRingHom.comp (comp (algebraMap S (Localization.Away a)) f))

Tactic:
apply hPi.left

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
this :
  comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P (S := Localization.Away a) (comp (algebraMap S (Localization.Away a)) f)

Tactic:
hs a ha
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
this :
  comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P (S := Localization.Away a) (comp (algebraMap S (Localization.Away a)) f)

Tactic:
exact hs a ha
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{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
h :
  ∃ (_ : Eq (α := Ideal S) (Ideal.span {1}) ⊤),
    ∀ (t : S),
      Membership.mem (γ := Set S) {1} t →
        (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
          (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away t)) (algebraMap R S))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R S)

Tactic:
use {1}
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{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
h :
  P (S := Localization.Away (M := S) 1)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away (M := S) 1)) (algebraMap R S))
⊢ ∃ (_ : Eq (α := Ideal S) (Ideal.span {1}) ⊤),
    ∀ (t : S),
      Membership.mem (γ := Set S) {1} t →
        (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
          (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away t)) (algebraMap R S))

Tactic:
simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]

Premises used: Ideal.span_singleton_one, forall_eq, Set.mem_singleton_iff, exists_const
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{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
⊢ LE.le (α := Submonoid S) (Submonoid.powers 1) (IsUnit.submonoid S)

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{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
h :
  P (S := Localization.Away (M := S) 1)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away (M := S) 1)) (algebraMap R S))
⊢ P (S := Localization.Away (M := S) 1)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away (M := S) 1)) (algebraMap R S))

Tactic:
let e : S ≃ₐ[R] (Localization.Away (1 : S)) :=
    (IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).restrictScalars R
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{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
e : S ≃ₐ[R] Localization.Away (M := S) 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
⊢ IsLocalization.Away r (Localization.Away (M := S) 1)

Tactic:
haveI : IsLocalization.Away r (Localization.Away (1 : S)) :=
    IsLocalization.isLocalization_of_algEquiv (Submonoid.powers r) e
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{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
e : S ≃ₐ[R] Localization.Away (M := S) 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away (M := S) 1)
h : P (S := Localization.Away (M := S) 1) (algebraMap R (Localization.Away (M := S) 1))
⊢ P (S := Localization.Away (M := S) 1)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away (M := S) 1)) (algebraMap R S))

Tactic:
rw [← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{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
e : S ≃ₐ[R] Localization.Away (M := S) 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away (M := S) 1)
⊢ P (S := Localization.Away (M := S) 1) (algebraMap R (Localization.Away (M := S) 1))

Tactic:
apply hPa _ r
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          g →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          (g.comp f)
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          g →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          (g.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
_ :
  ∀ [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          g →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          (g.comp f)
⊢ ∀ [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          g →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          (g.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
_ :
  ∀ [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          g →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          (g.comp f)
⊢ ∀ [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          g →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          (g.comp f)

Tactic:
_