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 J : Ideal R
x : S
hx :
  (∃ (a : ↥I) (b : ↥M),
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)) ∧
    ∃ (a : ↥J) (b : ↥M),
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
have obtain : ∀ (i : R) (hi : i ∈ I) (mi : ↥M)
  (hi' :
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mi : R) : S) =
      (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R))
  (j : R) (hj : j ∈ J) (mj : ↥M)
  (hj' :
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mj : R) : S) =
      (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ J) j hj) : R)),
  ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
Tactic: obtain ⟨⟨⟨i, hi⟩, mi, hi'⟩, ⟨j, hj⟩, mj, hj'⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
hi' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mi : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R)
j : R
hj : j ∈ J
mj : ↥M
hj' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mj : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ J) j hj) : R)
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
have hi'₁ : x = mk' S i mi
Tactic: simp only [← IsLocalization.eq_mk'_iff_mul_eq] at hi' hj'
Cleared hypotheses: hi', hj'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
hi' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mi : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R)
j : R
hj : j ∈ J
mj : ↥M
hj' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mj : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ J) j hj) : R)
hi'₁ : x = mk' S i mi
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
have hj'₁ : x = mk' S j mj
Tactic: simp only [← IsLocalization.eq_mk'_iff_mul_eq] at hi' hj'
Cleared hypotheses: hi', hj'
-- 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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
have obtain : ∀ (m : ↥M) (hm : (↑m : R) * ((↑mj : R) * i) = (↑m : R) * ((↑mi : R) * j)),
  ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
Tactic: obtain ⟨m, hm⟩ := IsLocalization.eq.mp (hi'.symm.trans hj')
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : (↑m : R) * ((↑mj : R) * i) = (↑m : R) * ((↑mi : R) * j)
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
have hm₁ : i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))
Tactic: rw [← mul_assoc, ← mul_assoc, mul_comm, ← mul_comm (j : R)] at hm
Cleared hypotheses: hm
-- 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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
have refine : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(mi * (m * mj)) : R) : S) =
  (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) sorry) : R)
Tactic: refine ⟨⟨i * (m * mj : M), I.mul_mem_right _ hi, hm ▸ J.mul_mem_right _ hj⟩, mi * (m * mj), ?_⟩
-- 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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))
⊢ HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(mi * (m * mj)) : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) ⋯) : R)
have rwa : x = mk' S (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) sorry) : R) (mi * (m * mj))
Tactic: rwa [← IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, IsLocalization.mk'_cancel]
-- 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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))
rwa : x = mk' S (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) ⋯) : R) (mi * (m * mj))
⊢ HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(mi * (m * mj)) : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) ⋯) : R)
have rwa₁ : x = mk' S (i * (↑(m * mj) : R)) (mi * (m * mj))
Tactic: rwa [← IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, IsLocalization.mk'_cancel]
-- 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
J : Ideal S
x : S
hJ : x ∈ J
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) x
have obtain : ∀ (r : R) (s : ↥M) (hx : mk' S r s = x),
  Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) x
Tactic: obtain ⟨r, s, hx⟩ := exists_mk'_eq M x
-- 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
J : Ideal S
x : S
hJ : x ∈ J
r : R
s : ↥M
hx : mk' S r s = x
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) x
have rw : ∀ (hJ : mk' S r s ∈ J) (hx : mk' S r s = x),
  Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) (mk' S r s)
Tactic: rw [← hx] at hJ ⊢
Cleared hypotheses: hJ, hx
-- 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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
⊢ Disjoint (↑M : Set R) (↑I.radical : Set R)
have contrapose : ∀ (hM : ¬Disjoint (↑M : Set R) (↑I.radical : Set R)), ¬Disjoint (↑M : Set R) (↑I : Set R)
Tactic: contrapose hM
Cleared hypotheses: hM
-- 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
hI : I.IsPrimary
hM : ¬Disjoint (↑M : Set R) (↑I.radical : Set R)
⊢ ¬Disjoint (↑M : Set R) (↑I : Set R)
have rw : ∀ (hM : ∃ x ∈ (↑M : Set R), x ∈ (↑I.radical : Set R)), ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)
Tactic: rw [Set.not_disjoint_iff] at hM ⊢
Cleared hypotheses: hM
-- 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
hI : I.IsPrimary
hM : ∃ x ∈ (↑M : Set R), x ∈ (↑I.radical : Set R)
⊢ ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)
have obtain : ∀ (a : R) (ha : a ∈ (↑M : Set R)) (k : ℕ) (hk : a ^ k ∈ I), ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)
Tactic: obtain ⟨a, ha, k, hk⟩ := hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
⊢ Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I
have key : Disjoint (↑M : Set R) (↑I.radical : Set R)
Tactic: have key : Disjoint (M : Set R) I.radical := by
    contrapose hM
    rw [Set.not_disjoint_iff] at hM ⊢
    obtain ⟨a, ha, k, hk⟩ := hM
    exact ⟨a ^ k, pow_mem ha k, hk⟩
