awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := OreLocalization S X) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 r /ₒ HMul.hMul (α := ↥S) 1 1) 0

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
y z : OreLocalization S R
x : OreLocalization S X
c :
  ∀ (r₁ : X) (s₁ : ↥S),
    HSMul.hSMul (β := OreLocalization S X) (y + z) (r₁ /ₒ s₁) =
      HSMul.hSMul (β := OreLocalization S X) y (r₁ /ₒ s₁) + HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)
⊢ (y + z) • x = y • x + z • x

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
y z : OreLocalization S R
r₁ : X
s₁ : ↥S
c :
  ∀ (r₂ : R) (s₂ : ↥S),
    HSMul.hSMul (β := OreLocalization S X) (r₂ /ₒ s₂ + z) (r₁ /ₒ s₁) =
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
        HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)
⊢ HSMul.hSMul (β := OreLocalization S X) (y + z) (r₁ /ₒ s₁) =
    HSMul.hSMul (β := OreLocalization S X) y (r₁ /ₒ s₁) + HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)

Tactic:
induction y 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
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
c :
  ∀ (r₃ : R) (s₃ : ↥S),
    HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
        HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
⊢ HSMul.hSMul (β := OreLocalization S X) (r₂ /ₒ s₂ + z) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)

Tactic:
induction z 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
c :
  ∀ (ra : R) (sa : ↥S) (ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R))
    (q : HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)),
    HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
        HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
⊢ HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)

Tactic:
rcases oreDivAddChar' r₂ r₃ s₂ s₃ with ⟨ra, sa, ha, q⟩

Premises used: OreLocalization.oreDivAddChar'
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
q : HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
⊢ HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)

Tactic:
rw [q]
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)

Tactic:
rw [OreLocalization.expand' r₂ s₂ sa]

Premises used: OreLocalization.expand'
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
c :
  ∀ (rb : R) (sb : ↥S) (hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R))
    (q :
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
        rb • r₁ /ₒ (sb * (sa * s₂))),
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
        HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)

Tactic:
rcases oreDivSMulChar' (sa • r₂) r₁ (sa * s₂) s₁ with ⟨rb, sb, hb, q⟩

Premises used: HMul.hMul, OreLocalization.oreDivSMulChar', HSMul.hSMul
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
q :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂))
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)

Tactic:
rw [q]
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
rw : (↑sb : R) * ((↑sa : R) * (↑s₂ : R)) ∈ S
⊢ (↑sb : R) * ra * (↑s₃ : R) ∈ S

Tactic:
rw [mul_assoc, ← ha]

Premises used: mul_assoc
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
norm_cast : (↑(sb * (sa * s₂)) : R) ∈ S
⊢ (↑sb : R) * ((↑sa : R) * (↑s₂ : R)) ∈ S

Tactic:
norm_cast
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
⊢ (↑(sb * (sa * s₂)) : R) ∈ S

Tactic:
apply SetLike.coe_mem

Premises used: SetLike.coe_mem
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
⊢ (↑sb : R) * ra * (↑s₃ : R) ∈ S

Tactic:
have hs₃rasb : sb * ra * s₃ ∈ S := by
    rw [mul_assoc, ← ha]
    norm_cast
    apply SetLike.coe_mem
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
        (((↑sb : R) * ra) • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sb : R) * ra * (↑s₃ : R)) hs₃rasb) (r₁ /ₒ s₁)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)

Tactic:
rw [OreLocalization.expand _ _ _ hs₃rasb]

Premises used: OreLocalization.expand
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
⊢ (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)

Tactic:
simp [ha, mul_assoc]

Premises used: mul_assoc
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
⊢ (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)

Tactic:
have ha' : ↑((sb * sa) * s₂) = sb * ra * s₃ := by simp [ha, mul_assoc]
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
        (r₁ /ₒ s₁)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
        (((↑sb : R) * ra) • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sb : R) * ra * (↑s₃ : R)) hs₃rasb) (r₁ /ₒ s₁)

