awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
simp_rw :
  Eq.{u_3 + 1} (α := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (mk' (Localization (M := R) I.primeCompl) x y) :
      Localization.AtPrime J)
    (mk' (R := P) (M := J.primeCompl) (Localization (M := P) J.primeCompl) ((f : (a : R) → P) x : P)
        (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑y : R)) ⋯ : ↥J.primeCompl) :
      Localization (M := P) J.primeCompl)
⊢ Eq.{u_3 + 1} (α := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (mk x y) :
      Localization.AtPrime J)
    (mk ((f : (a : R) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑y : R)) ⋯) :
      Localization (M := P) J.primeCompl)

Tactic:
simp_rw [mk_eq_mk', localRingHom_mk']

Premises used: Localization.mk_eq_mk', Localization.localRingHom_mk'
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
hx :
  IsUnit.{u_3} (M := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        x :
      Localization.AtPrime J)
rcases :
  ∀ (r : R) (s : ↥I.primeCompl)
    (hx :
      IsUnit.{u_3} (M := Localization.AtPrime J)
        (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
              (a : Localization.AtPrime I) → Localization.AtPrime J)
            (mk' (Localization.AtPrime I) r s) :
          Localization.AtPrime J)),
    IsUnit (M := Localization.AtPrime I) (mk' (Localization.AtPrime I) r s)
⊢ IsUnit x

Tactic:
rcases IsLocalization.exists_mk'_eq I.primeCompl x with ⟨r, s, rfl⟩

Premises used: Localization.r, Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx :
  IsUnit.{u_3} (M := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (mk' (Localization.AtPrime I) r s) :
      Localization.AtPrime J)
⊢ IsUnit.{u_3} (M := Localization.AtPrime J)
    (mk' (R := P) (M := J.primeCompl) (Localization.AtPrime J) ((f : (a : R) → P) r : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑s : R)) ⋯ : ↥J.primeCompl))

Tactic:
rw [localRingHom_mk'] at hx

Premises used: Localization.localRingHom_mk'
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx :
  IsUnit.{u_3} (M := Localization.AtPrime J)
    (mk' (R := P) (M := J.primeCompl) (Localization.AtPrime J) ((f : (a : R) → P) r : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑s : R)) ⋯ : ↥J.primeCompl))
rw : ∀ (hx : Membership.mem (α := P) J.primeCompl ((f : (a : R) → P) r : P)), r ∈ I.primeCompl
⊢ IsUnit (M := Localization.AtPrime I) (mk' (Localization.AtPrime I) r s)

Tactic:
rw [AtPrime.isUnit_mk'_iff] at hx ⊢

Premises used: IsLocalization.AtPrime.isUnit_mk'_iff
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : Membership.mem (α := P) J.primeCompl ((f : (a : R) → P) r : P)
⊢ r ∈ I.primeCompl

Tactic:
fun hr => hx ((SetLike.ext_iff.mp hIJ r).mp hr)

Premises used: Set.Mem, setOf, SetLike.ext_iff, Iff.mp, Not
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : Membership.mem (α := P) J.primeCompl ((f : (a : R) → P) r : P)
⊢ r ∈ I.primeCompl

Tactic:
exact fun hr => hx ((SetLike.ext_iff.mp hIJ r).mp hr)

Premises used: SetLike.ext_iff, Iff.mp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
j : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)
hj :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := Localization.AtPrime J)
      ((j : (a : Localization.AtPrime I) → Localization.AtPrime J)
          ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) x) :
        Localization.AtPrime J)
      ((algebraMap P (Localization.AtPrime J) : (a : P) → Localization.AtPrime J) ((f : (a : R) → P) x) :
        Localization.AtPrime J)
⊢ localRingHom I J f hIJ = j

Tactic:
map_unique _ _ hj

Premises used: Localization.localRingHom, IsLocalization.map_unique
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ Eq (α := Localization.AtPrime I →+* Localization.AtPrime I) (localRingHom I I (RingHom.id R) ⋯)
    (RingHom.id (Localization.AtPrime I))

Tactic:
localRingHom_unique _ _ _ _ fun _ => rfl

Premises used: Localization.localRingHom_unique, rfl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst_4 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
rw : Eq (α := Ideal R) (Ideal.comap f J) (Ideal.comap (g.comp f) K)
rw₁ : Eq (α := Ideal R) (Ideal.comap f (Ideal.comap g K)) (Ideal.comap (g.comp f) K)
rw₂ rw₃ : Eq (α := Ideal R) (Ideal.comap (g.comp f) K) (Ideal.comap (g.comp f) K)
⊢ I = Ideal.comap (g.comp f) K

Tactic:
rw [hIJ, hJK, Ideal.comap_comap f g]

Premises used: Ideal.comap_comap
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst_2 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
r : R
⊢ Eq.{u_3 + 1} (α := Localization.AtPrime K)
    (((RingHom.comp (β := Localization.AtPrime J) (localRingHom J K g hJK) (localRingHom I J f hIJ) :
            RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime K)) :
          (a : Localization.AtPrime I) → Localization.AtPrime K)
        ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) r) :
      Localization.AtPrime K)
    ((algebraMap P (Localization.AtPrime K) : (a : P) → Localization.AtPrime K) ((g.comp f : (a : R) → P) r) :
      Localization.AtPrime K)

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, localRingHom_to_map]

