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_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_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
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)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦ toAlgebra (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
a : (↑s : Type u)
⊢ P (S := Sₐ a) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₐ a)) (IsLocalization.Away.map R' S' f r))
have refine_3 : P (R := R') (S := Sₐ a)
  (IsLocalization.map (M := Submonoid.powers r) (P := Localization.Away (↑a : S)) (T := Submonoid.powers (rₐ a)) (Sₐ a)
    (comp (algebraMap S (Localization.Away (↑a : S))) f) sorry)
Tactic: rw [algebraMap_toAlgebra, IsLocalization.Away.map, IsLocalization.map_comp_map]
-- 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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 (R := R') (IsLocalization.map S' 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 (R := R') (IsLocalization.map S' f sorry)
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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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 (R := R') (IsLocalization.map S' f ⋯)
have rw : ∃ (ι : Type u) (s : ι → S') (_ : Eq (α := Ideal S') (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
  (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S' (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
  ∀ (i : ι),
    P (R := R') (S := Sₜ i)
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f sorry))
Tactic: rw [locally_iff_exists hPl.away.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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ 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 (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
have hM : ∀ (a : (↑s : Type u)),
  Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
Tactic: have hM (a : s) : M.map ((algebraMap S (Localization.Away a.val)).comp f) = Mₐ a :=
    (M.map_map _ _).symm
-- 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
a : (↑s : Type u)
⊢ IsLocalization
    (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
    (Sₐ a)
have rw : IsLocalization (Mₐ a) (Sₐ a)
Tactic: rw [hM]
-- 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ 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 (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
have this : ∀ (a : (↑s : Type u)),
  IsLocalization
    (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
    (Sₐ a)
Tactic: haveI (a : s) :
      IsLocalization (M.map ((algebraMap S (Localization.Away a.val)).comp f)) (Sₐ a) := by
    rw [hM]
    infer_instance
-- 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (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 (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
have this₁ : ∀ (a : (↑s : Type u)),
  IsLocalization (R := Localization.Away (↑a : S))
    (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
Tactic: haveI (a : s) :
      IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) (M.map f)) (Sₐ a) :=
    inferInstanceAs <| IsLocalization (Mₐ 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
⊢ ∃ (ι : 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 (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
have this₁ : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
Tactic: haveI (a : s) : IsScalarTower S S' (Sₐ a) :=
    IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (M.map f).le_comap_map).symm
-- 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S 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 (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
have refine_1 : Eq.{u + 1} (α := Ideal S') (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S)))
  ⊤
Tactic: refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ,
      inferInstance, inferInstance, fun a ↦ ?_, fun 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
refine_1 :
  Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
⊢ ∃ (ι : 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 (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
have refine_2 : ∀ (a : (↑s : Type u)),
  IsLocalization.Away.{u, u} (R := S') ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a)
    (Sₐ a)
Tactic: refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ,
      inferInstance, inferInstance, fun a ↦ ?_, fun 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 : LocalizationPreserves.{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
M : Submonoid 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 M R'
inst_7 : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
refine_1 :
  Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
refine_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization.Away.{u, u} (R := S')
      ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a) (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 (R := R') (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.map S' f ⋯))
have refine_3 : ∀ (a : (↑s : Type u)),
  P (R := R') (S := Sₐ a)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₐ a)) (IsLocalization.map S' f sorry))
Tactic: refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ,
      inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