-- 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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
⊢ Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I
have refine : ∀ (a : R)
  (ha :
    Membership.mem (γ := Submodule R R)
      (Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) a),
  a ∈ I
Tactic: refine le_antisymm (fun a ha ↦ ?_) Ideal.le_comap_map
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
ha :
  Membership.mem (γ := Submodule R R) (Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    a
⊢ a ∈ I
have ha₁ : ∃ (x : ↥I × ↥M),
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑x.1 : R)
Tactic: rw [Ideal.mem_comap, IsLocalization.mem_map_algebraMap_iff M S] at ha
Cleared hypotheses: ha
-- 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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
ha :
  ∃ (x : ↥I × ↥M),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
      (algebraMap R S : (a : R) → S) (↑x.1 : R)
⊢ a ∈ I
have obtain : ∀ (b : ↥I) (s : ↥M)
  (h :
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
        ((algebraMap R S : (a : R) → S) (↑(b, s).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (↑(b, s).1 : R)),
  a ∈ I
Tactic: obtain ⟨⟨b, s⟩, h⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
b : ↥I
s : ↥M
h :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
      ((algebraMap R S : (a : R) → S) (↑(b, s).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(b, s).1 : R)
⊢ a ∈ I
have h₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S) ((algebraMap R S : (a : R) → S) (↑b : R) : S)
Tactic: replace h : algebraMap R S (s * a) = algebraMap R S b := by
    simpa only [← map_mul, mul_comm] using h
Cleared hypotheses: h
-- 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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
b : ↥I
s : ↥M
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S)
    ((algebraMap R S : (a : R) → S) (↑b : R) : S)
⊢ a ∈ I
have obtain : ∀ (c : ↥M) (hc : (↑c : R) * ((↑s : R) * a) = (↑c : R) * (↑b : R)), a ∈ I
Tactic: obtain ⟨c, hc⟩ := (IsLocalization.eq_iff_exists M S).1 h
-- 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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
b : ↥I
s : ↥M
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S)
    ((algebraMap R S : (a : R) → S) (↑b : R) : S)
c : ↥M
hc : (↑c : R) * ((↑s : R) * a) = (↑c : R) * (↑b : R)
⊢ a * (↑(c * s) : R) ∈ I
have rw : (↑c : R) * (↑b : R) ∈ I
Tactic: rw [mul_comm, Submonoid.coe_mul, mul_assoc, hc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
b : ↥I
s : ↥M
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S)
    ((algebraMap R S : (a : R) → S) (↑b : R) : S)
c : ↥M
hc : (↑c : R) * ((↑s : R) * a) = (↑c : R) * (↑b : R)
⊢ a ∈ I
have this : a * (↑(c * s) : R) ∈ I
Tactic: have : a * (c * s : M) ∈ I := by
    rw [mul_comm, Submonoid.coe_mul, mul_assoc, hc]
    exact I.mul_mem_left c b.2
-- 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
J₁ J₂ : Ideal S
⊢ LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R) ↔
    J₁ ≤ J₂
