awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : Nontrivial Rₛ
inst_11 : IsLocalization S Rₛ
inst_12 : FinitePresentation R M
inst_13 : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this_1 : Module.Finite Rₛ M'
r : R
hr : r ∈ S
b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)
h :
  ∀ (i : I),
    Eq.{u_1 + 1} (α := M')
      ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
          ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
        M')
      ((b : (a : I) → M') i : M')
this : Nontrivial.{u_4} (Localization (Submonoid.powers r))
rw : finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = Nat.card I
⊢ finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
have rw₁ : Nat.card I = Nat.card I
Tactic: rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b']
-- 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
x : R
y : ↥M
I : Ideal S
⊢ mk' S x y ∈ I ↔ Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)
have mp : mk' S x y ∈ I → Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)
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
x : R
y : ↥M
I : Ideal S
mp : mk' S x y ∈ I → Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)
⊢ mk' S x y ∈ I ↔ Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)
have mpr : Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S) → mk' S x y ∈ I
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
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)
have mp : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) (mk' S x y) ∈ I
Tactic: rw [← mk'_spec S x y, mul_comm]
-- 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
x : R
y : ↥M
I : Ideal S
h : Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)
⊢ mk' S x y ∈ I
have h₁ : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
Tactic: rw [← mk'_spec S x y] at 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
x : R
y : ↥M
I : Ideal S
h : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
⊢ mk' S x y ∈ I
have mpr : ∀ (b : S) (hb : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b = 1), mk' S x y ∈ I
Tactic: obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (map_units S y)
-- 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
x : R
y : ↥M
I : Ideal S
h : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
b : S
hb : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b = 1
⊢ mk' S x y ∈ I
have this : b * HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
Tactic: have := I.mul_mem_left b 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
x : R
y : ↥M
I : Ideal S
h : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
b : S
hb : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b = 1
this : b * HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
⊢ mk' S x y ∈ I
have mpr : ∀ (this : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) * b ∈ I), mk' S x y ∈ I
Tactic: rwa [mul_comm, mul_assoc, hb, mul_one] at this
Cleared hypotheses: this
-- 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
x : R
y : ↥M
I : Ideal S
h : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
b : S
hb : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b = 1
this : b * HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
mpr : ∀ (this : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) * b ∈ I), mk' S x y ∈ I
⊢ mk' S x y ∈ I
have mpr₁ : ∀ (this : mk' S x y * HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b ∈ I), mk' S x y ∈ I
Tactic: rwa [mul_comm, mul_assoc, hb, mul_one] at this
Cleared hypotheses: this
-- 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
x : R
y : ↥M
I : Ideal S
h : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
b : S
hb : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b = 1
this : b * HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
mpr : ∀ (this : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) * b ∈ I), mk' S x y ∈ I
mpr₁ : ∀ (this : mk' S x y * HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b ∈ I), mk' S x y ∈ I
⊢ mk' S x y ∈ I
have mpr₂ : ∀ (this : mk' S x y * 1 ∈ I), mk' S x y ∈ I
Tactic: rwa [mul_comm, mul_assoc, hb, mul_one] at this
Cleared hypotheses: this
-- 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
x : R
y : ↥M
I : Ideal S
h : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
b : S
hb : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b = 1
this : b * HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ∈ I
mpr : ∀ (this : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) * b ∈ I), mk' S x y ∈ I
mpr₁ : ∀ (this : mk' S x y * HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b ∈ I), mk' S x y ∈ I
mpr₂ : ∀ (this : mk' S x y * 1 ∈ I), mk' S x y ∈ I
⊢ mk' S x y ∈ I
have mpr₃ : ∀ (this : mk' S x y ∈ I), mk' S x y ∈ I
Tactic: rwa [mul_comm, mul_assoc, hb, mul_one] at this
Cleared hypotheses: this
-- 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
a b : S
a' : ↥I × ↥M
ha : HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑a'.1 : R)
b' : ↥I × ↥M
hb : HMul.hMul (β := S) b ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑b'.1 : R)
Z : ↥I := Subtype.mk (p := fun (x : R) ↦ x ∈ I) ((↑a'.2 : R) * (↑b'.1 : R) + (↑b'.2 : R) * (↑a'.1 : R)) ⋯
⊢ Membership.mem (γ := Set S)
    {z : S |
      ∃ (x : ↥I × ↥M),
        HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
          (algebraMap R S : (a : R) → S) (↑x.1 : R)}
    (a + b)
have h : HMul.hMul (β := S) (a + b) ((algebraMap R S : (a : R) → S) (↑(Z, a'.2 * b'.2).2 : R) : S) =
  (algebraMap R S : (a : R) → S) (↑(Z, a'.2 * b'.2).1 : R)
Tactic: use ⟨Z, a'.2 * 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
I : Ideal R
a b : S
a' : ↥I × ↥M
ha : HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑a'.1 : R)
b' : ↥I × ↥M
hb : HMul.hMul (β := S) b ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑b'.1 : R)
Z : ↥I := Subtype.mk (p := fun (x : R) ↦ x ∈ I) ((↑a'.2 : R) * (↑b'.1 : R) + (↑b'.2 : R) * (↑a'.1 : R)) ⋯
⊢ HMul.hMul (β := S) (a + b) ((algebraMap R S : (a : R) → S) (↑(Z, a'.2 * b'.2).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Z, a'.2 * b'.2).1 : R)
have h : (a + b) *
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑b'.1 : R) : S) +
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑a'.1 : R) : S)
Tactic: simp only [Z, map_add, Submonoid.coe_mul, map_mul]
-- 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
a b : S
a' : ↥I × ↥M
ha : HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑a'.1 : R)
b' : ↥I × ↥M
hb : HMul.hMul (β := S) b ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑b'.1 : R)
Z : ↥I := Subtype.mk (p := fun (x : R) ↦ x ∈ I) ((↑a'.2 : R) * (↑b'.1 : R) + (↑b'.2 : R) * (↑a'.1 : R)) ⋯
⊢ (a + b) *
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S)
        ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S)
        ((algebraMap R S : (a : R) → S) (↑b'.1 : R) : S) +
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S)
        ((algebraMap R S : (a : R) → S) (↑a'.1 : R) : S)
have h : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑a'.1 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S) +
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑b'.1 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑a'.2 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑b'.1 : R) : S) +
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑b'.2 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑a'.1 : R) : S)
Tactic: rw [add_mul, ← mul_assoc a, ha, mul_comm (algebraMap R S a'.2) (algebraMap R S b'.2), ←
      mul_assoc b, hb]
-- 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
c x : S
x' : ↥I × ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑x'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x'.1 : R)
⊢ Membership.mem (γ := Set S)
    {z : S |
      ∃ (x : ↥I × ↥M),
        HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
          (algebraMap R S : (a : R) → S) (↑x.1 : R)}
    (c • x)
have obtain : ∀ (c' : R × ↥M)
  (hc : HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) (↑c'.2 : R) : S) = (algebraMap R S : (a : R) → S) c'.1),
  Membership.mem (γ := Set S)
    {z : S |
      ∃ (x : ↥I × ↥M),
        HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
          (algebraMap R S : (a : R) → S) (↑x.1 : R)}
    (c • x)
Tactic: obtain ⟨c', hc⟩ := IsLocalization.surj M c
-- 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
c x : S
x' : ↥I × ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑x'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x'.1 : R)
c' : R × ↥M
hc : HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) (↑c'.2 : R) : S) = (algebraMap R S : (a : R) → S) c'.1
Z : ↥I := Subtype.mk (p := fun (x : R) ↦ x ∈ I) (c'.1 * (↑x'.1 : R)) ⋯
⊢ Membership.mem (γ := Set S)
    {z : S |
      ∃ (x : ↥I × ↥M),
        HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
          (algebraMap R S : (a : R) → S) (↑x.1 : R)}
    (c • x)
have h : HMul.hMul (β := S) (c • x) ((algebraMap R S : (a : R) → S) (↑(Z, c'.2 * x'.2).2 : R) : S) =
  (algebraMap R S : (a : R) → S) (↑(Z, c'.2 * x'.2).1 : R)
Tactic: use ⟨Z, c'.2 * x'.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
I : Ideal R
c x : S
x' : ↥I × ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑x'.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x'.1 : R)
c' : R × ↥M
hc : HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) (↑c'.2 : R) : S) = (algebraMap R S : (a : R) → S) c'.1
Z : ↥I := Subtype.mk (p := fun (x : R) ↦ x ∈ I) (c'.1 * (↑x'.1 : R)) ⋯
⊢ HMul.hMul (β := S) (c • x) ((algebraMap R S : (a : R) → S) (↑(Z, c'.2 * x'.2).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Z, c'.2 * x'.2).1 : R)
have h : c * x *
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑c'.2 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑x'.2 : R) : S) =
  HMul.hMul (β := S) c ((algebraMap R S : (a : R) → S) (↑c'.2 : R) : S) *
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑x'.2 : R) : S)
Tactic: simp only [Z, ← hx, ← hc, smul_eq_mul, Submonoid.coe_mul, map_mul]
-- 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
z : S
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z ↔
    ∃ (x : ↥I × ↥M),
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x.1 : R)
have mp : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z →
  ∃ (x : ↥I × ↥M),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x.1 : 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
I : Ideal R
z : S
mp :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z →
    ∃ (x : ↥I × ↥M),
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x.1 : R)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z ↔
    ∃ (x : ↥I × ↥M),
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x.1 : R)
have mpr : (∃ (x : ↥I × ↥M),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) (↑x.1 : R)) →
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z
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
I : Ideal R
z : S
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z →
    Membership.mem (γ := Ideal S) (map_ideal M S I) z
