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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rcases :
  ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * sb = rc * (↑sa : R)),
    ∃ (u : ↥S),
      ∃ (v : R),
        u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
          (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)

Tactic:
rcases oreCondition sb sa with ⟨rc, sc, hc⟩

Premises used: OreLocalization.oreCondition
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
rw₁ : (↑sc : R) * rb * (↑s₂ : R) = rc * ((↑sa : R) * (↑s₁ : R))
rw₂ : (↑sc : R) * rb * (↑s₂ : R) = rc * (↑sa : R) * (↑s₁ : R)
rw₃ : (↑sc : R) * rb * (↑s₂ : R) = (↑sc : R) * sb * (↑s₁ : R)
rw₄ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * sb * (↑s₁ : R)
rw₅ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * (sb * (↑s₁ : R))
rw₆ rw₇ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * (rb * (↑s₂ : R))
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)

Tactic:
rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]

Premises used: mul_assoc
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)

Tactic:
have : sc * rb * s₂ = rc * ra * s₂ := by
    rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
rcases :
  ∀ (sd : ↥S) (hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)),
    ∃ (u : ↥S),
      ∃ (v : R),
        u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
          (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)

Tactic:
rcases ore_right_cancel _ _ s₂ this with ⟨sd, hd⟩

Premises used: OreLocalization.ore_right_cancel
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ∃ (v : R),
    (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
      (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)

Tactic:
use sd * sc
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  (sd * sc) • (sb • r₁ + rb • r₂) = ((↑sd : R) * rc) • (sa • r₁ + ra • r₂) ∧
    (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) =
      (↑sd : R) * rc * (↑(sa * s₁) : R)
⊢ ∃ (v : R),
    (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
      (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)

Tactic:
use sd * rc
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
      ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂ ∧
    (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
⊢ (sd * sc) • (sb • r₁ + rb • r₂) = ((↑sd : R) * rc) • (sa • r₁ + ra • r₂) ∧
    (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) =
      (↑sd : R) * rc * (↑(sa * s₁) : R)

Tactic:
simp only [smul_add, smul_smul, Submonoid.smul_def, Submonoid.coe_mul]

Premises used: smul_smul, Submonoid.smul_def, smul_add, Submonoid.coe_mul
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₂ : (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
      ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂ ∧
    (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))

Tactic:
constructor
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * ((↑sc : R) * rb)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₂ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₃ :
  ((↑sd : R) * ((↑sc : R) * sb)) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₄ :
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₅ :
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₆ h₇ :
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂

Tactic:
rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]

Premises used: mul_assoc
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ : (↑sd : R) * ((↑sc : R) * (sb * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₂ : (↑sd : R) * ((↑sc : R) * sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₃ : (↑sd : R) * (rc * (↑sa : R) * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₄ : (↑sd : R) * (rc * ((↑sa : R) * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₅ h₆ : (↑sd : R) * (rc * ((↑sa : R) * (↑s₁ : R))) = (↑sd : R) * (rc * ((↑sa : R) * (↑s₁ : R)))
⊢ (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))

Tactic:
rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]

Premises used: mul_assoc, Subtype.val
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • (r₁, s₁).fst = rb • (r₁', s₁').fst
hb' : (↑sb : R) * (↑(r₁, s₁).snd : R) = rb * (↑(r₁', s₁').snd : R)
rcases :
  ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)),
    Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)
⊢ Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)

Tactic:
rcases oreCondition (s₁' : R) s₂ with ⟨rc, sc, hc⟩

Premises used: OreLocalization.oreCondition, Subtype.val
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • (r₁, s₁).fst = rb • (r₁', s₁').fst
hb' : (↑sb : R) * (↑(r₁, s₁).snd : R) = rb * (↑(r₁', s₁').snd : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rcases :
  ∀ (rd : R) (sd : ↥S) (hd : (↑sd : R) * rb = rd * (↑sc : R)),
    Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)
⊢ Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)

Tactic:
rcases oreCondition rb sc with ⟨rd, sd, hd⟩

Premises used: OreLocalization.oreCondition
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • (r₁, s₁).fst = rb • (r₁', s₁').fst
hb' : (↑sb : R) * (↑(r₁, s₁).snd : R) = rb * (↑(r₁', s₁').snd : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
dsimp : Eq (α := OreLocalization S X) (add'' r₁' s₁' r₂ s₂) (add'' r₁ s₁ r₂ s₂)
⊢ Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)

Tactic:
dsimp at *
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw :
  Eq (α := OreLocalization S X)
    (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯)
    (add'' r₁ s₁ r₂ s₂)
⊢ Eq (α := OreLocalization S X) (add'' r₁' s₁' r₂ s₂) (add'' r₁ s₁ r₂ s₂)

