awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c :
  Eq (α := OreLocalization S X)
    (((↑s₄' : R) * r₃') • r₁' • x /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₁' * s) : R)) this)
    ((s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs)))
⊢ Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (r₂' • x /ₒ (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))

Tactic:
rw [OreLocalization.expand' (r₂' • x) _ (s₄' * s₃'), OreLocalization.expand _ _ _ this]

Premises used: HMul.hMul, OreLocalization.expand', OreLocalization.expand, HSMul.hSMul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c :
  Eq (α := OreLocalization S X)
    (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯)
    (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ (s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))))
⊢ Eq (α := OreLocalization S X)
    (((↑s₄' : R) * r₃') • r₁' • x /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₁' * s) : R)) this)
    ((s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs)))

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]

Premises used: mul_assoc, smul_smul, Submonoid.smul_def, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c :
  Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯ =
    s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
⊢ Eq (α := OreLocalization S X)
    (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯)
    (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ (s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))))

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c :
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯) : R) =
    (↑(s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))) : R)
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯ =
    s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))

Tactic:
ext
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c : (↑s₄' : R) * r₃' * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯) : R) =
    (↑(s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))) : R)

Tactic:
simp only [Submonoid.coe_mul, ← mul_assoc]

Premises used: mul_assoc, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c : (↑s₄' : R) * (r₃' * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
c₁ : (↑s₄' : R) * ((↑s₃' : R) * ((↑s₂' : R) * r₂)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
c₂ : (↑s₄' : R) * (↑s₃' : R) * ((↑s₂' : R) * r₂) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
c₃ c₄ : (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
⊢ (↑s₄' : R) * r₃' * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)

Tactic:
rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : (↑s' : R) * r₁ = r' * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Tactic:
smul'_char r₁ r₂ s₁ s₂ s' r' huv

Premises used: _private.0.OreLocalization.smul'_char, Quotient.mk', OreLocalization.liftExpand, OreLocalization.oreDiv
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : (↑s' : R) * r₁ = r' * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Tactic:
exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Premises used: _private.0.OreLocalization.smul'_char
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : (↑s' : R) * r₁ = r' * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Tactic:
with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Premises used: _private.0.OreLocalization.smul'_char
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : (↑s' : R) * r₁ = r' * (↑s₂ : R)
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Tactic:
smul'_char r₁ r₂ s₁ s₂ s' r' huv

Premises used: _private.0.OreLocalization.smul'_char, Quotient.mk', OreLocalization.liftExpand, OreLocalization.oreDiv
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : (↑s' : R) * r₁ = r' * (↑s₂ : R)
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Tactic:
exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Premises used: _private.0.OreLocalization.smul'_char
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : (↑s' : R) * r₁ = r' * (↑s₂ : R)
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Tactic:
with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Premises used: _private.0.OreLocalization.smul'_char
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
inst_3 : One X
⊢ Eq (α := OreLocalization S X) 1 (1 /ₒ 1)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
inst_3 : One X
⊢ Eq (α := OreLocalization S X) 1 (1 /ₒ 1)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
hr : r ∈ S
rw :
  ∃ (u : ↥S),
    ∃ (v : R),
      HSMul.hSMul (β := R) u 1 = v • r ∧ (↑u : R) * (↑1 : R) = v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) : R)
⊢ Eq (α := OreLocalization S R) (r /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) 1

Tactic:
rw [OreLocalization.one_def, oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff, OreLocalization.one_def
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
hr : r ∈ S
⊢ HSMul.hSMul (β := R) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) 1 = HSMul.hSMul (α := R) 1 r

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
hr : r ∈ S
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) : R) * (↑1 : R) =
    1 * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) : R)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
hr : r ∈ S
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      HSMul.hSMul (β := R) u 1 = v • r ∧ (↑u : R) * (↑1 : R) = v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) : R)

Tactic:
exact ⟨⟨r, hr⟩, 1, by simp, by simp⟩
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
s : ↥S
⊢ Eq (α := OreLocalization S R) ((↑s : R) /ₒ s) 1

Tactic:
OreLocalization.div_eq_one' _

Premises used: OreLocalization.div_eq_one'
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
x : OreLocalization S X
c : ∀ (r : X) (s : ↥S), HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) 1 (r /ₒ s) = r /ₒ s
⊢ HSMul.hSMul (α := OreLocalization S R) 1 x = x

Tactic:
cases x with | _ r s
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
⊢ (↑s : R) * 1 = 1 * (↑s : R)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) 1 (r /ₒ s) = r /ₒ s

Tactic:
simp [OreLocalization.one_def, oreDiv_smul_char 1 r 1 s 1 s (by simp)]

Premises used: OreLocalization.one_def, OreLocalization.oreDiv_smul_char, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x : OreLocalization S R
⊢ 1 * x = x

Tactic:
OreLocalization.one_smul x

Premises used: OreLocalization.one_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x : OreLocalization S R
c : ∀ (r : R) (s : ↥S), HMul.hMul (α := OreLocalization S R) (r /ₒ s) 1 = r /ₒ s
⊢ x * 1 = x

Tactic:
cases x with | _ r s
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
⊢ (↑1 : R) * r = r * (↑1 : R)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r /ₒ s) 1 = r /ₒ s

Tactic:
simp [OreLocalization.one_def, oreDiv_mul_char r (1 : R) s (1 : S) r 1 (by simp)]

Premises used: OreLocalization.oreDiv_mul_char, OreLocalization.one_def, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
x y : OreLocalization S R
z : OreLocalization S X
c : ∀ (r₁ : R) (s₁ : ↥S), (r₁ /ₒ s₁ * y) • z = HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (y • z)
⊢ (x * y) • z = x • y • z

Tactic:
cases x with | _ r₁ s₁
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
c :
  ∀ (r₂ : R) (s₂ : ↥S),
    HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) • z =
      HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (HSMul.hSMul (α := OreLocalization S R) (r₂ /ₒ s₂) z)
