awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
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)
s' : Finset S
h₁ : (↑s' : Set S) ⊆ s
h₂ : Eq (α := Ideal S) (Ideal.span (↑s' : Set S)) ⊤
⊢ ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)

Tactic:
⟨s', h₂, fun t ht ↦ hs t (h₁ ht)⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
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)
s' : Finset S
h₁ : (↑s' : Set S) ⊆ s
h₂ : Eq (α := Ideal S) (Ideal.span (↑s' : Set S)) ⊤
⊢ ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)

Tactic:
exact ⟨s', h₂, fun t ht ↦ hs t (h₁ ht)⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs : ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
w : Set S
w₁ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h :
  ∀ t ∈ (↑s : Set 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) f

Tactic:
use s, hsone, hs
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤
Sₜ : ι → Type u
inst_2 : (i : ι) → CommRing (Sₜ i)
inst_3 : (i : ι) → Algebra S (Sₜ i)
inst_4 : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)
h :
  ∀ t ∈ Set.range 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) f

Tactic:
use Set.range s, hsone

Premises used: Set.range
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤
Sₜ : ι → Type u
inst_2 : (i : ι) → CommRing (Sₜ i)
inst_3 : (i : ι) → Algebra S (Sₜ i)
inst_4 : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)
i : ι
h : P (S := Localization.Away (s i)) (comp (algebraMap S (Localization.Away (s i))) f)
⊢ P (S := Localization.Away (s i)) (comp (algebraMap S (Localization.Away (s i))) f)

Tactic:
let e : Localization.Away (s i) ≃+* Sₜ i :=
    (IsLocalization.algEquiv (Submonoid.powers (s i)) _ _).toRingEquiv
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤
Sₜ : ι → Type u
inst_2 : (i : ι) → CommRing (Sₜ i)
inst_3 : (i : ι) → Algebra S (Sₜ i)
inst_4 : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)
i : ι
e : Localization.Away (s i) ≃+* Sₜ i :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (s i)) (Localization.Away (s i)) (Sₜ i))
⊢ Eq (α := S →+* Localization.Away (s i)) (algebraMap S (Localization.Away (s i)))
    (e.symm.toRingHom.comp (algebraMap S (Sₜ i)))

Tactic:
have : algebraMap S (Localization.Away (s i)) = e.symm.toRingHom.comp (algebraMap S (Sₜ i)) :=
    RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _).symm _).symm)
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤
Sₜ : ι → Type u
inst_2 : (i : ι) → CommRing (Sₜ i)
inst_3 : (i : ι) → Algebra S (Sₜ i)
inst_4 : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)
i : ι
e : Localization.Away (s i) ≃+* Sₜ i :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (s i)) (Localization.Away (s i)) (Sₜ i))
this :
  Eq (α := S →+* Localization.Away (s i)) (algebraMap S (Localization.Away (s i)))
    (e.symm.toRingHom.comp (algebraMap S (Sₜ i)))
h : P (e.symm.toRingHom.comp (comp (algebraMap S (Sₜ i)) f))
⊢ P (S := Localization.Away (s i)) (comp (algebraMap S (Localization.Away (s i))) f)

Tactic:
rw [this, RingHom.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
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤
Sₜ : ι → Type u
inst_2 : (i : ι) → CommRing (Sₜ i)
inst_3 : (i : ι) → Algebra S (Sₜ i)
inst_4 : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)
i : ι
e : Localization.Away (s i) ≃+* Sₜ i :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (s i)) (Localization.Away (s i)) (Sₜ i))
this :
  Eq (α := S →+* Localization.Away (s i)) (algebraMap S (Localization.Away (s i)))
    (e.symm.toRingHom.comp (algebraMap S (Sₜ i)))
⊢ P (e.symm.toRingHom.comp (comp (algebraMap S (Sₜ i)) f))

Tactic:
hP.left _ _ (hf i)

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤
Sₜ : ι → Type u
inst_2 : (i : ι) → CommRing (Sₜ i)
inst_3 : (i : ι) → Algebra S (Sₜ i)
inst_4 : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)
i : ι
e : Localization.Away (s i) ≃+* Sₜ i :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (s i)) (Localization.Away (s i)) (Sₜ i))
this :
  Eq (α := S →+* Localization.Away (s i)) (algebraMap S (Localization.Away (s i)))
    (e.symm.toRingHom.comp (algebraMap S (Sₜ i)))
⊢ P (e.symm.toRingHom.comp (comp (algebraMap S (Sₜ i)) f))