Tactic:
rw [add''_char _ _ _ _ rc sc hc (sc * s₁').2]

Premises used: HMul.hMul, _private.0.OreLocalization.add''_char, Subtype.val, Subtype.property
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
rw₁ : (↑sd : R) * (rb * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
rw₂ : (↑sd : R) * rb * (↑s₁' : R) = rd * rc * (↑s₂ : R)
rw₃ : rd * (↑sc : R) * (↑s₁' : R) = rd * rc * (↑s₂ : R)
rw₄ : rd * ((↑sc : R) * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
rw₅ : rd * (rc * (↑s₂ : R)) = rd * rc * (↑s₂ : R)
rw₆ rw₇ : rd * rc * (↑s₂ : R) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)

Tactic:
rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]

Premises used: mul_assoc
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)

Tactic:
have : sd * sb * s₁ = rd * rc * s₂ := by
      rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
rw :
  Eq (α := OreLocalization S X)
    (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯)
    ((((↑sd : R) * (↑sb : R)) • r₁ + (rd * rc) • r₂) /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯)
⊢ Eq (α := OreLocalization S X)
    (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯)
    (add'' r₁ s₁ r₂ s₂)

Tactic:
rw [add''_char _ _ _ _ (rd * rc : R) (sd * sb) this (sd * sb * s₁).2]

Premises used: HMul.hMul, _private.0.OreLocalization.add''_char, Subtype.val, Subtype.property
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
rw :
  ∃ (u : ↥S),
    ∃ (v : R),
      u • ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = v • ((↑sc : R) • r₁' + rc • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
          v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)
⊢ Eq (α := OreLocalization S X)
    (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯)
    ((((↑sd : R) * (↑sb : R)) • r₁ + (rd * rc) • r₂) /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯)

Tactic:
rw [mul_smul, ← Submonoid.smul_def sb, hb, smul_smul, hd, oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff, smul_smul, Submonoid.smul_def, SemigroupAction.mul_smul
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
h :
  ∃ (v : R),
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) =
        v • ((↑sc : R) • r₁' + rc • r₂) ∧
      (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
        v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = v • ((↑sc : R) • r₁' + rc • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
          v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)

Tactic:
use 1
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
h :
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = rd • ((↑sc : R) • r₁' + rc • r₂) ∧
    (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
      rd * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)
⊢ ∃ (v : R),
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) =
        v • ((↑sc : R) • r₁' + rc • r₂) ∧
      (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
        v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)

Tactic:
use rd
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
h : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * ((↑sc : R) * (↑s₁' : R))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = rd • ((↑sc : R) • r₁' + rc • r₂) ∧
    (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
      rd * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)

Tactic:
simp only [mul_smul, smul_add, one_smul, OneMemClass.coe_one, one_mul, true_and]

Premises used: OneMemClass.coe_one, one_smul, SemigroupAction.mul_smul, smul_add, one_mul, true_and
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
h : rd * rc * (↑s₂ : R) = rd * ((↑sc : R) * (↑s₁' : R))
h₁ : rd * rc * (↑s₂ : R) = rd * (rc * (↑s₂ : R))
h₂ h₃ : rd * (rc * (↑s₂ : R)) = rd * (rc * (↑s₂ : R))
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * ((↑sc : R) * (↑s₁' : R))

Tactic:
rw [this, hc, mul_assoc]

Premises used: mul_assoc
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
x : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : (↑sb : R) * (↑(r₂, s₂).snd : R) = rb * (↑(r₁, s₁).snd : R)
c :
  ∀ (r₃ : X) (s₃ : ↥S),
    Eq (α := OreLocalization S X)
      ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ (add' rs.fst rs.snd (r₃ /ₒ s₃) : OreLocalization S X)) (r₁, s₁))
      ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ (add' rs.fst rs.snd (r₃ /ₒ s₃) : OreLocalization S X)) (r₂, s₂))
⊢ Eq (α := OreLocalization S X) ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ add' rs.fst rs.snd x) (r₁, s₁))
    ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ add' rs.fst rs.snd x) (r₂, s₂))

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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : (↑sb : R) * (↑(r₂, s₂).snd : R) = rb * (↑(r₁, s₁).snd : R)
r₃ : X
s₃ : ↥S
c : Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
⊢ Eq (α := OreLocalization S X) (add'' (r₃, s₃).fst (r₃, s₃).snd (r₁, s₁).fst (r₁, s₁).snd)
    (add'' (r₃, s₃).fst (r₃, s₃).snd (r₂, s₂).fst (r₂, s₂).snd)

Tactic:
dsimp only at *
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
c :
  ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)),
    Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)

Tactic:
rcases oreCondition (s₃ : R) s₂ with ⟨rc, sc, hc⟩

Premises used: OreLocalization.oreCondition, Subtype.val
-- 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 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
c :
  ∀ (rd : R) (sd : ↥S) (hd : (↑sd : R) * rc = rd * (↑sb : R)),
    Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)

Tactic:
rcases oreCondition rc sb with ⟨rd, sd, hd⟩

Premises used: OreLocalization.oreCondition