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_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_2 :
  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))
this : IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : 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₁ : IsLocalization.Away (R := Localization.Away a)
  ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) t : Localization.Away a)
  (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
Tactic: haveI : IsLocalization.Away (algebraMap S (Localization.Away a) t)
        (Localization.Away (algebraMap S T a)) :=
      IsLocalization.Away.commutes _ T ((Localization.Away (algebraMap S T a))) a t
-- 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_2 :
  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))
this_3 : IsScalarTower S (Localization.Away a) (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : T))
this :
  IsLocalization.Away (R := Localization.Away a)
    ((algebraMap S (Localization.Away a) : (a_1 : S) → Localization.Away a) t : Localization.Away a)
    (Localization.Away (M := T) ((algebraMap S T : (a : S) → T) a : 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 refine_2 : P (S := Localization.Away a) (comp (algebraMap S (Localization.Away a)) f)
Tactic: apply hPa _ (algebraMap S (Localization.Away a) t)
-- 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 : StableUnderCompositionWithLocalizationAwaySource.{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 R S
r : R
inst_4 : IsLocalization.Away r S
f : 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))
      (f.comp (algebraMap R S))
have this : ∀ (s : Set T) (hsone : Eq (α := Ideal T) (Ideal.span s) ⊤)
  (hs :
    ∀ t ∈ s,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
        (comp (algebraMap T (Localization.Away t)) f)),
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R S))
Tactic: ⟨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
hPa : StableUnderCompositionWithLocalizationAwaySource.{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 R S
r : R
inst_4 : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Eq (α := Ideal T) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R S))
have refine : ∀ (t : T) (ht : t ∈ s),
  (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
    (comp (algebraMap T (Localization.Away t)) (f.comp (algebraMap R S)))
Tactic: refine ⟨s, hsone, fun t ht ↦ ?_⟩
-- 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 : StableUnderCompositionWithLocalizationAwaySource.{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 R S
r : R
inst_4 : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Eq (α := Ideal T) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap T (Localization.Away t)) f)
t : T
ht : t ∈ s
⊢ (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
    (comp (algebraMap T (Localization.Away t)) (f.comp (algebraMap R S)))
have rw : (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
  (comp (comp (algebraMap T (Localization.Away t)) f) (algebraMap R S))
Tactic: rw [← 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
hPb : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
have apply : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T) →
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
Tactic: apply IsStableUnderBaseChange.mk (locally_respectsIso hPi)
-- 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
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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 R S
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
⊢ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have rw : {g : T |
    P (S := Localization.Away g)
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away g)) (algebraMap R T))} ⊆
  (↑(Ideal.comap (F := T →ₐ[R] S ⊗[R] T) Algebra.TensorProduct.includeRight
        (Ideal.span
          {g : S ⊗[R] T |
            P (S := Localization.Away g)
              (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
                (algebraMap S (S ⊗[R] T)))})) :
    Set T)
Tactic: rw [locally_iff_span_eq_top, eq_top_iff, ← Ideal.map_top Algebra.TensorProduct.includeRight,
    ← hf.span_eq_top, Ideal.map_le_iff_le_comap, Ideal.span_le]
-- 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
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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 R S
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg :
  Membership.mem (γ := Set T)
    {g : T |
      P (S := Localization.Away g)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away g)) (algebraMap R T))}
    g
⊢ g ∈
    (↑(Ideal.comap (F := T →ₐ[R] S ⊗[R] T) Algebra.TensorProduct.includeRight
          (Ideal.span
            {g : S ⊗[R] T |
              P (S := Localization.Away g)
                (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
                  (algebraMap S (S ⊗[R] T)))})) :
      Set T)
have a : Membership.mem (α := S ⊗[R] T) (γ := Set (S ⊗[R] T))
  {g : S ⊗[R] T |
    P (S := Localization.Away g)
      (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
        (algebraMap S (S ⊗[R] T)))}
  ((Algebra.TensorProduct.includeRight : (a : T) → S ⊗[R] T) g : S ⊗[R] T)