Tactic:
exact hP.left _ _ (hf i)

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
⊢ Eq.{u + 1} (α := Ideal S) (Ideal.span (Set.range fun (t : (↑s : Type u)) ↦ (↑t : S))) ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
rw :
  (∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) ↔
    ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P (comp (algebraMap S Sₜ) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P (comp (algebraMap S Sₜ) f)

Tactic:
rw [locally_iff_finite P f]

Premises used: RingHom.locally_iff_finite
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
⊢ (∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) ↔
    ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P (comp (algebraMap S Sₜ) f)

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

Premises used: _private.0.RingHom.locally_iff_isLocalization.match_1, Exists, _private.0.RingHom.locally_iff_finite.match_1, Iff.intro, Exists.intro
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
refine_1 :
  (∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) →
    ∀ (s : Finset S) (hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤)
      (hs : ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) (t : S) (ht : t ∈ s)
      (Sₜ : Type u) (x : CommRing Sₜ) (x_1 : Algebra S Sₜ), IsLocalization.Away t Sₜ → P (comp (algebraMap S Sₜ) f)
refine_2 :
  (∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P (comp (algebraMap S Sₜ) f)) →
    ∀ (s : Finset S) (hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤)
      (hs :
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
            P (comp (algebraMap S Sₜ) f)),
      ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
        ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
⊢ (∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) ↔
    ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P (comp (algebraMap S Sₜ) f)

Tactic:
refine ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun t ht Sₜ _ _ _ ↦ ?_⟩, fun ⟨s, hsone, hs⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs : ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
t : S
ht : t ∈ s
Sₜ : Type u
x : CommRing Sₜ
x_1 : Algebra S Sₜ
h_1 : IsLocalization.Away t Sₜ
refine_1 : P (comp (algebraMap S Sₜ) f)
⊢ P (comp (algebraMap S Sₜ) f)

Tactic:
let e : Localization.Away t ≃+* Sₜ :=
      (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs : ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
t : S
ht : t ∈ s
Sₜ : Type u
x : CommRing Sₜ
x_1 : Algebra S Sₜ
h_1 : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ)
⊢ Eq (α := S →+* Sₜ) (algebraMap S Sₜ) (e.toRingHom.comp (algebraMap S (Localization.Away t)))

Tactic:
have : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t)) :=
      RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _) _).symm)
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs : ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
t : S
ht : t ∈ s
Sₜ : Type u
x : CommRing Sₜ
x_1 : Algebra S Sₜ
h_1 : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ)
this : Eq (α := S →+* Sₜ) (algebraMap S Sₜ) (e.toRingHom.comp (algebraMap S (Localization.Away t)))
refine_1 : P (e.toRingHom.comp (comp (algebraMap S (Localization.Away t)) f))
⊢ P (comp (algebraMap S Sₜ) f)

Tactic:
rw [this, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs : ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
t : S
ht : t ∈ s
Sₜ : Type u
x : CommRing Sₜ
x_1 : Algebra S Sₜ
h_1 : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ)
this : Eq (α := S →+* Sₜ) (algebraMap S Sₜ) (e.toRingHom.comp (algebraMap S (Localization.Away t)))
⊢ P (e.toRingHom.comp (comp (algebraMap S (Localization.Away t)) f))

Tactic:
hP.left _ _ (hs t ht)

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs : ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
t : S
ht : t ∈ s
Sₜ : Type u
x : CommRing Sₜ
x_1 : Algebra S Sₜ
h_1 : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ)
this : Eq (α := S →+* Sₜ) (algebraMap S Sₜ) (e.toRingHom.comp (algebraMap S (Localization.Away t)))
⊢ P (e.toRingHom.comp (comp (algebraMap S (Localization.Away t)) f))

Tactic:
exact hP.left _ _ (hs t ht)

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s,
      ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
        P (comp (algebraMap S Sₜ) f)
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P (comp (algebraMap S Sₜ) f)
⊢ ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)

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

Premises used: Localization.Away, Exists.intro
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
h :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s,
      ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
        P (comp (algebraMap S Sₜ) f)
s : Finset S
hsone : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P (comp (algebraMap S Sₜ) f)
⊢ ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)

Tactic:
exact ⟨s, hsone, fun t ht ↦ hs t ht _⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
h :
  ∃ (_ : Eq (α := Ideal S) (Ideal.span {1}) ⊤),
    ∀ (t : S),
      Membership.mem (γ := Set S) {1} t →
        (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
          (comp (algebraMap S (Localization.Away t)) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f

Tactic:
use {1}
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
⊢ LE.le (α := Submonoid S) (Submonoid.powers 1) (IsUnit.submonoid S)

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
e : S ≃+* Localization.Away (M := S) 1 := AlgEquiv.toRingEquiv (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
h : P (S := Localization.Away (M := S) 1) (comp (algebraMap S (Localization.Away (M := S) 1)) f)
⊢ ∃ (_ : Eq (α := Ideal S) (Ideal.span {1}) ⊤),
    ∀ (t : S),
      Membership.mem (γ := Set S) {1} t →
        (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
          (comp (algebraMap S (Localization.Away t)) f)

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

Premises used: Ideal.span_singleton_one, forall_eq, Set.mem_singleton_iff, exists_const
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
e : S ≃+* Localization.Away (M := S) 1 := AlgEquiv.toRingEquiv (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
⊢ P (S := Localization.Away (M := S) 1) (comp (algebraMap S (Localization.Away (M := S) 1)) f)

Tactic:
hP.left f e hf

Premises used: MulEquiv.toMonoidHom, And.left, Quotient.mk', RingEquiv.toRingHom, OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst : CommRing R
inst_1 : CommRing S
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
e : S ≃+* Localization.Away (M := S) 1 := AlgEquiv.toRingEquiv (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
⊢ P (S := Localization.Away (M := S) 1) (comp (algebraMap S (Localization.Away (M := S) 1)) f)

Tactic:
exact hP.left f e hf

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] {f : R →+* S}, P f → Q f
R S : Type u
inst : CommRing R
inst_1 : CommRing S
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] ↦ Q) f
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
obtain ⟨s, hsone, hs⟩ := hf
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] {f : R →+* S}, P f → Q f
R S : Type u
inst : CommRing R
inst_1 : CommRing S
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] ↦ Q) f

Tactic:
⟨s, hsone, fun t ht ↦ hPQ (hs t ht)⟩

Premises used: RingHom.Locally, Exists.intro