Tactic:
rw [← Subtype.coe_eq_of_eq_mk ha']

Premises used: Subtype.coe_eq_of_eq_mk
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
c :
  ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R))
    (hc' :
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
          (r₁ /ₒ s₁) =
        rc • r₁ /ₒ (sc * (sb * sa * s₂))),
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
      rb • r₁ /ₒ (sb * (sa * s₂)) +
        HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
          (r₁ /ₒ s₁)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
        (r₁ /ₒ s₁)

Tactic:
rcases oreDivSMulChar' ((sb * ra) • r₃) r₁ (sb * sa * s₂) s₁ with ⟨rc, sc, hc, hc'⟩

Premises used: HMul.hMul, OreLocalization.oreDivSMulChar', HSMul.hSMul, Subtype.val
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HAdd.hAdd (α := OreLocalization S X) (rb • r₁ /ₒ (sb * (sa * s₂))) (rc • r₁ /ₒ (sc * (sb * sa * s₂)))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
        (r₁ /ₒ s₁)

Tactic:
rw [hc']
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ (↑sc : R) * (↑(sb * (sa * s₂)) : R) = 1 * (↑(sc * (sb * sa * s₂)) : R)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HAdd.hAdd (α := OreLocalization S X) (rb • r₁ /ₒ (sb * (sa * s₂))) (rc • r₁ /ₒ (sc * (sb * sa * s₂)))

Tactic:
rw [oreDiv_add_char _ _ 1 sc (by simp [mul_assoc])]

Premises used: OreLocalization.oreDiv_add_char, OfNat.ofNat
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
    (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
rw [OreLocalization.expand' (sa • r₂ + ra • r₃) (sa * s₂) (sc * sb)]

Premises used: HMul.hMul, OreLocalization.expand', HAdd.hAdd, HSMul.hSMul
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      (((↑sc : R) * (↑sb : R) * ((↑sa : R) * r₂) + (↑sc : R) * (↑sb : R) * (ra * r₃)) /ₒ (sc * sb * (sa * s₂)))
      (r₁ /ₒ s₁) =
    ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
    (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
simp only [smul_eq_mul, one_smul, Submonoid.smul_def, mul_add, Submonoid.coe_mul] at hb hc ⊢

Premises used: one_smul, Submonoid.smul_def, mul_add, smul_eq_mul, Submonoid.coe_mul
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * ((↑sa : R) * r₂) = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra * r₃) = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      (((↑sc : R) * rb + rc) * (↑s₁ : R) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
    ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      (((↑sc : R) * (↑sb : R) * ((↑sa : R) * r₂) + (↑sc : R) * (↑sb : R) * (ra * r₃)) /ₒ (sc * sb * (sa * s₂)))
      (r₁ /ₒ s₁) =
    ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
rw [mul_assoc, hb, mul_assoc, ← mul_assoc _ ra, hc, ← mul_assoc, ← add_mul]

Premises used: add_mul, mul_assoc
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * ((↑sa : R) * r₂) = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra * r₃) = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
c :
  Eq (α := OreLocalization S X) (((↑sc : R) * rb + rc) • r₁ /ₒ (sc * sb * (sa * s₂)))
    (((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂))))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      (((↑sc : R) * rb + rc) * (↑s₁ : R) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
    ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
rw [OreLocalization.smul_cancel']

Premises used: OreLocalization.smul_cancel'
-- 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
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * ((↑sa : R) * r₂) = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra * r₃) = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ Eq (α := OreLocalization S X) (((↑sc : R) * rb + rc) • r₁ /ₒ (sc * sb * (sa * s₂)))
    (((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂))))

Tactic:
simp only [add_smul, ← mul_assoc, smul_smul]

Premises used: mul_assoc, smul_smul, add_smul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
x y z : OreLocalization S R
⊢ x * (y + z) = x * y + x * z

Tactic:
OreLocalization.smul_add _ _ _

Premises used: OreLocalization.smul_add
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
x y z : OreLocalization S R
⊢ (x + y) * z = x * z + y * z

Tactic:
OreLocalization.add_smul _ _ _

Premises used: OreLocalization.add_smul