awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
hg : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
have hf₁ : ∃ (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: rw [locally_iff_finite] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
hg : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g
hf₁ :
  ∃ (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) (g.comp f)
have hg₁ : ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
  ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
Tactic: rw [locally_iff_finite] at hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf :
  ∃ (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)
hg :
  ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
have obtain : ∀ (sf : Finset S) (hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤)
  (hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)),
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
Tactic: obtain ⟨sf, hsfone, hsf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg :
  ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
have obtain : ∀ (sg : Finset T) (hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤)
  (hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)),
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
Tactic: obtain ⟨sg, hsgone, hsg⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
have rw : ∃ (ι : Type u) (s : ι → T) (_ : Eq (α := Ideal T) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
  (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra T (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
  ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap T (Sₜ i)) (g.comp f))
Tactic: rw [locally_iff_exists hPi]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
⊢ ∃ (ι : Type u) (s : ι → T) (_ : Eq (α := Ideal T) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra T (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap T (Sₜ i)) (g.comp f))
have refine_1 : Eq.{u + 1} (α := Ideal T)
  (Ideal.span
    (Set.range fun (x : ↥sf × ↥sg) ↦
      match (motive := ↥sf × ↥sg → T) x with
      | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T)))
  ⊤
Tactic: refine ⟨sf × sg, fun (a, b) ↦ g a * b, ?_,
      fun (a, b) ↦ Localization.Away ((algebraMap T (Localization.Away b.val)) (g a.val)),
      inferInstance, inferInstance, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
refine_1 :
  Eq.{u + 1} (α := Ideal T)
    (Ideal.span
      (Set.range fun (x : ↥sf × ↥sg) ↦
        match (motive := ↥sf × ↥sg → T) x with
        | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T)))
    ⊤
⊢ ∃ (ι : Type u) (s : ι → T) (_ : Eq (α := Ideal T) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra T (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap T (Sₜ i)) (g.comp f))
have refine_2 : ∀ (i : ↥sf × ↥sg),
  P (S :=
    (fun (x : ↥sf × ↥sg) ↦
        (match (motive := ↥sf × ↥sg → Type u) x with
          | (a, b) =>
            Localization.Away (M := Localization.Away (↑b : T))
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                  ((g : (a : S) → T) (↑a : S)) :
                Localization.Away (↑b : T)) :
          Type u))
      i)
    (comp
      (algebraMap T
        ((fun (x : ↥sf × ↥sg) ↦
            (match (motive := ↥sf × ↥sg → Type u) x with
              | (a, b) =>
                Localization.Away (M := Localization.Away (↑b : T))
                  ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                      ((g : (a : S) → T) (↑a : S)) :
                    Localization.Away (↑b : T)) :
              Type u))
          i))
      (g.comp f))
Tactic: refine ⟨sf × sg, fun (a, b) ↦ g a * b, ?_,
      fun (a, b) ↦ Localization.Away ((algebraMap T (Localization.Away b.val)) (g a.val)),
      inferInstance, inferInstance, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
⊢ Eq.{u + 1} (α := Ideal T)
    (Ideal.span
      (Set.range fun (x : ↥sf × ↥sg) ↦
        match (motive := ↥sf × ↥sg → T) x with
        | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T)))
    ⊤
have refine_1 : (↑sg : Set T) ⊆
  (↑(Ideal.span
        (Set.range fun (x : ↥sf × ↥sg) ↦
          match (motive := ↥sf × ↥sg → T) x with
          | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T))) :
    Set T)
Tactic: rw [eq_top_iff, ← hsgone, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
⊢ t ∈
    (↑(Ideal.span
          (Set.range fun (x : ↥sf × ↥sg) ↦
            match (motive := ↥sf × ↥sg → T) x with
            | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T))) :
      Set T)
have this : Membership.mem (γ := Ideal S) (Ideal.span (Set.range fun (a : ↥sf) ↦ (↑a : S))) 1
Tactic: have : 1 ∈ Ideal.span (Set.range <| fun a : sf ↦ a.val) := by simp [hsfone]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
this : Membership.mem (γ := Ideal S) (Ideal.span (Set.range fun (a : ↥sf) ↦ (↑a : S))) 1
⊢ t ∈
    (↑(Ideal.span
          (Set.range fun (x : ↥sf × ↥sg) ↦
            match (motive := ↥sf × ↥sg → T) x with
            | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T))) :
      Set T)
