awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : 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))
⊢ ∀ [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_5 : 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
inst_4 : IsLocalization.Away r S
f : S →+* T
this :
  ∀ (s : Set T) (hsone : Eq (α := Ideal T) (Ideal.span s) ⊤)
    (hs :
      ∀ t ∈ s,
        (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
          (comp (algebraMap T (Localization.Away t)) f)),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R S))
⊢ (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:
⟨s, hsone, hs⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : 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
inst_4 : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Eq (α := Ideal T) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R S))

Tactic:
⟨s, hsone, fun t ht ↦ ?_⟩

Premises used: RingHom.Locally, Exists.intro
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : 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
inst_4 : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Eq (α := Ideal T) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) f)
refine :
  ∀ (t : T) (ht : t ∈ s),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) (f.comp (algebraMap R S)))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R S))

Tactic:
refine ⟨s, hsone, fun t ht ↦ ?_⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : 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
inst_4 : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Eq (α := Ideal T) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) f)
t : T
ht : t ∈ s
rw : P (S := Localization.Away t) (comp (comp (algebraMap T (Localization.Away t)) f) (algebraMap R S))
⊢ P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) (f.comp (algebraMap R S)))

Tactic:
rw [← 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 : 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
inst_4 : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Eq (α := Ideal T) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) f)
t : T
ht : t ∈ s
⊢ (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
    (comp (comp (algebraMap T (Localization.Away t)) f) (algebraMap R S))

Tactic:
hPa _ r _ (hs t ht)
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : 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
inst_4 : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Eq (α := Ideal T) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) f)
t : T
ht : t ∈ s
⊢ (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
    (comp (comp (algebraMap T (Localization.Away t)) f) (algebraMap R S))

Tactic:
exact hPa _ r _ (hs t ht)
-- 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
hPb : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
apply :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T) →
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P

Tactic:
apply IsStableUnderBaseChange.mk (locally_respectsIso hPi)

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.locally_respectsIso
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
rw :
  {g : T |
      P (S := Localization.Away g)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away g)) (algebraMap R T))} ⊆
    (↑(Ideal.comap (F := T →ₐ[R] S ⊗[R] T) Algebra.TensorProduct.includeRight
          (Ideal.span
            {g : S ⊗[R] T |
              P (S := Localization.Away g)
                (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
                  (algebraMap S (S ⊗[R] T)))})) :
      Set T)
⊢ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
rw [locally_iff_span_eq_top, eq_top_iff, ← Ideal.map_top Algebra.TensorProduct.includeRight,
    ← hf.span_eq_top, Ideal.map_le_iff_le_comap, Ideal.span_le]

Premises used: Ideal.span_le, eq_top_iff, RingHom.locally_iff_span_eq_top, RingHom.Locally.span_eq_top, Ideal.map_le_iff_le_comap, Ideal.map_top, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg :
  Membership.mem (γ := Set T)
    {g : T |
      P (S := Localization.Away g)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away g)) (algebraMap R T))}
    g
a :
  Membership.mem (α := S ⊗[R] T) (γ := Set (S ⊗[R] T))
    {g : S ⊗[R] T |
      P (S := Localization.Away g)
        (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
          (algebraMap S (S ⊗[R] T)))}
    ((Algebra.TensorProduct.includeRight : (a : T) → S ⊗[R] T) g : S ⊗[R] T)
⊢ g ∈
    (↑(Ideal.comap (F := T →ₐ[R] S ⊗[R] T) Algebra.TensorProduct.includeRight
          (Ideal.span
            {g : S ⊗[R] T |
              P (S := Localization.Away g)
                (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
                  (algebraMap S (S ⊗[R] T)))})) :
      Set T)

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg :
  Membership.mem (γ := Set T)
    {g : T |
      P (S := Localization.Away g)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away g)) (algebraMap R T))}
    g
a :
  ∀ (hg : P (S := Localization.Away g) (algebraMap R (Localization.Away g))),
    P (S := Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g))
      (algebraMap S (Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)))
⊢ Membership.mem (α := S ⊗[R] T) (γ := Set (S ⊗[R] T))
    {g : S ⊗[R] T |
      P (S := Localization.Away g)
        (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
          (algebraMap S (S ⊗[R] T)))}
    ((Algebra.TensorProduct.includeRight : (a : T) → S ⊗[R] T) g : S ⊗[R] T)

Tactic:
simp only [Set.mem_setOf_eq, Algebra.TensorProduct.includeRight_apply,
    ← IsScalarTower.algebraMap_eq] at hg ⊢

Premises used: Algebra.TensorProduct.includeRight_apply, Set.mem_setOf_eq, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (S := Localization.Away g) (algebraMap R (Localization.Away g))
a :
  P (S := Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)) (algebraMap S (Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)))
⊢ P (S := Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)) (algebraMap S (Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)))

Tactic:
let e := IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (S := Localization.Away g) (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
a :
  P
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑e : S ⊗[R] Localization.Away g →ₐ[S] Localization.Away (1 ⊗ₜ[R] g)) :
        S ⊗[R] Localization.Away g →+* Localization.Away (1 ⊗ₜ[R] g))
      (algebraMap S (S ⊗[R] Localization.Away g)))
⊢ P (S := Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)) (algebraMap S (Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)))

Tactic:
rw [← e.toAlgHom.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (S := Localization.Away g) (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
⊢ P
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑e : S ⊗[R] Localization.Away g →ₐ[S] Localization.Away (1 ⊗ₜ[R] g)) :
        S ⊗[R] Localization.Away g →+* Localization.Away (1 ⊗ₜ[R] g))
      (algebraMap S (S ⊗[R] Localization.Away g)))

Tactic:
hPi.left _ _ (hPb.tensorProduct _ hg)

Premises used: RingHom.IsStableUnderBaseChange.tensorProduct, MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, And.left, RingHomClass.toRingHom, RingEquiv.toRingHom
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (S := Localization.Away g) (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
⊢ P
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑e : S ⊗[R] Localization.Away g →ₐ[S] Localization.Away (1 ⊗ₜ[R] g)) :
        S ⊗[R] Localization.Away g →+* Localization.Away (1 ⊗ₜ[R] g))
      (algebraMap S (S ⊗[R] Localization.Away g)))

Tactic:
exact hPi.left _ _ (hPb.tensorProduct _ hg)

Premises used: RingHom.IsStableUnderBaseChange.tensorProduct, And.left
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
obtain :
  ∀ (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)),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)

Tactic:
obtain ⟨s, hsone, hs⟩ := hf
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rw :
  ∃ (ι : Type u) (s : ι → S') (_ : Eq (α := Ideal S') (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S' (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι),
      P (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)

Tactic:
rw [locally_iff_exists hPl.respectsIso]

Premises used: RingHom.LocalizationAwayPreserves.respectsIso, RingHom.locally_iff_exists
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
⊢ ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)

Tactic:
haveI (a : s) :
      IsLocalization.Away (((algebraMap S (Localization.Away a.val)).comp f) r) (Sₐ a) :=
    inferInstanceAs (IsLocalization.Away (rₐ a) (Sₐ a))
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
a : (↑s : Type u)
⊢ IsLocalization.Away (rₐ a) (Sₐ a)

Tactic:
(inferInstance : IsLocalization.Away (rₐ a) (Sₐ a))

Premises used: inferInstance
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
a : (↑s : Type u)
h :
  Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r)) =
    Submonoid.powers (rₐ a)
⊢ IsLocalization (R := Localization.Away (↑a : S))
    (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)

Tactic:
convert! (inferInstance : IsLocalization.Away (rₐ a) (Sₐ a))

Premises used: inferInstance