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_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))
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))
⊢ 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 refine_2 : P (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)))
  (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
Tactic: simp only [this, a']
-- 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))
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))
⊢ P (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)))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))
have refine_2 : P (R := Localization.Away (↑a : S)) (Localization.awayMap g' (↑a : S))
Tactic: apply hPc _ _ (hsf a.val a.property)
-- 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))
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))
⊢ P (R := Localization.Away (↑a : S)) (Localization.awayMap g' (↑a : S))
have apply : IsLocalization (Submonoid.map g' (Submonoid.powers (↑a : 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)))
Tactic: apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property)
-- 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
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
⊢ StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
have intro : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
  (fun {R S : Type u} [CommRing R] [CommRing S] ↦
        (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
      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))
        g →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        (g.comp f)
Tactic: classical
  intro R S T _ _ _ f g hf hg
  rw [locally_iff_finite] at hf hg
  obtain ⟨sf, hsfone, hsf⟩ := hf
  obtain ⟨sg, hsgone, hsg⟩ := hg
  rw [locally_iff_exists hPi]
  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, ?_⟩
  · rw [eq_top_iff, ← hsgone, Ideal.span_le]
    intro t ht
    have : 1 ∈ Ideal.span (Set.range <| fun a : sf ↦ a.val) := by simp [hsfone]
    simp only [Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe] at this ⊢
    obtain ⟨cf, hcf⟩ := this
    let cg : sg → T := Pi.single ⟨t, ht⟩ 1
    use fun (a, b) ↦ g (cf a) * cg b
    simp [cg, Pi.single_apply, Fintype.sum_prod_type, ← mul_assoc, ← Finset.sum_mul, ← map_mul,
      ← map_sum, hcf] at hcf ⊢
  · intro ⟨a, b⟩
    let g' := (algebraMap T (Localization.Away b.val)).comp g
    let a' := (algebraMap T (Localization.Away b.val)) (g a.val)
    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
    simp only [this, a']
    apply hPc _ _ (hsf a.val a.property)
    apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property)
    exact IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val
-- 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
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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] ↦ P) (comp (algebraMap S T) 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] ↦ P) (comp (algebraMap S T) 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_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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] ↦ P) (comp (algebraMap S T) f)
have refine_1 : Eq (α := Ideal T) (Ideal.span ((⇑(algebraMap S T) : (a : S) → T) '' s)) ⊤
Tactic: refine ⟨algebraMap S T '' s, ?_, ?_⟩
-- 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
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
refine_1 : Eq (α := Ideal T) (Ideal.span ((⇑(algebraMap S T) : (a : S) → T) '' s)) ⊤
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (comp (algebraMap S T) f)
have refine_2 : ∀ (t : T),
  Membership.mem (γ := Set T) ((⇑(algebraMap S T) : (a : S) → T) '' s) t →
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away t)) (comp (algebraMap S T) f))
Tactic: refine ⟨algebraMap S T '' s, ?_, ?_⟩
-- 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
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
⊢ Eq (α := Ideal T) (Ideal.span ((⇑(algebraMap S T) : (a : S) → T) '' s)) ⊤
have refine_1 : Eq (α := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (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_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
refine_1 : Eq (α := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.span s)) ⊤
⊢ Eq (α := Ideal T) (Ideal.span ((⇑(algebraMap S T) : (a : S) → T) '' s)) ⊤
have refine_1₁ : Eq (α := Ideal T) (Ideal.map (R := S) (F := S →+* T) (algebraMap S 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_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
refine_1 : Eq (α := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.span s)) ⊤
refine_1₁ : Eq (α := Ideal T) (Ideal.map (R := S) (F := S →+* T) (algebraMap S T) ⊤) ⊤
⊢ Eq (α := Ideal T) (Ideal.span ((⇑(algebraMap S T) : (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 (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
a : S
ha : a ∈ s
this : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
⊢ P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (comp (algebraMap S T) f))
have this₁ : Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
  (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
    (algebraMap S (Localization.Away a)))
  (@comp _ _ _ _ Semiring.toNonAssocSemiring _
    (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
Tactic: have : (algebraMap (Localization.Away a) (Localization.Away (algebraMap S T a))).comp
        (algebraMap S (Localization.Away a)) =
        (algebraMap T (Localization.Away (algebraMap S T a))).comp (algebraMap S T) := by
      simp [algebraMap_toAlgebra, IsLocalization.Away.map]
-- 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
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
a : S
ha : a ∈ s
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
⊢ P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (comp (algebraMap S T) f))
have refine_2 : P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
  (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
    (comp (algebraMap S (Localization.Away a)) f))
Tactic: rw [← comp_assoc, ← this, comp_assoc]
-- 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
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
a : S
ha : a ∈ s
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
⊢ IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
have h : ∀ (x : S),
  Eq (α := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    ((algebraMap S (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :
          (a_1 : S) → Localization.Away ((algebraMap S T : (a : S) → T) a))
        x :
      Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    ((algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :
          (a_1 : Localization.Away a) → Localization.Away ((algebraMap S T : (a : S) → T) a))
        ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) x) :
      Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
Tactic: apply IsScalarTower.of_algebraMap_eq
-- 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
hPa : StableUnderCompositionWithLocalizationAwayTarget.{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
inst_3 : Algebra S T
t : S
inst_4 : IsLocalization.Away t T
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)
a : S
ha : a ∈ s
this_1 : Algebra (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)) :=
  toAlgebra
    (IsLocalization.Away.map (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
      (algebraMap S T) a)
this :
  Eq (α := S →+* Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (algebraMap S (Localization.Away a)))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))) (algebraMap S T))
⊢ P (S := Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
    (@comp _ (Localization.Away a) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T)))
      (comp (algebraMap S (Localization.Away a)) f))
have this₁ : IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
Tactic: haveI : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a)) := by
      apply IsScalarTower.of_algebraMap_eq
      intro x
      simp [algebraMap_toAlgebra, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply]