awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
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:
simp [RingHom.algebraMap_toAlgebra, Localization.awayMap, IsLocalization.Away.map,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra]

Premises used: IsLocalization.Away.map, Algebra.TensorProduct.tmul_one_eq_one_tmul, Localization.awayMap, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
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))
⊢ 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]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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))))
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))))
⊢ P (R := Localization.Away r) (S := Localization.Away r ⊗[R] S)
    (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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)
    (@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:
hP.1 _ _ (hf ⟨r, hr⟩)

Premises used: Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, Subtype.mk, MulEquiv.toMonoidHom, And.left, RingHomClass.toRingHom, RingEquiv.toRingHom
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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)
    (@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:
exact hP.1 _ _ (hf ⟨r, hr⟩)

Premises used: Subtype.mk, And.left
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
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)))
⊢ P (algebraMap R S)

Tactic:
rw [← (IsLocalization.algEquiv M (Localization M) S).toAlgHom.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom, Localization, IsLocalization.algEquiv
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
    (@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:
hP.1 _ _ (H _)

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, And.left, RingHomClass.toRingHom, RingEquiv.toRingHom
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
    (@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:
exact hP.1 _ _ (H _)

Premises used: And.left
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P

Tactic:
fun _ _ _ _ _ r _ ↦ hP _ (Submonoid.powers r)

Premises used: RingHom.HoldsForLocalizationAway, Submonoid.powers
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
⊢ Submonoid.map f M ≤ T

Tactic:
simpa [Submonoid.map_le_iff_le_comap]

Premises used: Submonoid.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
have : ∀ (hle : Submonoid.map f M ≤ T), P (R := R') (IsLocalization.map S' f hy)
⊢ P (R := R') (IsLocalization.map S' f hy)

Tactic:
have hle : Submonoid.map f M ≤ T := by simpa [Submonoid.map_le_iff_le_comap]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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
⊢ IsScalarTower S (Localization (Submonoid.map f M)) S'

Tactic:
have : IsScalarTower S (Localization (Submonoid.map f M)) S' :=
    IsLocalization.localization_isScalarTower_of_submonoid_le _ _ _ _ _
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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'
⊢ 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
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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_2 : IsScalarTower S (Localization (Submonoid.map f M)) S'
this :
  IsLocalization
    (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
h :
  Eq (α := R →+* S') (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map S' f hy) (algebraMap R R'))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
        (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
      (algebraMap R R'))
⊢ Eq (α := R' →+* S') (IsLocalization.map S' f hy)
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))

Tactic:
apply IsLocalization.ringHom_ext M

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.LocalProperties.Basic
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_2 : IsScalarTower S (Localization (Submonoid.map f M)) S'
this :
  IsLocalization
    (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
h :
  ∀ (x : R),
    Eq (α := S')
      ((@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map S' f hy) (algebraMap R R') : (a : R) → S') x :
        S')
      ((@comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
                (algebraMap (Localization (Submonoid.map f M)) S')
                (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
              (algebraMap R R') :
            (a : R) → S')
          x :
        S')
⊢ Eq (α := R →+* S') (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map S' f hy) (algebraMap R R'))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
        (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
      (algebraMap R R'))

Tactic:
ext