awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddGroup X
inst_3 : DistribMulAction R X
r : X
t : R
s : ↥S
ht : t * (↑s : R) ∈ S
rw : Eq (α := OreLocalization S X) (-r /ₒ s) (t • -r /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
rw₁ rw₂ : Eq (α := OreLocalization S X) (-r /ₒ s) (-r /ₒ s)
⊢ Eq (α := OreLocalization S X) (-r /ₒ s) (-(t • r) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)

Tactic:
rw [← smul_neg, ← OreLocalization.expand]

Premises used: OreLocalization.expand, smul_neg
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddGroup X
inst_3 : DistribMulAction R X
r : X
s : ↥S
⊢ Eq (α := OreLocalization S X) (-(r /ₒ s)) (-r /ₒ s)

Tactic:
rfl
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddGroup X
inst_3 : DistribMulAction R X
r : X
s : ↥S
⊢ Eq (α := OreLocalization S X) (-(r /ₒ s)) (-r /ₒ s)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddGroup X
inst_3 : DistribMulAction R X
x : OreLocalization S X
c : ∀ (r : X) (s : ↥S), HAdd.hAdd (α := OreLocalization S X) (-(r /ₒ s)) (r /ₒ s) = 0
⊢ -x + x = 0

Tactic:
induction x with | _ r s
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddGroup X
inst_3 : DistribMulAction R X
r : X
s : ↥S
⊢ HAdd.hAdd (α := OreLocalization S X) (-(r /ₒ s)) (r /ₒ s) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.OreLocalization.Cardinality
Goal:
R : Type u
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
⊢ #(OreLocalization S R) = #R

Tactic:
le_antisymm (cardinalMk_le S) (mk_le_of_injective (numeratorHom_inj hS))

Premises used: OreLocalization.numeratorHom_inj, le_antisymm, Cardinal.mk_le_of_injective, OreLocalization.cardinalMk_le
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
hS : S ≤ nonZeroDivisorsLeft R
⊢ Nontrivial.{u_1} (OreLocalization S R)

Tactic:
nontrivial_iff.mpr (fun e ↦ one_ne_zero <| hS e 1 (zero_mul _))

Premises used: Iff.mpr, MulZeroClass.zero_mul, one_ne_zero, OfNat.ofNat, OreLocalization.nontrivial_iff
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
hS : S ≤ nonZeroDivisorsRight R
⊢ Nontrivial.{u_1} (OreLocalization S R)

Tactic:
nontrivial_iff.mpr (fun e ↦ one_ne_zero <| hS e 1 (mul_zero _))

Premises used: Iff.mpr, MulZeroClass.mul_zero, one_ne_zero, OfNat.ofNat, OreLocalization.nontrivial_iff
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
hS : S ≤ R⁰
⊢ Nontrivial.{u_1} (OreLocalization S R)

Tactic:
nontrivial_of_nonZeroDivisorsLeft (hS.trans inf_le_left)

Premises used: inf_le_left, LE.le.trans, OreLocalization.nontrivial_of_nonZeroDivisorsLeft
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
⊢ Nontrivial.{u_1} (OreLocalization R⁰ R)

Tactic:
nontrivial_of_nonZeroDivisors (refl R⁰)

Premises used: nonZeroDivisors, refl, OreLocalization.nontrivial_of_nonZeroDivisors
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
pos :
  ∀ (hr : r = 0),
    Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        r s)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))
neg :
  ∀ (hr : ¬r = 0),
    Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        r s)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))
⊢ Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      r s)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
hr : r = 0
⊢ Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      r s)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))

Tactic:
simp [hr]
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
hr : ¬r = 0
pos :
  ∀ (ht : t = 0),
    Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        r s)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))
neg :
  ∀ (ht : ¬t = 0),
    Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        r s)
      ((fun (r : R) (s : ↥R⁰) ↦
          (if hr : r = 0 then 0
            else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
            OreLocalization R⁰ R))
        (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))
⊢ Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      r s)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))

Tactic:
by_cases ht : t = 0
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
hr : ¬r = 0
ht : t = 0
pos : False
⊢ Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      r s)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))

Tactic:
exfalso
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
hr : ¬r = 0
ht : t = 0
pos : (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst) : R) = 0
⊢ False

Tactic:
apply nonZeroDivisors.coe_ne_zero ⟨_, hst⟩

Premises used: Subtype.mk, nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
hr : ¬r = 0
ht : t = 0
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst) : R) = 0