Tactic: apply Ideal.subset_span
-- 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
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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 R S
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg :
  Membership.mem (γ := Set T)
    {g : T |
      P (S := Localization.Away g)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T (Localization.Away g)) (algebraMap R T))}
    g
⊢ Membership.mem (α := S ⊗[R] T) (γ := Set (S ⊗[R] T))
    {g : S ⊗[R] T |
      P (S := Localization.Away g)
        (@comp _ (S ⊗[R] T) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] T) (Localization.Away g))
          (algebraMap S (S ⊗[R] T)))}
    ((Algebra.TensorProduct.includeRight : (a : T) → S ⊗[R] T) g : S ⊗[R] T)
have a : ∀ (hg : P (S := Localization.Away g) (algebraMap R (Localization.Away g))),
  P (S := Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)) (algebraMap S (Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)))
Tactic: simp only [Set.mem_setOf_eq, Algebra.TensorProduct.includeRight_apply,
    ← IsScalarTower.algebraMap_eq] at hg ⊢
Cleared hypotheses: hg
-- 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
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange.{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 R S
inst_4 : Algebra R T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (S := Localization.Away g) (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
⊢ P (S := Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)) (algebraMap S (Localization.Away (M := S ⊗[R] T) (1 ⊗ₜ[R] g)))
have a : P
  (@comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(↑e : S ⊗[R] Localization.Away g →ₐ[S] Localization.Away (1 ⊗ₜ[R] g)) :
      S ⊗[R] Localization.Away g →+* Localization.Away (1 ⊗ₜ[R] g))
    (algebraMap S (S ⊗[R] Localization.Away g)))
Tactic: rw [← e.toAlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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) (IsLocalization.Away.map R' S' f r)
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) (IsLocalization.Away.map R' S' f r)
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_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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) (IsLocalization.Away.map R' S' f r)
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 _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
Tactic: rw [locally_iff_exists hPl.respectsIso]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
⊢ ∃ (ι : 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 _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
have this : ∀ (a : (↑s : Type u)),
  IsLocalization.Away (R := Localization.Away (↑a : S))
    ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
      Localization.Away (↑a : S))
    (Sₐ a)
Tactic: haveI (a : s) :
      IsLocalization.Away (((algebraMap S (Localization.Away a.val)).comp f) r) (Sₐ a) :=
    inferInstanceAs (IsLocalization.Away (rₐ a) (Sₐ a))
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
a : (↑s : Type u)
⊢ IsLocalization (R := Localization.Away (↑a : S))
    (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
have h : Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r)) =
  Submonoid.powers (rₐ a)
Tactic: convert! (inferInstance : IsLocalization.Away (rₐ a) (Sₐ a))
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
⊢ ∃ (ι : 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 _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
have this₁ : ∀ (a : (↑s : Type u)),
  IsLocalization (R := Localization.Away (↑a : S))
    (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
Tactic: haveI (a : s) : IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val)
    (Submonoid.map f (Submonoid.powers r))) (Sₐ a) := by
    convert! (inferInstance : IsLocalization.Away (rₐ a) (Sₐ a))
    simp [rₐ, Algebra.algebraMapSubmonoid]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves.{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
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) 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)
rₐ : (a : (↑s : Type u)) → Localization.Away (↑a : S) :=
  fun (a : (↑s : Type u)) ↦
    (algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) r)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization.Away (rₐ a)
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away (R := Localization.Away (↑a : S))
      ((comp (algebraMap S (Localization.Away (↑a : S))) f : (a_1 : R) → Localization.Away (↑a : S)) r :
        Localization.Away (↑a : S))
      (Sₐ a)
this :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
⊢ ∃ (ι : 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 _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
have H : ∀ (a : (↑s : Type u)),
  LE.le (α := Submonoid S) (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S)
    (Submonoid.comap (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
        (Submonoid.powers (rₐ a)) :
      Submonoid S)
Tactic: have H (a : s) : Submonoid.powers (f r) ≤
      (Submonoid.powers (rₐ a)).comap (algebraMap S (Localization.Away a.val)) := by
    simp [rₐ, Submonoid.powers_le]