awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
      Eq (α := Ideal R) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R),
      Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))) → P f
have h : ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
  (∀ (s : Set a),
      Eq (α := Ideal a) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) ↔
    ∀ (s : Finset a),
      Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
Tactic: apply forall₅_congr
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
⊢ (∀ (s : Set a),
      Eq (α := Ideal a) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) ↔
    ∀ (s : Finset a),
      Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
have h : (∀ (s : Set a),
    Eq (α := Ideal a) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) →
  ∀ (s : Finset a),
    Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
      (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  (∀ (s : Set a),
      Eq (α := Ideal a) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) →
    ∀ (s : Finset a),
      Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
⊢ (∀ (s : Set a),
      Eq (α := Ideal a) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) ↔
    ∀ (s : Finset a),
      Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
        (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
have h₁ : (∀ (s : Finset a),
    Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
      (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e) →
  ∀ (s : Set a),
    Eq (α := Ideal a) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset a),
    Eq (α := Ideal a) (Ideal.span (↑s : Set a)) ⊤ →
      (∀ (r : ↥s), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))) → P e
s : Set a
hs : Eq (α := Ideal a) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (R := Localization.Away (↑r : a)) (Localization.awayMap e (↑r : a))
⊢ P e
have h₁ : ∀ (s' : Finset a) (h₁ : (↑s' : Set a) ⊆ s) (h₂ : Eq (α := Ideal a) (Ideal.span (↑s' : Set a)) ⊤), P e
Tactic: obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
      Eq (α := Ideal S) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)) →
          P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset S),
      Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)) → P f
have h : ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
  (∀ (s : Set b),
      Eq (α := Ideal b) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
          P e) ↔
    ∀ (s : Finset b),
      Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
Tactic: apply forall₅_congr
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
⊢ (∀ (s : Set b),
      Eq (α := Ideal b) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
          P e) ↔
    ∀ (s : Finset b),
      Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
have h : (∀ (s : Set b),
    Eq (α := Ideal b) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
        P e) →
  ∀ (s : Finset b),
    Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
      (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  (∀ (s : Set b),
      Eq (α := Ideal b) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
          P e) →
    ∀ (s : Finset b),
      Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
⊢ (∀ (s : Set b),
      Eq (α := Ideal b) (Ideal.span s) ⊤ →
        (∀ (r : (↑s : Type u)),
            P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
          P e) ↔
    ∀ (s : Finset b),
      Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
        (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
have h₁ : (∀ (s : Finset b),
    Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
      (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e) →
  ∀ (s : Set b),
    Eq (α := Ideal b) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) →
        P e
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a b : Type u
c : CommRing a
d : CommRing b
e : a →+* b
h :
  ∀ (s : Finset b),
    Eq (α := Ideal b) (Ideal.span (↑s : Set b)) ⊤ →
      (∀ (r : ↥s), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)) → P e
s : Set b
hs : Eq (α := Ideal b) (Ideal.span s) ⊤
hs' : ∀ (r : (↑s : Type u)), P (S := Localization.Away (↑r : b)) (comp (algebraMap b (Localization.Away (↑r : b))) e)
⊢ P e
have h₁ : ∀ (s' : Finset b) (h₁ : (↑s' : Set b) ⊆ s) (h₂ : Eq (α := Ideal b) (Ideal.span (↑s' : Set b)) ⊤), P e
Tactic: obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
⊢ P f
have refine : ∀ (r : R) (hr : r ∈ s),
  P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
Tactic: refine H s hs (fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
r : R
hr : r ∈ s
⊢ Eq (α := Localization.Away r →+* Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
        Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
have h : Eq (α := R →+* Localization.Away r ⊗[R] S)
  (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S)) (algebraMap R (Localization.Away r)))
  (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
        Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
    (algebraMap R (Localization.Away r)))
Tactic: apply IsLocalization.ringHom_ext (Submonoid.powers r)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
r : R
hr : r ∈ s
⊢ Eq (α := R →+* Localization.Away r ⊗[R] S)
    (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S)) (algebraMap R (Localization.Away r)))
    (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
          Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
        (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
      (algebraMap R (Localization.Away r)))
have h : ∀ (x_1 : R),
  Eq (α := Localization.Away r ⊗[R] S)
    ((@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S)) (algebraMap R (Localization.Away r)) :
          (a : R) → Localization.Away r ⊗[R] S)
        x_1 :
      Localization.Away r ⊗[R] S)
    ((@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
            (@comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
                Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
              (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
            (algebraMap R (Localization.Away r)) :
          (a : R) → Localization.Away r ⊗[R] S)
        x_1 :
      Localization.Away r ⊗[R] S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
r : R
hr : r ∈ s
⊢ P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
have have : ∀
  (this :
    Eq (α := Localization.Away r →+* Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
          Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
        (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))),
  P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
Tactic: have : algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
      ((IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm : _ →+* _).comp
        (algebraMap (Localization.Away r) (Localization.Away (algebraMap R S r))) := by
    apply IsLocalization.ringHom_ext (Submonoid.powers r)
    ext
    simp [RingHom.algebraMap_toAlgebra, Localization.awayMap, IsLocalization.Away.map,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : Algebra R S] (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ r ∈ s,
          P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
            (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) →
        P (algebraMap R S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (Localization.Away (↑r : R)) _ _ _
      (Localization.awayMap f (↑r : R))
algInst : Algebra R S := f.toAlgebra
x : (r : R) → Algebra (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :=
  fun (r : R) ↦ toAlgebra (Localization.awayMap (algebraMap R S) r)
r : R
hr : r ∈ s
this :
  Eq (α := Localization.Away r →+* Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
        Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
⊢ P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
have rw : P (R := Localization.Away r)
  (@comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(AlgEquiv.symm (IsLocalization.Away.tensorRightEquiv S r (Localization.Away r))) :
      Localization.Away ((algebraMap R S : (a : R) → S) r) →+* Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
H : ∀ {R : Type u} [inst : CommRing R] (M : Submonoid R), P (S := Localization M) (algebraMap R (Localization M))
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ P (algebraMap R S)
have rw : P
  (@comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(↑(IsLocalization.algEquiv M (Localization (M := R) M) S) : Localization M →ₐ[R] S) : Localization M →+* S)
    (algebraMap R (Localization (M := R) M)))
Tactic: rw [← (IsLocalization.algEquiv M (Localization M) S).toAlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
⊢ P (R := R') (IsLocalization.map S' f hy)
have have : ∀ (hle : Submonoid.map f M ≤ T), P (R := R') (IsLocalization.map S' f hy)
Tactic: have hle : Submonoid.map f M ≤ T := by simpa [Submonoid.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
⊢ P (R := R') (IsLocalization.map S' f hy)
have this₁ : IsScalarTower S (Localization (Submonoid.map f M)) S'
Tactic: have : IsScalarTower S (Localization (Submonoid.map f M)) S' :=
    IsLocalization.localization_isScalarTower_of_submonoid_le _ _ _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this_1 : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this : IsScalarTower S (Localization (Submonoid.map f M)) S'
⊢ P (R := R') (IsLocalization.map S' f hy)
have this₁ : IsLocalization
  (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
Tactic: have : IsLocalization (T.map (algebraMap S (Localization (M.map f)))) S' :=
    IsLocalization.isLocalization_of_submonoid_le _ _ (M.map f) T hle