have mp : ∀ (h : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z) (z : S)
  (hz : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)) z),
  z ∈ (↑(map_ideal M S I) : Set S)
Tactic: refine fun h => Ideal.mem_sInf.1 h fun z hz => ?_
-- 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
z_1 : S
h : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z_1
z : S
hz : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)) z
⊢ z ∈ (↑(map_ideal M S I) : Set S)
have mp : ∀ (y : R) (hy : y ∈ (↑I : Set R) ∧ (algebraMap R S : (a : R) → S) y = z), z ∈ (↑(map_ideal M S I) : Set S)
Tactic: obtain ⟨y, hy⟩ := hz
Cleared hypotheses: hz
-- 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
z_1 : S
h : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z_1
z : S
y : R
hy : y ∈ (↑I : Set R) ∧ (algebraMap R S : (a : R) → S) y = z
Z : ↥I := Subtype.mk (p := fun (x : R) ↦ x ∈ I) y ⋯
⊢ z ∈ (↑(map_ideal M S I) : Set S)
have h₁ : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(Z, 1).2 : R) : S) =
  (algebraMap R S : (a : R) → S) (↑(Z, 1).1 : R)
Tactic: use ⟨Z, 1⟩
-- 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
z : S
a : ↥I
s : ↥M
h :
  HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(a, s).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(a, s).1 : R)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z