Premises used: Localization.localRingHom_to_map, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
rw : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap f J)
rw₁ : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap (F := R →+* P) (↑f : R →+* P) J)
rw₂ :
  J =
    Ideal.comap (F := P →+* P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* P) (↑f.symm : P →+* R))
      J
rw₃ : J = Ideal.comap (F := P →+* P) (RingHom.id P) J
rw₄ rw₅ : J = J
⊢ J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) I

Tactic:
rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]

Premises used: Ideal.comap_coe, Ideal.comap_id, RingEquiv.comp_symm, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
⊢ ((localRingHom J I (↑f.symm : P →+* R) ⋯ : RingHom.{u_3, u_1} (Localization.AtPrime J) (Localization.AtPrime I)) :
        (a : Localization.AtPrime J) → Localization.AtPrime I)
      (OneHom.toFun
        (↑(↑(localRingHom I J (↑f : R →+* P) hIJ) : Localization.AtPrime I →* Localization.AtPrime J) :
          OneHom (Localization.AtPrime I) (Localization.AtPrime J))
        x) =
    x

Tactic:
simp [localRingHom, map_map]

Premises used: Localization.localRingHom, IsLocalization.map_map
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime J
⊢ OneHom.toFun (M := Localization.AtPrime I)
      (↑(↑(localRingHom I J (↑f : R →+* P) hIJ) : Localization.AtPrime I →* Localization.AtPrime J) :
        OneHom (Localization.AtPrime I) (Localization.AtPrime J))
      (((localRingHom J I (↑f.symm : P →+* R) ⋯ :
            RingHom.{u_3, u_1} (Localization.AtPrime J) (Localization.AtPrime I)) :
          (a : Localization.AtPrime J) → Localization.AtPrime I)
        x) =
    x

Tactic:
simp [localRingHom, map_map]

Premises used: Localization.localRingHom, IsLocalization.map_map
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I_1 : Ideal R
hI : I_1.IsPrime
inst_4 : Algebra R P
I : Ideal S
inst_5 : I.IsPrime
J : Ideal P
inst_6 : J.IsPrime
f : S →ₐ[R] P
hIJ : I = Ideal.comap f J
r : R
⊢ Eq (α := Localization.AtPrime J)
    (OneHom.toFun (M := Localization.AtPrime I)
      (↑(↑(localRingHom I J f.toRingHom hIJ) : Localization.AtPrime I →* Localization.AtPrime J) :
        OneHom (Localization.AtPrime I) (Localization.AtPrime J))
      ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) r))
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) r)

Tactic:
simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime I),
      localRingHom_to_map, IsScalarTower.algebraMap_apply R P (Localization.AtPrime J)]

