awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Integral (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦ x.IsIntegral) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
r : S
this_1 : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this_2 : Algebra (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :=
  (Localization.awayMap f t).toAlgebra
this_3 : IsScalarTower R (Localization.Away t) (Localization.Away (M := S) ((f : (a : R) → S) t : S))
this_4 :
  _root_.IsIntegral (Localization.Away t) (A := Localization.Away (M := S) ((f : (a : R) → S) t : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) t : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) t))
        r :
      Localization.Away (M := S) ((f : (a : R) → S) t : S))
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
pos : (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₁ : (t ^ m) ^ (p.natDegree - 1 + 1) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₂ : ((t ^ m) ^ (p.natDegree - 1) * t ^ m) • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₃ : (t ^ m) ^ (p.natDegree - 1) • t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
pos₄ : HSMul.hSMul (β := S) ((t ^ m) ^ (p.natDegree - 1)) 0 = 0
⊢ eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) = 0
have pos₅ : Eq.{u_1 + 1} (α := S) 0 0
Tactic: rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    Eq.{u + 1} (α := Ideal S)
      (Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) ⊤
have refine : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
  ∀ (s : Set S) (hs : Eq (α := Ideal S) (Ideal.span s) ⊤)
    (h :
      ∀ 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 {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) ⊤
Tactic: refine ⟨fun ⟨s, hs, h⟩ ↦ ?_, fun h ↦ ⟨_, h, fun g hg ↦ hg⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
h_1 : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h :
  ∀ 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 {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) ⊤
have rw : s ⊆ (↑(Ideal.span {g : S | P (S := Localization.Away g) (comp (algebraMap S (Localization.Away g)) f)}) : Set S)
Tactic: rw [eq_top_iff, ← hs, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
⊢ 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, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
have mp : 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, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
mp :
  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, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) 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, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
have mpr : (∃ (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)) →
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
have mp : ∀ (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: obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hsone
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
have w : Set S
Tactic: use s, hsone, hs
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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)) ⊤
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
have 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)
Tactic: use s, hsone, hs
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
have 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)
Tactic: use Set.range s, hsone
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
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))
⊢ P (S := Localization.Away (s i)) (comp (algebraMap S (Localization.Away (s i))) f)
have this : 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)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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 (S := Localization.Away (s i)) (comp (algebraMap S (Localization.Away (s i))) f)
have h : P (e.symm.toRingHom.comp (comp (algebraMap S (Sₜ i)) f))
Tactic: rw [this, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
⊢ 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)
have 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)
Tactic: rw [locally_iff_finite P f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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)
have 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)
Tactic: refine ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun t ht Sₜ _ _ _ ↦ ?_⟩, fun ⟨s, hsone, hs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: refine ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun t ht Sₜ _ _ _ ↦ ?_⟩, fun ⟨s, hsone, hs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
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ₜ)
⊢ P (comp (algebraMap S Sₜ) f)
have this : 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)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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 (comp (algebraMap S Sₜ) f)
have refine_1 : P (e.toRingHom.comp (comp (algebraMap S (Localization.Away t)) f))
Tactic: rw [this, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
have 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)
Tactic: use {1}
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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) ⋯)
⊢ ∃ (_ : 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)
have h : P (S := Localization.Away (M := S) 1) (comp (algebraMap S (Localization.Away (M := S) 1)) f)
Tactic: simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have 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
Tactic: obtain ⟨s, hsone, hs⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
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 :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦
        (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
      _ (Localization.Away (↑r : S)) _ _ (comp (algebraMap S (Localization.Away (↑r : S))) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
have choose : ∀ (t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S)))
  (htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤)
  (ht :
    ∀ (r : (↑s : Type u)),
      ∀ t_1 ∈ t r,
        (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
          (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
            (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
            (comp (algebraMap S (Localization.Away (↑r : S))) f))),
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
Tactic: choose t htone ht using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
have 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 (algebraMap S (Sₜ i)) f)
Tactic: rw [locally_iff_exists hP]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
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
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
⊢ ∃ (ι : 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 (algebraMap S (Sₜ i)) f)
have refine_1 : ∀ (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) (a : (↑s : Type u)) (b : (↑(t a) : Type u)),
  IsLocalization.Away
    (IsLocalization.Away.mulNumerator s (Rₜ := fun (t : (↑s : Type u)) ↦ Localization.Away (↑t : S)) t
      (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
    ((fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
        (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
          | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
          Type u))
      (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
Tactic: refine ⟨(a : s) × t a, IsLocalization.Away.mulNumerator s t,
      IsLocalization.Away.span_range_mulNumerator_eq_top hsone htone,
      fun ⟨a, b⟩ ↦ Localization.Away b.val, inferInstance, inferInstance, fun ⟨a, b⟩ ↦ ?_, ?_⟩