awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ (↑I : Set R)
hny : y ∈ (↑M : Set R)
hx :
  Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((algebraMap R S : (a : R) → S) y : S)
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) y : S)
x : S
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤

Tactic:
apply Ideal.eq_top_of_isUnit_mem

Premises used: Ideal.eq_top_of_isUnit_mem
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ (↑I : Set R)
hny : y ∈ (↑M : Set R)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((algebraMap R S : (a : R) → S) y : S)

Tactic:
Ideal.mem_map_of_mem (algebraMap R _) hy

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ (↑I : Set R)
hny : y ∈ (↑M : Set R)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((algebraMap R S : (a : R) → S) y : S)

Tactic:
exact Ideal.mem_map_of_mem (algebraMap R _) hy

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ (↑I : Set R)
hny : y ∈ (↑M : Set R)
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
IsLocalization.map_units _ (⟨y, hny⟩ : M)

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ (↑I : Set R)
hny : y ∈ (↑M : Set R)
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
exact IsLocalization.map_units _ (⟨y, hny⟩ : M)

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
s : S ⧸ I
obtain :
  ∀ (s : S),
    ∃ (a : R ⧸ J),
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) s : S ⧸ I)
⊢ ∃ (a : R ⧸ J),
    ((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a = s

Tactic:
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
s : S
obtain :
  ∀ (r m : R) (hm : m ∈ M),
    ∃ (a : R ⧸ J),
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
⊢ ∃ (a : R ⧸ J),
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) s : S ⧸ I)

Tactic:
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := exists_mk'_eq M s

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
pos :
  ∀
    (hM :
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
        ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
              (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
            m :
          HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
        (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))),
    ∃ (a : R ⧸ J),
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
neg :
  ∀
    (hM :
      ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
                (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
              m :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))),
    ∃ (a : R ⧸ J),
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
⊢ ∃ (a : R ⧸ J),
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
by_cases hM : (Ideal.Quotient.mk (I.comap (algebraMap R S))) m = 0

Premises used: Algebra.algebraMap, Ideal.Quotient.mk, Ideal.comap, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) : (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
        m :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rw : 1 ∈ I
⊢ I = ⊤

Tactic:
rw [Ideal.eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) : (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
        m :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
⊢ Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) m : S)

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM

Premises used: Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM : Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) m : S)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) ∈ I

Tactic:
I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM

Premises used: Subtype.mk, IsLocalization.mk', Ideal.mul_mem_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM : Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) m : S)
h : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm))
⊢ 1 ∈ I

Tactic:
convert! I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM

Premises used: Subtype.mk, IsLocalization.mk', Ideal.mul_mem_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM : Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) m : S)
h : 1 = mk' S m (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
h₁ h₂ : Eq.{u_2 + 1} (α := S) 1 1
⊢ 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm))

Tactic:
rw [← mk'_eq_mul_mk'_one, mk'_self]

Premises used: IsLocalization.mk'_eq_mul_mk'_one, IsLocalization.mk'_self
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) : (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
        m :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
⊢ I = ⊤

Tactic:
have : I = ⊤ := by
      rw [Ideal.eq_top_iff_one]
      rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM
      convert! I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM
      rw [← mk'_eq_mul_mk'_one, mk'_self]
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) : (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
        m :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
this : I = ⊤
⊢ Eq (α := S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
    (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) 0 : S ⧸ I)

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem, this]

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) : (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
        m :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
this : I = ⊤
⊢ ∃ (a : R ⧸ J),
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
exact ⟨0, eq_comm.1 (by simp [Ideal.Quotient.eq_zero_iff_mem, this])⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : Ideal.IsMaximal (Ideal.under R I)
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
neg :
  ∀ (hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))) (r m : R) (hm : m ∈ M)
    (hM :
      ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
                (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
              m :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))),
    ∃ (a : R ⧸ J),
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
⊢ ∃ (a : R ⧸ J),
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient] at hI

Premises used: Ideal.Quotient.maximal_ideal_iff_isField_quotient
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
neg :
  ∀ (n : HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
    (hn :
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
                (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
              m :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          n =
        1),
    ∃ (a : R ⧸ J),
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
⊢ ∃ (a : R ⧸ J),
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
obtain ⟨n, hn⟩ := hI.3 hM

Premises used: IsField.mul_inv_cancel
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
n : HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I)
hn :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      n =
    1
neg :
  ∀ (rn : R)
    (hn :
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I)) (β :=
          HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
                (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
              m :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I : Ideal R)) =
        1),
    ∃ (a : R ⧸ J),
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
⊢ ∃ (a : R ⧸ J),
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
obtain ⟨rn, rfl⟩ := Ideal.Quotient.mk_surjective n

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I : Ideal R)) =
    1
⊢ ∃ (a : R ⧸ J),
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
⟨(Ideal.Quotient.mk J) (r * rn), ?_⟩

Premises used: HMul.hMul, Ideal.Quotient.mk, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I : Ideal R)) =
    1
⊢ Eq.{u_2 + 1} (α := S ⧸ I)
    ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
        (HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I)) (β :=
          HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
                (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
              m :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I : Ideal R))) :
      S ⧸ I)
    ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I) 1 : S ⧸ I)

Tactic:
replace hn := congr_arg (Ideal.quotientMap I (algebraMap R S) le_rfl) hn