Premises used: Localization.localRingHom_to_map, Localization.AtPrime, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
I : Ideal S
inst_5 : I.IsPrime
J : Ideal P
inst_6 : J.IsPrime
f : S →ₐ[R] P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
⊢ Eq.{u_3 + 1} (α := Localization.AtPrime J)
    (((localAlgHom I J f hIJ : AlgHom.{u_1, u_2, u_3} R (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        x :
      Localization.AtPrime J)
    (((localRingHom I J f.toRingHom hIJ : RingHom.{u_2, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        x :
      Localization.AtPrime J)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
I : Ideal R
hI : I.IsPrime
P : Ideal S
inst_4 : P.IsPrime
s : Subalgebra R S
⊢ P.primeCompl ⊓ s.toSubmonoid ≤ s.toSubmonoid

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
left :
  Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
right :
  Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
⊢ Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
this :
  ∀ a ∈ s,
    ∀ b ∈ s,
      b ∉ P →
        ∀ c ∈ s,
          ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)

Tactic:
simpa [Function.Injective, (IsLocalization.mk'_surjective p.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq', Subtype.ext_iff, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, IsLocalization.eq_iff_exists p.primeCompl]

Premises used: IsLocalization.mk'_surjective, Function.Surjective.forall, Localization.localRingHom_mk', Subtype.ext_iff, map_mul, Ideal.primeCompl, Ideal.over_def, Function.Injective, IsLocalization.mk'_eq_iff_eq', IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
left :
  ∀ a ∈ s,
    ∀ b ∈ s,
      b ∉ P →
        ∀ c ∈ s,
          ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)

Tactic:
suffices ∀ a ∈ s, ∀ b ∈ s, b ∉ P → ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P,
        x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b) by
      simpa [Function.Injective, (IsLocalization.mk'_surjective p.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq', Subtype.ext_iff, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, IsLocalization.eq_iff_exists p.primeCompl]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
left :
  a ∈ s →
    ∀ b ∈ s,
      b ∉ P →
        ∀ c ∈ s,
          ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ a ∈ s →
    ∀ b ∈ s,
      b ∉ P →
        ∀ c ∈ s,
          ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
_
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
left :
  b ∈ s →
    b ∉ P →
      ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ b ∈ s →
    b ∉ P →
      ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
_
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
left :
  b ∉ P →
    ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ b ∉ P →
    ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
_
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
h_2 : b ∉ P
c : S
left : c ∈ s → ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ c ∈ s → ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
_
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
h_2 : b ∉ P
c : S
h_3 : c ∈ s
d : S
left : d ∈ s → d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ d ∈ s → d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
_
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
h_2 : b ∉ P
c : S
h_3 : c ∈ s
d : S
h_4 : d ∈ s
left : d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
_
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
h_2 : b ∉ P
c : S
h_3 : c ∈ s
d : S
h_4 : d ∈ s
h_5 : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
left :
  ∀ (t : S) (ht : t * x ∈ s) (htP : t ∈ (↑P.primeCompl : Set S)), ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
obtain ⟨t, ⟨htP, -⟩, ht⟩ := H.ge (Set.mem_univ x)

Premises used: Eq.ge, Set.mem_univ
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
h_2 : b ∉ P
c : S
h_3 : c ∈ s
d : S
h_4 : d ∈ s
h_5 : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
t : S
ht : t * x ∈ s
htP : t ∈ (↑P.primeCompl : Set S)
⊢ t * x * (a * d) = t * x * (c * b)

Tactic:
simp [mul_assoc, e]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
h_2 : b ∉ P
c : S
h_3 : c ∈ s
d : S
h_4 : d ∈ s
h_5 : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
t : S
ht : t * x ∈ s
htP : t ∈ (↑P.primeCompl : Set S)
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
exact ⟨_, ‹P.IsPrime›.mul_notMem htP hxP, ht, by simp [mul_assoc, e]⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
this : ∀ (y z : S), z ∉ P → ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)

Tactic:
simpa [(IsLocalization.mk'_surjective p.primeCompl).exists,
        (IsLocalization.mk'_surjective P.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, Function.Surjective] using this

Premises used: IsLocalization.mk'_surjective, Function.Surjective.forall, Localization.localRingHom_mk', Function.Surjective.exists, IsLocalization.mk'_eq_iff_eq, map_mul, Ideal.primeCompl, Ideal.over_def, Function.Surjective, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
right : ∀ (y z : S), z ∉ P → ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)

Tactic:
suffices ∀ y, ∀ z ∉ P, ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y) by
      simpa [(IsLocalization.mk'_surjective p.primeCompl).exists,
        (IsLocalization.mk'_surjective P.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, Function.Surjective] using this