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
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ (↑(sc * (sa * s₁)) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) ⋯) : R)

Tactic:
hc
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ (↑(sc * (sa * s₁)) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) ⋯) : R)

Tactic:
exact hc
-- 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
s : ↥S
rw : ∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := X) u 0 = HSMul.hSMul (β := X) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑s : R)
⊢ Eq (α := OreLocalization S X) (0 /ₒ s) 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff, OreLocalization.zero_def
-- 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
s : ↥S
⊢ HSMul.hSMul (β := X) s 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := X) 1 0 ∧ (↑s : R) * (↑1 : R) = 1 * (↑s : R)

Tactic:
simp
-- 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
s : ↥S
⊢ ∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := X) u 0 = HSMul.hSMul (β := X) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑s : R)

Tactic:
exact ⟨s, 1, by simp⟩
-- 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
c : ∀ (r : X) (s : ↥S), HAdd.hAdd (α := OreLocalization S X) 0 (r /ₒ s) = r /ₒ s
⊢ 0 + x = x

Tactic:
induction x
-- 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
c : Eq (α := OreLocalization S X) ((0 + r) /ₒ s) (r /ₒ s)
⊢ HAdd.hAdd (α := OreLocalization S X) 0 (r /ₒ s) = r /ₒ s

Tactic:
rw [← zero_oreDiv, add_oreDiv]

Premises used: OreLocalization.zero_oreDiv, OreLocalization.add_oreDiv
-- 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
⊢ Eq (α := OreLocalization S X) ((0 + r) /ₒ s) (r /ₒ s)

Tactic:
simp
-- 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
c : ∀ (r : X) (s : ↥S), HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) 0 = r /ₒ s
⊢ x + 0 = x

Tactic:
induction x
-- 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
c : Eq (α := OreLocalization S X) ((r + 0) /ₒ s) (r /ₒ s)
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) 0 = r /ₒ s

Tactic:
rw [← zero_oreDiv, add_oreDiv]

Premises used: OreLocalization.zero_oreDiv, OreLocalization.add_oreDiv
-- 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
⊢ Eq (α := OreLocalization S X) ((r + 0) /ₒ s) (r /ₒ s)

Tactic:
simp
-- 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
⊢ nsmul 0 x = 0

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 : AddMonoid X
inst_3 : DistribMulAction R X
x : OreLocalization S X
⊢ nsmul 0 x = 0

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 : AddMonoid X
inst_3 : DistribMulAction R X
x : ℕ
x_1 : OreLocalization S X
⊢ nsmul (x + 1) x_1 = nsmul x x_1 + x_1

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 : AddMonoid X
inst_3 : DistribMulAction R X
x : ℕ
x_1 : OreLocalization S X
⊢ nsmul (x + 1) x_1 = nsmul x x_1 + x_1

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 : AddMonoid X
inst_3 : DistribMulAction R X
x : OreLocalization S R
c : ∀ (r : R) (s : ↥S), HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0
⊢ HSMul.hSMul (β := OreLocalization S X) x 0 = 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 : AddMonoid X
inst_3 : DistribMulAction R X
r : R
s : ↥S
c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := X) r 0 /ₒ s) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S X) (0 /ₒ s) (0 /ₒ 1)
c₃ : Eq (α := OreLocalization S X) 0 (0 /ₒ 1)
c₄ c₅ : Eq (α := OreLocalization S X) 0 0
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0

Tactic:
rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]

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

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

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

Tactic:
induction z 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₂ : ↥S
r₃ : R
s₃ : ↥S
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₁)),
    HSMul.hSMul (α := OreLocalization S R) (r₃ /ₒ s₃) (HAdd.hAdd (α := OreLocalization S X) (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 R) (r₃ /ₒ s₃) (HAdd.hAdd (α := OreLocalization S X) (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, ha'⟩

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

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

Tactic:
apply SetLike.coe_mem

Premises used: SetLike.coe_mem
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
c :
  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₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (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₃) (r₂ /ₒ s₂)

Tactic:
rw [OreLocalization.expand r₂ s₂ ra (by rw [← ha]; apply SetLike.coe_mem)]

Premises used: OreLocalization.expand
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
c :
  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₁))
⊢ 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₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯)

Tactic:
rw [← Subtype.coe_eq_of_eq_mk ha]

Premises used: Subtype.coe_eq_of_eq_mk
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
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₁))
⊢ 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₁))

Tactic:
rw [oreDiv_smul_oreDiv]

Premises used: OreLocalization.oreDiv_smul_oreDiv
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
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₁))
⊢ 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]

Premises used: OreLocalization.oreDiv_smul_oreDiv
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
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₃))
⊢ 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]

Premises used: OreLocalization.oreDiv_smul_oreDiv
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
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₃))
⊢ 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₁))

Tactic:
repeat rw [oreDiv_smul_oreDiv]

Premises used: OreLocalization.oreDiv_smul_oreDiv
-- 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₃ : 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₃) =
    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:
simp only [smul_add, add_oreDiv]

Premises used: OreLocalization.add_oreDiv, smul_add
-- 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₀ : 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
rw₁ rw₂ : Eq (α := OreLocalization S X) 0 0
⊢ HSMul.hSMul (β := OreLocalization S X) x 0 = 0

Tactic:
rw [← smul_one_oreDiv_one_smul, smul_zero]

Premises used: smul_zero, OreLocalization.smul_one_oreDiv_one_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₀ : 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₀
x_1 x_2 : OreLocalization S X
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2

Tactic:
simp only [← smul_one_oreDiv_one_smul, smul_add]

Premises used: OreLocalization.smul_one_oreDiv_one_smul, smul_add
-- 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 : AddCommMonoid X
inst_3 : DistribMulAction R X
x y : OreLocalization S X
c : ∀ (r : X) (s : ↥S), r /ₒ s + y = y + r /ₒ s
⊢ x + y = y + x

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 : AddCommMonoid X
inst_3 : DistribMulAction R X
y : OreLocalization S X
r : X
s : ↥S
c :
  ∀ (r' : X) (s' : ↥S),
    HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = HAdd.hAdd (α := OreLocalization S X) (r' /ₒ s') (r /ₒ s)
⊢ r /ₒ s + y = y + r /ₒ s

Tactic:
induction y 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 : AddCommMonoid X
inst_3 : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
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)
⊢ 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'⟩

Premises used: OreLocalization.oreDivAddChar'
-- 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 : 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)
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)) ⋯)
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = HAdd.hAdd (α := OreLocalization S X) (r' /ₒ s') (r /ₒ s)

Tactic:
rw [ha', oreDiv_add_char' s' s _ _ ha.symm (ha ▸ (sa * s).2), add_comm]

Premises used: HMul.hMul, OreLocalization.oreDiv_add_char', Eq.rec, add_comm, Eq.symm, 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 : 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)
c : sa * s = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) ⋯
⊢ 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)) ⋯)

Tactic:
congr
-- 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 : 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)
c : (↑(sa * s) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) ⋯) : R)
⊢ sa * s = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) ⋯

Tactic:
ext
-- 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 : 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) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) ⋯) : R)

Tactic:
ha
-- 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 : 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) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s' : R)) ⋯) : R)

Tactic:
exact ha