have mpr : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
  (HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑s : R) : S))
Tactic: rw [← Ideal.unit_mul_mem_iff_mem _ (map_units S s), mul_comm]
-- 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
x : R
s : ↥M
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (mk' S x s) ↔ ∃ s ∈ M, s * x ∈ I
have rw : (∃ (x_1 : ↥I × ↥M),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
        ((algebraMap R S : (a : R) → S) (↑x_1.2 : R) : S) =
      (algebraMap R S : (a : R) → S) (↑x_1.1 : R)) ↔
  ∃ s ∈ M, s * x ∈ I
Tactic: rw [← Ideal.unit_mul_mem_iff_mem _ (IsLocalization.map_units S s), IsLocalization.mk'_spec',
    IsLocalization.mem_map_algebraMap_iff M]
-- 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
x : R
s : ↥M
⊢ (∃ (x_1 : ↥I × ↥M),
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
          ((algebraMap R S : (a : R) → S) (↑x_1.2 : R) : S) =
        (algebraMap R S : (a : R) → S) (↑x_1.1 : R)) ↔
    ∃ s ∈ M, s * x ∈ I
have simp_rw : (∃ (x_1 : ↥I × ↥M) (c : ↥M), (↑(c * x_1.2) : R) * x = (↑c : R) * (↑x_1.1 : R)) ↔ ∃ s ∈ M, s * x ∈ I
Tactic: simp_rw [← map_mul, IsLocalization.eq_iff_exists M, mul_comm x, ← mul_assoc, ← Submonoid.coe_mul]
-- 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
x : 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) x : S) ↔
    ∃ m ∈ M, m * x ∈ I
have rw : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (mk' (M := M) S x 1) ↔ ∃ m ∈ M, m * x ∈ I
Tactic: rw [← IsLocalization.mk'_one (M := M), mk'_mem_map_algebraMap_iff]
-- 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
x : R
rw :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (mk' (M := M) S x 1) ↔ ∃ m ∈ M, m * x ∈ I
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
      ((algebraMap R S : (a : R) → S) x : S) ↔
    ∃ m ∈ M, m * x ∈ I
have rw₁ : (∃ s ∈ M, s * x ∈ I) ↔ ∃ m ∈ M, m * x ∈ I
Tactic: rw [← IsLocalization.mk'_one (M := M), mk'_mem_map_algebraMap_iff]
-- 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
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤ ↔ Disjoint (↑M : Set R) (↑I : Set R)
have simp : ¬Disjoint (↑M : Set R) (↑I : Set R) ↔ ∃ m ∈ M, m * 1 ∈ I
Tactic: simp only [ne_eq, Ideal.eq_top_iff_one, ← map_one (algebraMap R S), not_iff_comm,
    IsLocalization.algebraMap_mem_map_algebraMap_iff M]
-- 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
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ⊓ J))
    (Ideal.map (F := R →+* S) (algebraMap R S) I ⊓ Ideal.map (F := R →+* S) (algebraMap R S) J)
have refine : ∀ (x : S)
  (hx :
    Membership.mem (γ := Submodule S S)
      (Ideal.map (F := R →+* S) (algebraMap R S) I ⊓ Ideal.map (F := R →+* S) (algebraMap R S) J) x),
  Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ⊓ J)) x
Tactic: refine le_antisymm (Ideal.map_inf_le (algebraMap R S)) fun x 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 J : Ideal R
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Ideal.map (F := R →+* S) (algebraMap R S) I ⊓ Ideal.map (F := R →+* S) (algebraMap R S) J) x
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ⊓ J)) x
have simp : ∀
  (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)
Tactic: simp only [Ideal.mem_inf, IsLocalization.mem_map_algebraMap_iff M, Prod.exists] at hx ⊢
Cleared hypotheses: hx