Tactic:
simp [ht]
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
hr : ¬r = 0
ht : ¬t = 0
neg :
  Eq (α := OreLocalization R⁰ R)
    ((↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯)
    (t * (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * r) ⋯)
⊢ Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      r s)
    ((fun (r : R) (s : ↥R⁰) ↦
        (if hr : r = 0 then 0
          else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯ :
          OreLocalization R⁰ R))
      (t • r) (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst))

Tactic:
simp only [hr, ht, dif_neg, not_false_iff, or_self_iff, mul_eq_zero, smul_eq_mul]

Premises used: or_self_iff, mul_eq_zero, dif_neg, smul_eq_mul, not_false_iff
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Nontrivial R
inst_3 : OreSet R⁰
inst_4 : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : Membership.mem (γ := Submonoid R) R⁰ (t * (↑s : R))
hr : ¬r = 0
ht : ¬t = 0
⊢ Eq (α := OreLocalization R⁰ R)
    ((↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯)
    (t * (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * r) ⋯)

Tactic:
apply OreLocalization.expand

Premises used: OreLocalization.expand
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
r : R
s : ↥R⁰
⊢ Eq (α := OreLocalization R⁰ R) (r /ₒ s)⁻¹
    (if hr : r = 0 then 0 else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯)

Tactic:
rfl
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
r : R
s : ↥R⁰
⊢ Eq (α := OreLocalization R⁰ R) (r /ₒ s)⁻¹
    (if hr : r = 0 then 0 else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
x : OreLocalization R⁰ R
h : x ≠ 0
c :
  ∀ (r : R) (s : ↥R⁰) (h : Ne (α := OreLocalization R⁰ R) (r /ₒ s) 0),
    HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s) (r /ₒ s)⁻¹ = 1
⊢ x * x⁻¹ = 1

Tactic:
induction x with | _ r s
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
r : R
s : ↥R⁰
h : Ne (α := OreLocalization R⁰ R) (r /ₒ s) 0
c :
  HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s)
      (if hr : r = 0 then 0
      else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯) =
    1 /ₒ 1
⊢ HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s) (r /ₒ s)⁻¹ = 1

Tactic:
rw [OreLocalization.inv_def, OreLocalization.one_def]

Premises used: OreLocalization.one_def, OreLocalization.inv_def
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
s : ↥R⁰
h : Ne (α := OreLocalization R⁰ R) (0 /ₒ s) 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
r : R
s : ↥R⁰
h : Ne (α := OreLocalization R⁰ R) (r /ₒ s) 0
⊢ r ≠ 0

Tactic:
have hr : r ≠ 0 := by
    rintro rfl
    simp at h
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
r : R
s : ↥R⁰
h : Ne (α := OreLocalization R⁰ R) (r /ₒ s) 0
hr : r ≠ 0
c :
  HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s)
      (if h : False then 0
      else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯) =
    1 /ₒ 1
⊢ HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s)
      (if hr : r = 0 then 0
      else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯) =
    1 /ₒ 1

Tactic:
simp only [hr]
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
r : R
s : ↥R⁰
h : Ne (α := OreLocalization R⁰ R) (r /ₒ s) 0
hr : r ≠ 0
⊢ HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s)
      (if h : False then 0
      else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯) =
    1 /ₒ 1

Tactic:
apply OreLocalization.mul_inv ⟨r, _⟩

Premises used: Subtype.mk, OreLocalization.mul_inv
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
r : R
s : ↥R⁰
h : Ne (α := OreLocalization R⁰ R) (r /ₒ s) 0
hr : r ≠ 0
⊢ HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s)
      (if h : False then 0
      else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯) =
    1 /ₒ 1

Tactic:
with_unfolding_all apply OreLocalization.mul_inv ⟨r, _⟩

Premises used: Subtype.mk, OreLocalization.mul_inv
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
rw :
  Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
    (if hr : Eq.{u_1 + 1} (α := R) 0 0 then 0
    else (↑1 : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) 0 ⋯)
    (0 /ₒ 1)
⊢ Eq.{u_1 + 1} (α := OreLocalization R⁰ R) 0⁻¹ 0

Tactic:
rw [OreLocalization.zero_def, OreLocalization.inv_def]

Premises used: OreLocalization.zero_def, OreLocalization.inv_def
-- Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
inst_2 : OreSet R⁰
inst_3 : NoZeroDivisors R
⊢ Eq.{u_1 + 1} (α := OreLocalization R⁰ R)
    (if hr : Eq.{u_1 + 1} (α := R) 0 0 then 0
    else (↑1 : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) 0 ⋯)
    (0 /ₒ 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
mp :
  Nonempty.{u_1 + 1} (OreSet S) →
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
mpr :
  ((∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)) →
    Nonempty.{u_1 + 1} (OreSet S)
⊢ Nonempty.{u_1 + 1} (OreSet S) ↔
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
⊢ Nonempty.{u_1 + 1} (OreSet S) →
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)