have mp : LE.le.{u_1} (α := Ideal R)
    ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := sorry } :
            Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
          (a : Ideal S) → Ideal R)
        J₁ :
      Ideal R)
    ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := sorry } :
            Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
          (a : Ideal S) → Ideal R)
        J₂ :
      Ideal R) →
  J₁ ≤ J₂
Tactic: constructor
-- 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
J₁ J₂ : Ideal S
mp :
  LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R) →
    J₁ ≤ J₂
⊢ LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R) ↔
    J₁ ≤ J₂
have mpr : J₁ ≤ J₂ →
  LE.le.{u_1} (α := Ideal R)
    ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := sorry } :
            Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
          (a : Ideal S) → Ideal R)
        J₁ :
      Ideal R)
    ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := sorry } :
            Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
          (a : Ideal S) → Ideal R)
        J₂ :
      Ideal R)
Tactic: constructor
-- 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
J : Ideal S
⊢ J.IsPrime ↔ Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
have mp : J.IsPrime → Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
Tactic: constructor
-- 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
J : Ideal S
mp : J.IsPrime → Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
⊢ J.IsPrime ↔ Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
have mpr : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) → J.IsPrime
Tactic: constructor
-- 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
J : Ideal S
⊢ J.IsPrime → Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
have mp : ∀ (h : J.IsPrime), Ne (α := Ideal R) (Ideal.under R J) ⊤
Tactic: refine fun h =>
      ⟨⟨?_, ?_⟩,
        Set.disjoint_left.mpr fun m hm1 hm2 =>
          h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
-- 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
J : Ideal S
mp : ∀ (h : J.IsPrime), Ne (α := Ideal R) (Ideal.under R J) ⊤
⊢ J.IsPrime → Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
have mp₁ : ∀ (h : J.IsPrime) {x y : R},
  Membership.mem (γ := Ideal R) (Ideal.under R J) (x * y) →
    Membership.mem (γ := Ideal R) (Ideal.under R J) x ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) y
Tactic: refine fun h =>
      ⟨⟨?_, ?_⟩,
        Set.disjoint_left.mpr fun m hm1 hm2 =>
          h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
-- 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
J : Ideal S
h : J.IsPrime
⊢ Ne (α := Ideal R) (Ideal.under R J) ⊤
have mp : ∀ (hJ : Eq (α := Ideal R) (Ideal.under R J) ⊤), J = ⊤
Tactic: refine fun hJ => h.ne_top ?_
-- 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
J : Ideal S
h : J.IsPrime
hJ : Eq (α := Ideal R) (Ideal.under R J) ⊤
⊢ J = ⊤
have mp : LE.le.{u_1} (α := Ideal R)
  (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) ⊤ : Ideal R)
  (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) J : Ideal R)
Tactic: rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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
J : Ideal S
h : J.IsPrime
x y : R
hxy : Membership.mem (γ := Ideal R) (Ideal.under R J) (x * y)
⊢ Membership.mem (γ := Ideal R) (Ideal.under R J) x ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) y
have hxy₁ : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ∈ J
Tactic: rw [Ideal.mem_comap, map_mul] at hxy
Cleared hypotheses: hxy
-- 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
J : Ideal S
⊢ Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) → J.IsPrime
have mpr : ∀ (h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)) (hJ : J = ⊤),
  LE.le (α := Ideal R) ⊤ (Ideal.under R J)
Tactic: refine fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 ?_), ?_⟩
-- 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
J : Ideal S
mpr :
  ∀ (h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)) (hJ : J = ⊤),
    LE.le (α := Ideal R) ⊤ (Ideal.under R J)
⊢ Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) → J.IsPrime
have mpr₁ : ∀ (h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)) {x y : S},
  x * y ∈ J → x ∈ J ∨ y ∈ J
Tactic: refine fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 ?_), ?_⟩
-- 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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
hJ : J = ⊤
⊢ LE.le (α := Ideal R) ⊤ (Ideal.under R J)
have mpr : ∀ (hJ : ⊤ ≤ J), LE.le (α := Ideal R) ⊤ (Ideal.under R J)
Tactic: rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ
Cleared hypotheses: hJ