awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (comp (algebraMap S T) f))
⊢ P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (comp (algebraMap S T) f))

Tactic:
letI : Algebra (Localization.Away a) (Localization.Away (algebraMap S T a)) :=
      (IsLocalization.Away.map _ _ (algebraMap S T) a).toAlgebra
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
⊢ Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))

Tactic:
simp [algebraMap_toAlgebra, IsLocalization.Away.map]

Premises used: IsLocalization.Away.map, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
⊢ Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))

Tactic:
have : (algebraMap (Localization.Away a) (Localization.Away (algebraMap S T a))).comp
        (algebraMap S (Localization.Away a)) =
        (algebraMap T (Localization.Away (algebraMap S T a))).comp (algebraMap S T) := by
      simp [algebraMap_toAlgebra, IsLocalization.Away.map]
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
refine_2 :
  P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (comp (algebraMap S (Localization.Away a)) f))
⊢ P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (comp (algebraMap S T) f))

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

Premises used: RingHom.comp_assoc
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
h :
  ∀ (x : S),
    Eq (α := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      ((algebraMap S (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :
            (a_1 : S) → Localization.Away ((algebraMap S T : (a : S) → T) a))
          x :
        Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      ((algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :
            (a_1 : Localization.Away a) → Localization.Away ((algebraMap S T : (a : S) → T) a))
          ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) x) :
        Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
⊢ IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))

Tactic:
apply IsScalarTower.of_algebraMap_eq

Premises used: IsScalarTower.of_algebraMap_eq
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
x : S
⊢ Eq (α := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    ((algebraMap S (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :
          (a_1 : S) → Localization.Away ((algebraMap S T : (a : S) → T) a))
        x :
      Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    ((algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :
          (a_1 : Localization.Away a) → Localization.Away ((algebraMap S T : (a : S) → T) a))
        ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) x) :
      Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))

Tactic:
simp [algebraMap_toAlgebra, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply]

Premises used: IsLocalization.Away.map, RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
⊢ IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))

Tactic:
haveI : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a)) := by
      apply IsScalarTower.of_algebraMap_eq
      intro x
      simp [algebraMap_toAlgebra, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this_2 :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
this : IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
⊢ IsLocalization.Away (R := Localization.Away a)
    ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) t : Localization.Away a)
    (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))

Tactic:
haveI : IsLocalization.Away (algebraMap S (Localization.Away a) t)
        (Localization.Away (algebraMap S T a)) :=
      IsLocalization.Away.commutes _ T ((Localization.Away (algebraMap S T a))) a t
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this_2 :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
this_3 : IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
this :
  IsLocalization.Away (R := Localization.Away a)
    ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) t : Localization.Away a)
    (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
refine_2 : P (S := Localization.Away a) (comp (algebraMap S (Localization.Away a)) f)
⊢ P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (comp (algebraMap S (Localization.Away a)) f))

Tactic:
apply hPa _ (algebraMap S (Localization.Away a) t)

Premises used: Algebra.algebraMap, Localization.Away, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
f : R →+* S
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
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this_2 :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
this_3 : IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
this :
  IsLocalization.Away (R := Localization.Away a)
    ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) t : Localization.Away a)
    (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
⊢ P (S := Localization.Away a) (comp (algebraMap S (Localization.Away a)) f)

Tactic:
apply hs a ha
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource.{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] [inst_3 : Algebra R S] (r : R)
    [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] (r : R)
    [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource.{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] [inst_3 : Algebra R S] (r : R) [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))
⊢ ∀ [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] (r : R) [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource.{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] [inst_3 : Algebra R S] (r : R) [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))
⊢ ∀ [inst_2 : CommRing T] [inst_3 : Algebra R S] (r : R) [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource.{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
_ :
  ∀ [inst_3 : Algebra R S] (r : R) [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))
⊢ ∀ [inst_3 : Algebra R S] (r : R) [IsLocalization.Away r S] (f : 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))
        (f.comp (algebraMap R S))

Tactic:
_