Tactic:
fun ⟨_⟩ ↦ ⟨ore_right_cancel, fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩⟩

Premises used: OreLocalization.oreNum, OreLocalization.ore_eq, And, OreLocalization.ore_right_cancel, _private.0.OreLocalization.nonempty_oreSet_iff.match_1, And.intro, Exists.intro, OreLocalization.oreDenom
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
⊢ Nonempty.{u_1 + 1} (OreSet S) →
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)

Tactic:
exact fun ⟨_⟩ ↦ ⟨ore_right_cancel, fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩⟩
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂
H' : ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
mpr :
  ∀ (r' : (r : R) → (s : ↥S) → R) (s' : (r : R) → (s : ↥S) → ↥S)
    (h : ∀ (r : R) (s : ↥S), (↑(s' r s) : R) * r = r' r s * (↑s : R)), Nonempty.{u_1 + 1} (OreSet S)
⊢ Nonempty.{u_1 + 1} (OreSet S)

Tactic:
choose r' s' h using H'
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂
r' : (r : R) → (s : ↥S) → R
s' : (r : R) → (s : ↥S) → ↥S
h : ∀ (r : R) (s : ↥S), (↑(s' r s) : R) * r = r' r s * (↑s : R)
⊢ Nonempty.{u_1 + 1} (OreSet S)

Tactic:
⟨H, r', s', h⟩

Premises used: Nonempty.intro, OreLocalization.OreSet.mk
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * (↑s : R) = r₂ * (↑s : R) → ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂
r' : (r : R) → (s : ↥S) → R
s' : (r : R) → (s : ↥S) → ↥S
h : ∀ (r : R) (s : ↥S), (↑(s' r s) : R) * r = r' r s * (↑s : R)
⊢ Nonempty.{u_1 + 1} (OreSet S)

Tactic:
exact ⟨H, r', s', h⟩
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
mp : Nonempty.{u_1 + 1} (OreSet S) → ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
mpr : (∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)) → Nonempty.{u_1 + 1} (OreSet S)
⊢ Nonempty.{u_1 + 1} (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty.{u_1 + 1} (OreSet S) → ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)

Tactic:
fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩

Premises used: _private.0.OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors.match_1, OreLocalization.oreNum, OreLocalization.ore_eq, Exists.intro, OreLocalization.oreDenom
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty.{u_1 + 1} (OreSet S) → ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)

Tactic:
exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
H : ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
mpr :
  ∀ (r' : (r : R) → (s : ↥S) → R) (s' : (r : R) → (s : ↥S) → ↥S)
    (h : ∀ (r : R) (s : ↥S), (↑(s' r s) : R) * r = r' r s * (↑s : R)), Nonempty.{u_1 + 1} (OreSet S)
⊢ Nonempty.{u_1 + 1} (OreSet S)

Tactic:
choose r' s' h using H
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
r' : (r : R) → (s : ↥S) → R
s' : (r : R) → (s : ↥S) → ↥S
h : ∀ (r : R) (s : ↥S), (↑(s' r s) : R) * r = r' r s * (↑s : R)
⊢ Nonempty.{u_1 + 1} (OreSet S)

Tactic:
⟨oreSetOfNoZeroDivisors r' s' h⟩

Premises used: Nonempty.intro, OreLocalization.oreSetOfNoZeroDivisors
-- Module: Mathlib.RingTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
r' : (r : R) → (s : ↥S) → R
s' : (r : R) → (s : ↥S) → ↥S
h : ∀ (r : R) (s : ↥S), (↑(s' r s) : R) * r = r' r s * (↑s : R)
⊢ Nonempty.{u_1 + 1} (OreSet S)

Tactic:
exact ⟨oreSetOfNoZeroDivisors r' s' h⟩
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
x : OreLocalization S X
c : ∀ (r : X) (s : ↥S), HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) 0 (r /ₒ s) = 0
⊢ HSMul.hSMul (α := OreLocalization S R) 0 x = 0

Tactic:
induction x with | _ r s
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r : X
s : ↥S
⊢ HMul.hMul (α := R) (↑1 : R) 0 = 0 * (↑s : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r : X
s : ↥S
c : Eq (α := OreLocalization S X) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 r /ₒ HMul.hMul (α := ↥S) 1 1) 0
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) 0 (r /ₒ s) = 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_smul_char 0 r 1 s 0 1 (by simp)]

Premises used: OreLocalization.zero_def, OreLocalization.oreDiv_smul_char, OfNat.ofNat