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_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 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦ toAlgebra (IsLocalization.map (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 (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
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 (H a)).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 : 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)
⊢ ∃ (ι : 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 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 : 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)
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 (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
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 : 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)
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 (S := Sₜ i)
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₜ i)) (IsLocalization.Away.map R' S' f r))
have refine_3 : ∀ (a : (↑s : Type u)),
  P (S := Sₐ a) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₐ a)) (IsLocalization.Away.map R' S' f r))
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 : 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)
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
Tactic: rw [← Set.image_eq_range, ← 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_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)
refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1₁ : Eq (α := Ideal S') (Ideal.map (F := S →+* S') (algebraMap S S') (Ideal.span s)) ⊤
Tactic: rw [← Set.image_eq_range, ← 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_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)
refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
refine_1₁ : Eq (α := Ideal S') (Ideal.map (F := S →+* S') (algebraMap S S') (Ideal.span s)) ⊤
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1₂ : Eq (α := Ideal S') (Ideal.map (R := S) (F := S →+* S') (algebraMap S S') ⊤) ⊤
Tactic: rw [← Set.image_eq_range, ← 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_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)
refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
refine_1₁ : Eq (α := Ideal S') (Ideal.map (F := S →+* S') (algebraMap S S') (Ideal.span s)) ⊤
refine_1₂ : Eq (α := Ideal S') (Ideal.map (R := S) (F := S →+* S') (algebraMap S S') ⊤) ⊤
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1₃ : Eq.{u + 1} (α := Ideal S') ⊤ ⊤
Tactic: rw [← Set.image_eq_range, ← 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_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)
⊢ IsLocalization.Away.{u, u} (R := S') ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a)
    (Sₐ a)
have h : Eq (α := Submonoid S')
  (Submonoid.powers ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a))
  (Algebra.algebraMapSubmonoid S' (Submonoid.powers (↑a : S)))
Tactic: convert!
    IsLocalization.commutes (T := Sₐ a) (M₁ := (Submonoid.powers r).map f) (S₁ := S') (S₂ :=
      Localization.Away a.val) (M₂ := Submonoid.powers a.val)