awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsLocalIso R S
algInst : Algebra S T := (↑e : S →ₐ[R] T).toAlgebra
⊢ IsStandardOpenImmersion S T

Tactic:
have : IsStandardOpenImmersion S T := .of_bijective e.bijective
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsLocalIso R S
algInst : Algebra S T := (↑e : S →ₐ[R] T).toAlgebra
this : IsStandardOpenImmersion S T
⊢ IsLocalIso R T

Tactic:
.trans _ S _

Premises used: Algebra.IsLocalIso.trans
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsLocalIso R S
algInst : Algebra S T := (↑e : S →ₐ[R] T).toAlgebra
this : IsStandardOpenImmersion S T
⊢ IsLocalIso R T

Tactic:
exact .trans _ S _
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
⊢ IsLocalIso R S ↔ IsLocalIso R T

Tactic:
⟨fun _ ↦ .of_algEquiv e, fun _ ↦ .of_algEquiv e.symm⟩

Premises used: AlgEquiv.symm, Iff.intro, Algebra.IsLocalIso.of_algEquiv
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalIso R S
rw :
  {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} ⊆
    (↑(Ideal.comap (F := S →ₐ[R] T ⊗[R] S) TensorProduct.includeRight
          (Ideal.span {g : T ⊗[R] S | IsStandardOpenImmersion T (Localization.Away g)})) :
      Set S)
⊢ IsLocalIso T (T ⊗[R] S)

Tactic:
rw [iff_span_isStandardOpenImmersion_eq_top, _root_.eq_top_iff,
    ← Ideal.map_top Algebra.TensorProduct.includeRight, ← span_isStandardOpenImmersion_eq_top R S,
    Ideal.map_le_iff_le_comap, Ideal.span_le]

Premises used: Ideal.span_le, eq_top_iff, Ideal.map_le_iff_le_comap, Algebra.IsLocalIso.iff_span_isStandardOpenImmersion_eq_top, Ideal.map_top, Algebra.IsLocalIso.span_isStandardOpenImmersion_eq_top, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalIso R S
g : S
hg : Membership.mem (γ := Set S) {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} g
a :
  Membership.mem (α := T ⊗[R] S) (γ := Set (T ⊗[R] S)) {g : T ⊗[R] S | IsStandardOpenImmersion T (Localization.Away g)}
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) g : T ⊗[R] S)
⊢ g ∈
    (↑(Ideal.comap (F := S →ₐ[R] T ⊗[R] S) TensorProduct.includeRight
          (Ideal.span {g : T ⊗[R] S | IsStandardOpenImmersion T (Localization.Away g)})) :
      Set S)

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalIso R S
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ IsStandardOpenImmersion T
    (Localization.Away (M := T ⊗[R] S) ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) g : T ⊗[R] S))

Tactic:
.of_algEquiv <| IsLocalization.Away.tensorProductEquivTMulRight R T g (Localization.Away g)

Premises used: IsLocalization.Away.tensorProductEquivTMulRight, Localization.Away, Algebra.IsStandardOpenImmersion.of_algEquiv
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalIso R S
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ IsStandardOpenImmersion T
    (Localization.Away (M := T ⊗[R] S) ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) g : T ⊗[R] S))

Tactic:
exact .of_algEquiv <| IsLocalization.Away.tensorProductEquivTMulRight R T g (Localization.Away g)

Premises used: IsLocalization.Away.tensorProductEquivTMulRight, Localization.Away
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h :
  ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
    (∀ (s : Set a),
        Eq (α := Ideal a) (Ideal.span s) ⊤ →
          (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) ↔
      ∀ (s : Finset a),
        Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
          (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
      Eq (α := Ideal R) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R),
      Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))) → P f

Tactic:
apply forall₅_congr

Premises used: forall₅_congr
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  (∀ (s : Set a),
      Eq (α := Ideal a) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) →
    ∀ (s : Finset a),
      Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
h₁ :
  (∀ (s : Finset a),
      Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) →
    ∀ (s : Set a),
      Eq (α := Ideal a) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
⊢ (∀ (s : Set a),
      Eq (α := Ideal a) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) ↔
    ∀ (s : Finset a),
      Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Set a),
    Eq (α := Ideal a) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
s : Finset a
⊢ Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
    (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e

Tactic:
h s

Premises used: SetLike.coe
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Set a),
    Eq (α := Ideal a) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