have refine_1 : ∀ (this : ∃ (c : ↥sf → S), Eq.{u + 1} (α := S) (∑ i : ↥sf, c i * (↑i : S)) 1),
  ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t
Tactic: simp only [Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
this : ∃ (c : ↥sf → S), Eq.{u + 1} (α := S) (∑ i : ↥sf, c i * (↑i : S)) 1
⊢ ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t
have refine_1 : ∀ (cf : ↥sf → S) (hcf : Eq.{u + 1} (α := S) (∑ i : ↥sf, cf i * (↑i : S)) 1),
  ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t
Tactic: obtain ⟨cf, hcf⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
cf : ↥sf → S
hcf : Eq.{u + 1} (α := S) (∑ i : ↥sf, cf i * (↑i : S)) 1
cg : ↥sg → T := Pi.single (M := fun (a : ↥sg) ↦ T) (Subtype.mk (p := fun (x : T) ↦ x ∈ sg) t ht) 1
⊢ ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t
have h : ∑ i : ↥sf × ↥sg,
    (fun (x : ↥sf × ↥sg) ↦
          (match (motive := ↥sf × ↥sg → T) x with
            | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (cf a) : T) (cg b) :
            T))
        i *
      HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) =
  t
Tactic: use fun (a, b) ↦ g (cf a) * cg b
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
⊢ Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
have a₁ : ∀ (x : R),
  Eq (α := Localization.Away a')
    ((comp (algebraMap T (Localization.Away a')) (g.comp f) : (a : R) → Localization.Away a') x : Localization.Away a')
    ((comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) :
          (a : R) → Localization.Away a')
        x :
      Localization.Away a')
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
x : R
⊢ Eq (α := Localization.Away a')
    ((comp (algebraMap T (Localization.Away a')) (g.comp f) : (a : R) → Localization.Away a') x : Localization.Away a')
    ((comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) :
          (a : R) → Localization.Away a')
        x :
      Localization.Away a')
have a₁ : Eq (α :=
  Localization.Away (M := Localization.Away (↑b : T))
    ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
      Localization.Away (↑b : T)))
  ((algebraMap T
          (Localization.Away (M := Localization.Away (↑b : T))
            ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                ((g : (a : S) → T) (↑a : S)) :
              Localization.Away (↑b : T))) :
        (a_1 : T) →
          Localization.Away
            ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
              ((g : (a : S) → T) (↑a : S))))
      ((g : (a : S) → T) ((f : (a : R) → S) x : S)) :
    Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))
  ((Localization.awayMap g' (↑a : S) :
        (a_1 : Localization.Away (↑a : S)) → Localization.Away ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S)))
      ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) x)) :
    Localization.Away (M := Localization.Away (↑b : T))
      ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))
Tactic: simp only [coe_comp, Function.comp_apply, a']
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
⊢ P (S :=
    (fun (x : ↥sf × ↥sg) ↦
        (match (motive := ↥sf × ↥sg → Type u) x with
          | (a, b) =>
            Localization.Away (M := Localization.Away (↑b : T))
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                  ((g : (a : S) → T) (↑a : S)) :
                Localization.Away (↑b : T)) :
          Type u))
      (a, b))
    (comp
      (algebraMap T
        ((fun (x : ↥sf × ↥sg) ↦
            (match (motive := ↥sf × ↥sg → Type u) x with
              | (a, b) =>
                Localization.Away (M := Localization.Away (↑b : T))
                  ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                      ((g : (a : S) → T) (↑a : S)) :
                    Localization.Away (↑b : T)) :
              Type u))
          (a, b)))
      (g.comp f))
have this : Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
  (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
Tactic: have : (algebraMap T <| Localization.Away a').comp (g.comp f) =
        (Localization.awayMap g' a.val).comp ((algebraMap S (Localization.Away a.val)).comp f) := by
      ext x
      simp only [coe_comp, Function.comp_apply, a']
      change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))
      simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]
      rfl