awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
have x : S
Tactic: apply Ideal.eq_top_of_isUnit_mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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
⊢ ∃ (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
have 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)
Tactic: obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨r, ⟨m, hm⟩, rfl⟩ := exists_mk'_eq M s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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
⊢ ∃ (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)
have 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)
Tactic: by_cases hM : (Ideal.Quotient.mk (I.comap (algebraMap R S))) m = 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: by_cases hM : (Ideal.Quotient.mk (I.comap (algebraMap R S))) m = 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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 = ⊤
have rw : 1 ∈ I
Tactic: rw [Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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))
⊢ 1 ∈ I
have hM₁ : 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
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ 1 ∈ I
have 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))
Tactic: convert! I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ 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))
have h : 1 = mk' S m (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
Tactic: rw [← mk'_eq_mul_mk'_one, mk'_self]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ 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))
have h₁ : Eq.{u_2 + 1} (α := S) 1 1
Tactic: rw [← mk'_eq_mul_mk'_one, mk'_self]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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))
⊢ ∃ (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)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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))
⊢ ∃ (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)
have 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)
Tactic: rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient] at hI
Cleared hypotheses: hI, r, m, hm, hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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))
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨n, hn⟩ := hI.3 hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨rn, rfl⟩ := Ideal.Quotient.mk_surjective n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I)
        ((Ideal.Quotient.mk J : (a : R) → R ⧸ J) (r * rn)) :
      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)
have hn₁ : Eq.{u_2 + 1} (α := S ⧸ I)
  ((Ideal.quotientMap I (algebraMap R S) sorry : (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) sorry : (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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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 :
  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)
⊢ 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)
        ((Ideal.Quotient.mk J : (a : R) → R ⧸ J) (r * rn)) :
      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)
have hn₁ : HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
    ((Ideal.quotientMap I (algebraMap R S) sorry : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
        ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m) :
      S ⧸ I)
    ((Ideal.quotientMap I (algebraMap R S) sorry : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
        ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn) :
      S ⧸ I) =
  1
Tactic: rw [map_one, map_mul] at hn
Cleared hypotheses: hn