awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : 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
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
x : R
⊢ Eq (α :=
    Localization.Away (M := Localization.Away (↑b : T))
      ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))
    ((algebraMap T
            (Localization.Away (M := Localization.Away (↑b : T))
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                  ((g : (a : S) → T) (↑a : S)) :
                Localization.Away (↑b : T))) :
          (a_1 : T) →
            Localization.Away
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                ((g : (a : S) → T) (↑a : S))))
        ((g : (a : S) → T) ((f : (a : R) → S) x : S)) :
      Localization.Away (M := Localization.Away (↑b : T))
        ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
            ((g : (a : S) → T) (↑a : S)) :
          Localization.Away (↑b : T)))
    ((algebraMap (Localization.Away (↑b : T))
            (Localization.Away (M := Localization.Away (↑b : T))
              ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T))) :
          (a_1 : Localization.Away (↑b : T)) → Localization.Away ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S)))
        ((g' : (a : S) → Localization.Away (↑b : T)) ((f : (a : R) → S) x)) :
      Localization.Away (M := Localization.Away (↑b : T))
        ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))

Tactic:
rfl
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : 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
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
⊢ Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))

Tactic:
have : (algebraMap T <| Localization.Away a').comp (g.comp f) =
        (Localization.awayMap g' a.val).comp ((algebraMap S (Localization.Away a.val)).comp f) := by
      ext x
      simp only [coe_comp, Function.comp_apply, a']
      change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))
      simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]
      rfl
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : 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
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
this :
  Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
refine_2 :
  P (S :=
    Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
⊢ P (S :=
    (fun (x : ↥sf × ↥sg) ↦
        (match (motive := ↥sf × ↥sg → Type u) x with
          | (a, b) =>
            Localization.Away (M := Localization.Away (↑b : T))
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                  ((g : (a : S) → T) (↑a : S)) :
                Localization.Away (↑b : T)) :
          Type u))
      (a, b))
    (comp
      (algebraMap T
        ((fun (x : ↥sf × ↥sg) ↦
            (match (motive := ↥sf × ↥sg → Type u) x with
              | (a, b) =>
                Localization.Away (M := Localization.Away (↑b : T))
                  ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                      ((g : (a : S) → T) (↑a : S)) :
                    Localization.Away (↑b : T)) :
              Type u))
          (a, b)))
      (g.comp f))

Tactic:
simp only [this, a']
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : 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
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
this :
  Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
refine_2 : P (R := Localization.Away (↑a : S)) (Localization.awayMap g' (↑a : S))
⊢ P (S :=
    Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))

Tactic:
apply hPc _ _ (hsf a.val a.property)

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : 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
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
this :
  Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
apply :
  IsLocalization (Submonoid.map g' (Submonoid.powers (↑a : S)))
    (Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))
⊢ P (R := Localization.Away (↑a : S)) (Localization.awayMap g' (↑a : S))

Tactic:
apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property)

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : 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
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
this :
  Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
⊢ IsLocalization (Submonoid.map g' (Submonoid.powers (↑a : S)))
    (Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))

Tactic:
IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val

Premises used: Set.Mem, IsLocalization.Away.instMapRingHomPowersOfCoe, Localization.Away, Quotient.mk', Subtype.val, OreLocalization.oreDiv, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : 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
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
this :
  Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
⊢ IsLocalization (Submonoid.map g' (Submonoid.powers (↑a : S)))
    (Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))

Tactic:
exact IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val

Premises used: IsLocalization.Away.instMapRingHomPowersOfCoe, Localization.Away, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : 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] (s : S)
    [IsLocalization.Away s T] (f : 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))
        (comp (algebraMap S T) f)
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra S T] (s : S)
    [IsLocalization.Away s T] (f : 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))
        (comp (algebraMap S T) f)

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

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

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

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : 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
_ :
  ∀ [IsLocalization.Away t T] (f : 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))
        (comp (algebraMap S T) f)
⊢ ∀ [IsLocalization.Away t T] (f : 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))
        (comp (algebraMap S T) f)

Tactic:
_
-- 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
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) (comp (algebraMap S T) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (comp (algebraMap S T) f)

Tactic:
obtain ⟨s, hsone, hs⟩ := hf
-- 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)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (comp (algebraMap S T) f)

Tactic:
⟨algebraMap S T '' s, ?_, ?_⟩

Premises used: Algebra.algebraMap, RingHom.Locally, Exists.intro, Set.image, 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)
refine_1 : Eq (α := Ideal T) (Ideal.span ((⇑(algebraMap S T) : (a : S) → T) '' s)) ⊤
refine_2 :
  ∀ (t : T),
    Membership.mem (γ := Set T) ((⇑(algebraMap S T) : (a : S) → T) '' s) t →
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away t)) (comp (algebraMap S T) f))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (comp (algebraMap S T) f)

Tactic:
refine ⟨algebraMap S T '' s, ?_, ?_⟩
-- 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)
refine_1 : Eq (α := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.span s)) ⊤
refine_1₁ : Eq (α := Ideal T) (Ideal.map (R := S) (F := S →+* T) (algebraMap S T) ⊤) ⊤
refine_1₂ refine_1₃ : Eq.{u + 1} (α := Ideal T) ⊤ ⊤
⊢ Eq (α := Ideal T) (Ideal.span ((⇑(algebraMap S T) : (a : S) → T) '' s)) ⊤

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

Premises used: Ideal.map_span, Ideal.map_top