awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Free
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))
refine : finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'

Tactic:
refine ⟨r, hr, .of_basis b', ?_⟩
-- Module: Mathlib.RingTheory.Localization.Free
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
rw₁ rw₂ : Nat.card I = Nat.card I
⊢ finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'

Tactic:
rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b']

Premises used: Module.finrank_eq_nat_card_basis
-- 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
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)
mpr : Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S) → mk' S x y ∈ I
⊢ mk' S x y ∈ I ↔ Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)

Tactic:
constructor
-- 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
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
mp : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) (mk' S x y) ∈ I
⊢ Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)

Tactic:
rw [← mk'_spec S x y, mul_comm]

Premises used: mul_comm, IsLocalization.mk'_spec
-- 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
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) (mk' S x y) ∈ I

Tactic:
I.mul_mem_left ((algebraMap R S) y) h

Premises used: Algebra.algebraMap, Set.Mem, Ideal.mul_mem_left, Subtype.val, DFunLike.coe
-- 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
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) (mk' S x y) ∈ I

Tactic:
exact I.mul_mem_left ((algebraMap R S) y) h

Premises used: Algebra.algebraMap, Ideal.mul_mem_left, Subtype.val, DFunLike.coe
-- 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
x : R
y : ↥M
I : Ideal S
h : Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) x : S)
⊢ 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

Premises used: IsLocalization.mk'_spec
-- 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
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
mpr : ∀ (b : S) (hb : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) b = 1), mk' S x y ∈ I
⊢ mk' S x y ∈ I

Tactic:
obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (map_units S y)

Premises used: isUnit_iff_exists_inv, Iff.mp, 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
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
⊢ 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
-- 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
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
mpr₃ mpr₄ mpr₅ mpr₆ : ∀ (this : mk' S x y ∈ I), mk' S x y ∈ I
⊢ mk' S x y ∈ I

Tactic:
rwa [mul_comm, mul_assoc, hb, mul_one] at this

Premises used: mul_assoc, mul_comm, mul_one
-- 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
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)) ⋯
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)
⊢ 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)

Tactic:
use ⟨Z, a'.2 * b'.2⟩
-- 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
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)) ⋯
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)
⊢ 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:
simp only [Z, map_add, Submonoid.coe_mul, map_mul]

Premises used: map_add, map_mul, Submonoid.coe_mul
-- 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
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)) ⋯
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)
⊢ (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:
rw [add_mul, ← mul_assoc a, ha, mul_comm (algebraMap R S a'.2) (algebraMap R S b'.2), ←
      mul_assoc b, hb]

Premises used: add_mul, Algebra.algebraMap, mul_assoc, mul_comm, Subtype.val, Prod.snd, DFunLike.coe
-- 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
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) (β := 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:
ring
-- 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
⊢ HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑(0, 1).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(0, 1).1 : R)

Tactic:
simp
-- 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
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)
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)
⊢ 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

Premises used: IsLocalization.surj
-- 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
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)) ⋯
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)
⊢ 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:
use ⟨Z, c'.2 * x'.2⟩
-- 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
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)) ⋯
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)
⊢ 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:
simp only [Z, ← hx, ← hc, smul_eq_mul, Submonoid.coe_mul, map_mul]

Premises used: map_mul, smul_eq_mul, Submonoid.coe_mul
-- 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
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)) ⋯
⊢ 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:
ring
-- 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
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)
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
⊢ 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
-- 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
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

Tactic:
fun h => Ideal.mem_sInf.1 h fun z hz => ?_

Premises used: Ideal.mem_sInf, Iff.mp
-- 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
z : S
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)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z →
    Membership.mem (γ := Ideal S) (map_ideal M S I) z

Tactic:
refine fun h => Ideal.mem_sInf.1 h fun z hz => ?_
-- 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
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
mp : ∀ (y : R) (hy : y ∈ (↑I : Set R) ∧ (algebraMap R S : (a : R) → S) y = z), z ∈ (↑(map_ideal M S I) : Set S)
⊢ z ∈ (↑(map_ideal M S I) : Set S)

Tactic:
obtain ⟨y, hy⟩ := hz
-- 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
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 ⋯
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)
⊢ z ∈ (↑(map_ideal M S I) : Set S)

Tactic:
use ⟨Z, 1⟩
-- 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
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 ⋯
⊢ 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:
simp [Z, hy.right]

Premises used: And.right
-- 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
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)
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))
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z

Tactic:
rw [← Ideal.unit_mul_mem_iff_mem _ (map_units S s), mul_comm]

Premises used: Ideal.unit_mul_mem_iff_mem, mul_comm, 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
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)
    (HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑s : R) : S))

Tactic:
h.symm ▸ Ideal.mem_map_of_mem _ a.2

Premises used: Ideal.mem_map_of_mem, Set.Mem, Eq.rec, Eq.symm, Subtype.property
-- 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
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)
    (HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑s : R) : S))

Tactic:
exact h.symm ▸ Ideal.mem_map_of_mem _ a.2
-- 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
x : R
s : ↥M
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
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (mk' S x s) ↔ ∃ 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]

Premises used: IsLocalization.mk'_spec', Ideal.unit_mul_mem_iff_mem, IsLocalization.map_units, IsLocalization.mem_map_algebraMap_iff
-- 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
x : R
s : ↥M
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
⊢ (∃ (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:
simp_rw [← map_mul, IsLocalization.eq_iff_exists M, mul_comm x, ← mul_assoc, ← Submonoid.coe_mul]

Premises used: mul_assoc, map_mul, mul_comm, Submonoid.coe_mul, IsLocalization.eq_iff_exists
-- 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
x : R
s_1 : ↥M
h_1 : ∃ s ∈ M, s * x ∈ I
s : R
hs : s ∈ M
h : s * x ∈ I
⊢ (↑(1 * (Subtype.mk (p := fun (x : R) ↦ x ∈ I) (s * x) h, Subtype.mk (p := fun (x : R) ↦ x ∈ M) s hs).2) : R) * x =
    (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) (s * x) h, Subtype.mk (p := fun (x : R) ↦ x ∈ M) s hs).1 : R)

Tactic:
simp