s : Finset a
⊢ Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
    (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e

Tactic:
exact h s

Premises used: SetLike.coe
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset a),
    Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
      (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
s : Set a
hs : Eq (α := Ideal a) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))
h₁ : ∀ (s' : Finset a) (h₁ : (↑s' : Set a) ⊆ s) (h₂ : Eq (α := Ideal a) (Ideal.span (↑s' : Set a)) ⊤), P e
⊢ P e

Tactic:
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset a),
    Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
      (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
s : Set a
hs : Eq (α := Ideal a) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))
s' : Finset a
h₁ : (↑s' : Set a) ⊆ s
h₂ : Eq (α := Ideal a) (Ideal.span (↑s' : Set a)) ⊤
⊢ P e

Tactic:
h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

Premises used: Subtype.mk, Subtype.prop, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset a),
    Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
      (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
s : Set a
hs : Eq (α := Ideal a) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))
s' : Finset a
h₁ : (↑s' : Set a) ⊆ s
h₂ : Eq (α := Ideal a) (Ideal.span (↑s' : Set a)) ⊤
⊢ P e

Tactic:
exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

Premises used: Subtype.mk, Subtype.prop, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h :
  ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
    (∀ (s : Set b),
        Eq (α := Ideal b) (Ideal.span s) ⊤ →
          (∀ (r : (↑s : Type u)),
              P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
            P e) ↔
      ∀ (s : Finset b),
        Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
          (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
      Eq (α := Ideal S) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)) →
          P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset S),
      Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)) → P f

Tactic:
apply forall₅_congr

Premises used: forall₅_congr
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  (∀ (s : Set b),
      Eq (α := Ideal b) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
          P e) →
    ∀ (s : Finset b),
      Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
h₁ :
  (∀ (s : Finset b),
      Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e) →
    ∀ (s : Set b),
      Eq (α := Ideal b) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
          P e
⊢ (∀ (s : Set b),
      Eq (α := Ideal b) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
          P e) ↔
    ∀ (s : Finset b),
      Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Set b),
    Eq (α := Ideal b) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
        P e
s : Finset b
⊢ Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
    (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e

Tactic:
h s

Premises used: Set.Mem, SetLike.coe
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Set b),
    Eq (α := Ideal b) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
        P e
s : Finset b
⊢ Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
    (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e

Tactic:
exact h s

Premises used: SetLike.coe
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset b),
    Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
      (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
s : Set b
hs : Eq (α := Ideal b) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)
h₁ : ∀ (s' : Finset b) (h₁ : (↑s' : Set b) ⊆ s) (h₂ : Eq (α := Ideal b) (Ideal.span (↑s' : Set b)) ⊤), P e
⊢ P e

Tactic:
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset b),
    Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
      (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
s : Set b
hs : Eq (α := Ideal b) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)
s' : Finset b
h₁ : (↑s' : Set b) ⊆ s
h₂ : Eq (α := Ideal b) (Ideal.span (↑s' : Set b)) ⊤
⊢ P e

Tactic:
h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

Premises used: Subtype.mk, Subtype.prop, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset b),
    Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
      (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
s : Set b
hs : Eq (α := Ideal b) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)
s' : Finset b
h₁ : (↑s' : Set b) ⊆ s
h₂ : Eq (α := Ideal b) (Ideal.span (↑s' : Set b)) ⊤
⊢ P e

Tactic:
exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

Premises used: Subtype.mk, Subtype.prop, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
let : P f
⊢ P f

Tactic:
let _ := fun r : R => (Localization.awayMap (algebraMap R S) r).toAlgebra
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
⊢ P f

Tactic:
H s hs (fun r hr ↦ ?_)
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
refine :
  ∀ (r : R) (hr : r ∈ s),
    P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
⊢ P f

Tactic:
refine H s hs (fun r hr ↦ ?_)
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
r : R
hr : r ∈ s
h :
  Eq (α := R →+* Localization.Away r ⊗[R] S)
    (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S)) (algebraMap R (Localization.Away r)))
    (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
          Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
        (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
      (algebraMap R (Localization.Away r)))
⊢ Eq (α := Localization.Away r →+* Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
        Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))

Tactic:
apply IsLocalization.ringHom_ext (Submonoid.powers r)

Premises used: Submonoid.powers, IsLocalization.ringHom_ext