⊢ (r₁ /ₒ s₁ * y) • z = HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (y • z)

Tactic:
cases y with | _ r₂ s₂
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
c :
  ∀ (r₃ : X) (s₃ : ↥S),
    HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
      HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
        (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) • z =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (HSMul.hSMul (α := OreLocalization S R) (r₂ /ₒ s₂) z)

Tactic:
cases z with | _ r₃ s₃
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
c :
  ∀ (ra : R) (sa : ↥S) (ha : (↑sa : R) * r₁ = ra * (↑s₂ : R))
    (ha' : HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)),
    HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
      HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
        (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
⊢ HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))

Tactic:
rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩

Premises used: OreLocalization.oreDivMulChar'
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
ha' : HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
⊢ HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))

Tactic:
rw [ha']
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
c :
  ∀ (rb : R) (sb : ↥S) (hb : (↑sb : R) * r₂ = rb * (↑s₃ : R))
    (hb' :
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)),
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
      HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
        (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))

Tactic:
rcases oreDivSMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩

Premises used: OreLocalization.oreDivSMulChar'
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * r₂ = rb * (↑s₃ : R)
hb' : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))

Tactic:
rw [hb']
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * r₂ = rb * (↑s₃ : R)
c :
  ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * ra = rc * (↑sb : R)),
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))

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

Premises used: OreLocalization.oreCondition
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * r₂ = rb * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ra = rc * (↑sb : R)
c :
  (rc * rb) • r₃ /ₒ (sc * (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
c₁ : (↑sc : R) * (ra * r₂) = rc * rb * (↑s₃ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))

Tactic:
rw [oreDiv_smul_char (ra * r₂) r₃ (sa * s₁) s₃ (rc * rb) sc]

Premises used: HMul.hMul, OreLocalization.oreDiv_smul_char
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * r₂ = rb * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ra = rc * (↑sb : R)
c : (↑sc : R) * ra * r₂ = rc * rb * (↑s₃ : R)
c₁ : rc * (↑sb : R) * r₂ = rc * rb * (↑s₃ : R)
c₂ : rc * ((↑sb : R) * r₂) = rc * rb * (↑s₃ : R)
c₃ : rc * (rb * (↑s₃ : R)) = rc * rb * (↑s₃ : R)
c₄ c₅ : rc * rb * (↑s₃ : R) = rc * rb * (↑s₃ : R)
⊢ (↑sc : R) * (ra * r₂) = rc * rb * (↑s₃ : R)

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

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * r₂ = rb * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ra = rc * (↑sb : R)
c :
  rc • rb • r₃ /ₒ (sc * sa * s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
⊢ (rc * rb) • r₃ /ₒ (sc * (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))

Tactic:
rw [← mul_assoc, mul_smul]

Premises used: mul_assoc, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * r₂ = rb * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ra = rc * (↑sb : R)
c :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂)) =
    rc • rb • r₃ /ₒ (sc * sa * s₁)
⊢ rc • rb • r₃ /ₒ (sc * sa * s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))

Tactic:
symm