awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (ra • r₂ /ₒ (sa * s₁))
have c : oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (ra • r₂ /ₒ (sa * s₁))
Tactic: rw [oreDiv_smul_oreDiv]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (ra • r₂ /ₒ (sa * s₁))
have c : oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
  oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (ra • r₂ /ₒ (sa * s₁))
Tactic: rw [oreDiv_smul_oreDiv]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (ra • r₂ /ₒ (sa * s₁))
have c : oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
  HAdd.hAdd (α := OreLocalization S X) (oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃))
    (oreNum r₃ (sa * s₁) • ra • r₂ /ₒ (oreDenom r₃ (sa * s₁) * s₃))
Tactic: rw [oreDiv_smul_oreDiv]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (ra • r₂ /ₒ (sa * s₁))
have c : oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
  HAdd.hAdd (α := OreLocalization S X) (oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃))
    (oreNum r₃ (sa * s₁) • ra • r₂ /ₒ (oreDenom r₃ (sa * s₁) * s₃))
Tactic: repeat rw [oreDiv_smul_oreDiv]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
R₀ : Type u_3
inst_4 : Monoid R₀
inst_5 : MulAction R₀ X
inst_6 : MulAction R₀ R
inst_7 : IsScalarTower R₀ R X
inst_8 : IsScalarTower R₀ R R
x : R₀
⊢ HSMul.hSMul (β := OreLocalization S X) x 0 = 0
have rw : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (HSMul.hSMul (β := R) x 1 /ₒ 1) 0 = 0
Tactic: rw [← smul_one_oreDiv_one_smul, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
R₀ : Type u_3
inst_4 : Monoid R₀
inst_5 : MulAction R₀ X
inst_6 : MulAction R₀ R
inst_7 : IsScalarTower R₀ R X
inst_8 : IsScalarTower R₀ R R
x : R₀
rw : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (HSMul.hSMul (β := R) x 1 /ₒ 1) 0 = 0
⊢ HSMul.hSMul (β := OreLocalization S X) x 0 = 0
have rw₁ : Eq (α := OreLocalization S X) 0 0
Tactic: rw [← smul_one_oreDiv_one_smul, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : DistribMulAction R X
x y : OreLocalization S X
⊢ x + y = y + x
have c : ∀ (r : X) (s : ↥S), r /ₒ s + y = y + r /ₒ s
Tactic: induction x with | _ r s
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : DistribMulAction R X
y : OreLocalization S X
r : X
s : ↥S
⊢ r /ₒ s + y = y + r /ₒ s
have c : ∀ (r' : X) (s' : ↥S),
  HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = HAdd.hAdd (α := OreLocalization S X) (r' /ₒ s') (r /ₒ s)
Tactic: induction y with | _ r' s'
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = HAdd.hAdd (α := OreLocalization S X) (r' /ₒ s') (r /ₒ s)
have c : ∀ (ra : R) (sa : ↥S) (ha : (↑sa : R) * (↑s : R) = ra * (↑s' : R))
  (ha' : HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = (sa • r + ra • r') /ₒ (sa * s)),
  HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = HAdd.hAdd (α := OreLocalization S X) (r' /ₒ s') (r /ₒ s)
Tactic: rcases oreDivAddChar' r r' s s' with ⟨ra, sa, ha, ha'⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s : R) = ra * (↑s' : R)
ha' : HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = (sa • r + ra • r') /ₒ (sa * s)
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = HAdd.hAdd (α := OreLocalization S X) (r' /ₒ s') (r /ₒ s)
have c : Eq (α := OreLocalization S X) ((ra • r' + sa • r) /ₒ (sa * s))
  ((ra • r' + (↑sa : R) • r) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) sorry)
Tactic: rw [ha', oreDiv_add_char' s' s _ _ ha.symm (ha ▸ (sa * s).2), add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s : R) = ra * (↑s' : R)
ha' : HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = (sa • r + ra • r') /ₒ (sa * s)
⊢ Eq (α := OreLocalization S X) ((ra • r' + sa • r) /ₒ (sa * s))
    ((ra • r' + (↑sa : R) • r) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) ⋯)
have c : sa * s = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s : R) = ra * (↑s' : R)
ha' : HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = (sa • r + ra • r') /ₒ (sa * s)
⊢ sa * s = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) ⋯
have c : (↑(sa * s) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) sorry) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
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
⊢ Eq (α := OreLocalization S X) (-r /ₒ s) (-(t • r) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
have rw : 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]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
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)
⊢ Eq (α := OreLocalization S X) (-r /ₒ s) (-(t • r) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
have rw₁ : Eq (α := OreLocalization S X) (-r /ₒ s) (-r /ₒ s)
Tactic: rw [← smul_neg, ← OreLocalization.expand]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
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
⊢ -x + x = 0
have c : ∀ (r : X) (s : ↥S), HAdd.hAdd (α := OreLocalization S X) (-(r /ₒ s)) (r /ₒ s) = 0
Tactic: induction x with | _ r s
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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))
⊢ 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))
have 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 sorry :
          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 sorry :
          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
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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))
⊢ 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))
have 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 sorry :
          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 sorry :
          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
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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))
have 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 sorry :
          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 sorry :
          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
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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))
⊢ 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))
have 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 sorry :
          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 sorry :
          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
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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.{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))
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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
⊢ False
have pos : (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * (↑s : R)) hst) : R) = 0
Tactic: apply nonZeroDivisors.coe_ne_zero ⟨_, hst⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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.{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))
have neg : Eq (α := OreLocalization R⁰ R) ((↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r sorry)
  (t * (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) (t * r) sorry)
Tactic: simp only [hr, ht, dif_neg, not_false_iff, or_self_iff, mul_eq_zero, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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
⊢ x * x⁻¹ = 1
have c : ∀ (r : R) (s : ↥R⁰) (h : Ne (α := OreLocalization R⁰ R) (r /ₒ s) 0),
  HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s) (r /ₒ s)⁻¹ = 1
Tactic: induction x with | _ r s
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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
⊢ HMul.hMul (α := OreLocalization R⁰ R) (r /ₒ s) (r /ₒ s)⁻¹ = 1
have 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 sorry) =
  1 /ₒ 1
Tactic: rw [OreLocalization.inv_def, OreLocalization.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (hypothesis)
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
⊢ 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
have hr : r ≠ 0
Tactic: have hr : r ≠ 0 := by
    rintro rfl
    simp at h
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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 hr : r = 0 then 0
      else (↑s : R) /ₒ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r ⋯) =
    1 /ₒ 1
have 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 sorry) =
  1 /ₒ 1
Tactic: simp only [hr]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.NonZeroDivisors (goal)
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) 0⁻¹ 0
have 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 sorry)
  (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, OreLocalization.inv_def]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.OreSet (goal)
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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.OreSet (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.OreSet (goal)
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)
⊢ Nonempty.{u_1 + 1} (OreSet S)
have 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)
Tactic: choose r' s' h using H'
Cleared hypotheses: H'