awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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))
⊢ ∃ (ι : 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_2 : ∀ (i : (a : (↑s : Type u)) × (↑(t a) : Type u)),
  P (S :=
    (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))
      i)
    (comp
      (algebraMap S
        ((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))
          i))
      f)
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⟩ ↦ ?_, ?_⟩
-- 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))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ IsLocalization.Away (R := Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
        (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).1 :
      Localization.Away (↑a : S))
    (Localization.Away (↑b : Localization.Away (↑a : S)))
have h : Associated (↑b : Localization.Away (↑a : S))
  ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
    (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).1)
Tactic: apply IsLocalization.Away.of_associated (r := b.val)
-- 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))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ Associated (↑b : Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
      (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).1)
have h : Associated (↑b : Localization.Away (↑a : S))
  (HMul.hMul (β := Localization.Away (↑a : S)) (↑b : Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
        ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
      Localization.Away (↑a : S)))
Tactic: rw [← IsLocalization.Away.sec_spec]
-- 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))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ Associated (↑b : Localization.Away (↑a : S))
    (HMul.hMul (β := Localization.Away (↑a : S)) (↑b : Localization.Away (↑a : S))
      ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
          ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
        Localization.Away (↑a : S)))
have h : IsUnit (M := Localization.Away (↑a : S))
  ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
      ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
    Localization.Away (↑a : S))
Tactic: apply associated_mul_unit_right
-- 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))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ IsUnit (M := Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
        ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
      Localization.Away (↑a : S))
have h : IsUnit
  (HPow.hPow (α := Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) (↑a : S))
    (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2)
Tactic: rw [map_pow _ _]
-- 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))
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ P (S :=
    (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))
    (comp
      (algebraMap S
        ((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)))
      f)
have refine_2 : P (S :=
  (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))
  (comp
    (@comp _ (Localization.Away (↑a : S)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away (↑a : S)) (Localization.Away (↑b : Localization.Away (↑a : S))))
      (algebraMap S (Localization.Away (↑a : S))))
    f)
Tactic: rw [IsScalarTower.algebraMap_eq S (Localization.Away a.val) (Localization.Away b.val)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦
      (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
    (e.toRingHom.comp f)
have refine_1 : Eq (α := Ideal T) (Ideal.span ((⇑e : (a : S) → T) '' s)) ⊤
Tactic: refine ⟨e '' s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
refine_1 : Eq (α := Ideal T) (Ideal.span ((⇑e : (a : S) → T) '' s)) ⊤
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)
have refine_2 : ∀ (t : T),
  Membership.mem (γ := Set T) ((⇑e : (a : S) → T) '' s) t →
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) (e.toRingHom.comp f))
Tactic: refine ⟨e '' s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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 (α := Ideal T) (Ideal.span ((⇑e : (a : S) → T) '' s)) ⊤
have refine_1 : Eq (α := Ideal T) (Ideal.map e (Ideal.span s)) ⊤
Tactic: rw [← Ideal.map_span, hsone, Ideal.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
refine_1 : Eq (α := Ideal T) (Ideal.map e (Ideal.span s)) ⊤
⊢ Eq (α := Ideal T) (Ideal.span ((⇑e : (a : S) → T) '' s)) ⊤
have refine_1₁ : Eq (α := Ideal T) (Ideal.map (R := S) e ⊤) ⊤
Tactic: rw [← Ideal.map_span, hsone, Ideal.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
refine_1 : Eq (α := Ideal T) (Ideal.map e (Ideal.span s)) ⊤
refine_1₁ : Eq (α := Ideal T) (Ideal.map (R := S) e ⊤) ⊤
⊢ Eq (α := Ideal T) (Ideal.span ((⇑e : (a : S) → T) '' s)) ⊤
have refine_1₂ : Eq.{u + 1} (α := Ideal T) ⊤ ⊤
Tactic: rw [← Ideal.map_span, hsone, Ideal.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
⊢ comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))
have a₁ : ∀ (x : S),
  Eq (α := Localization.Away (M := T) ((e : (a : S) → T) a : T))
    ((comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom :
          (a_1 : S) → Localization.Away ((e : (a : S) → T) a))
        x :
      Localization.Away (M := T) ((e : (a : S) → T) a : T))
    ((e'.toRingHom.comp (algebraMap S (Localization.Away a)) : (a_1 : S) → Localization.Away ((e : (a : S) → T) a)) x :
      Localization.Away (M := T) ((e : (a : S) → T) a : T))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
⊢ P (S := Localization.Away (M := T) ((e : (a : S) → T) a : T))
    (comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) (e.toRingHom.comp f))
have this : comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
  e'.toRingHom.comp (algebraMap S (Localization.Away a))
Tactic: have : (algebraMap T (Localization.Away (e a))).comp e.toRingHom =
          e'.toRingHom.comp (algebraMap S (Localization.Away a)) := by
        ext x
        simp [e']
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
this :
  comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P (S := Localization.Away (M := T) ((e : (a : S) → T) a : T))
    (comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) (e.toRingHom.comp f))
have refine_2 : P (e'.toRingHom.comp (comp (algebraMap S (Localization.Away a)) f))
Tactic: rw [← RingHom.comp_assoc, this, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
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)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (M := T) ((e : (a : S) → T) a : T) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (M := T) ((e : (a : S) → T) a : T)) e ⋯
this :
  comp (algebraMap T (Localization.Away (M := T) ((e : (a : S) → T) a : T))) e.toRingHom =
    e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P (e'.toRingHom.comp (comp (algebraMap S (Localization.Away a)) f))
have refine_2 : P (S := Localization.Away a) (comp (algebraMap S (Localization.Away a)) f)
Tactic: apply hPi.left
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R S)
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 _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away t)) (algebraMap R S))
Tactic: use {1}
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ ∃ (_ : 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 _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away t)) (algebraMap R S))
have h : P (S := Localization.Away (M := S) 1)
  (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away (M := S) 1)) (algebraMap R S))
Tactic: simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away (M := S) 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
⊢ P (S := Localization.Away (M := S) 1)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away (M := S) 1)) (algebraMap R S))
have this : IsLocalization.Away r (Localization.Away (M := S) 1)
Tactic: haveI : IsLocalization.Away r (Localization.Away (1 : S)) :=
    IsLocalization.isLocalization_of_algEquiv (Submonoid.powers r) e
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away (M := S) 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away (M := S) 1)
⊢ P (S := Localization.Away (M := S) 1)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away (M := S) 1)) (algebraMap R S))
have h : P (S := Localization.Away (M := S) 1) (algebraMap R (Localization.Away (M := S) 1))
Tactic: rw [← IsScalarTower.algebraMap_eq]