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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
rcases :
  ∀ (r₃' : R) (s₃' : ↥S) (h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)),
    Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))

Tactic:
rcases oreCondition (s₁' : R) (s₂') with ⟨r₃', s₃', h₃⟩

Premises used: OreLocalization.oreCondition, Subtype.val
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
rw : r₃' * (r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)) = r₃' * r₂' * r₂ * (↑s' : R)
⊢ (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)

Tactic:
rw [mul_assoc, ← h₁, ← mul_assoc, h₃, mul_assoc, h₂]

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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
⊢ r₃' * (r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)) = r₃' * r₂' * r₂ * (↑s' : R)

Tactic:
simp [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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
⊢ (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)

Tactic:
have : s₃' * r₁' * s' = (r₃' * r₂' * r₂) * s' := by
      rw [mul_assoc, ← h₁, ← mul_assoc, h₃, mul_assoc, h₂]
      simp [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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
rcases :
  ∀ (s₄' : ↥S) (h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)),
    Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))

Tactic:
rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩

Premises used: OreLocalization.ore_right_cancel
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
rw : (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R) * (↑s : R)) ∈ S
⊢ (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S

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

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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
⊢ (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R) * (↑s : R)) ∈ S

Tactic:
(s₄' * (s₃' * s₁' * s)).2

Premises used: HMul.hMul, Set.Mem, Subtype.property
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
⊢ (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R) * (↑s : R)) ∈ S

Tactic:
exact (s₄' * (s₃' * s₁' * s)).2

Premises used: HMul.hMul, Subtype.property
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
⊢ (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S

Tactic:
have : (s₄' * r₃') * (s₂' * s) ∈ S := by
      rw [mul_assoc, ← mul_assoc r₃', ← h₃]
      exact (s₄' * (s₃' * s₁' * s)).2
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
rw :
  Eq (α := OreLocalization S X) ((s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)))
    (((↑s₄' : R) * r₃') • r₂' • r₂ • r₁ /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₂' * s) : R)) this)
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))

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

Premises used: HMul.hMul, OreLocalization.expand', OreLocalization.expand
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
simp :
  Eq (α := OreLocalization S X) (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ (s₄' * (s₃' * (s₁' * s))))
    (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯)
⊢ Eq (α := OreLocalization S X) ((s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)))
    (((↑s₄' : R) * r₃') • r₂' • r₂ • r₁ /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₂' * s) : R)) this)

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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
e_s : s₄' * (s₃' * (s₁' * s)) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯
⊢ Eq (α := OreLocalization S X) (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ (s₄' * (s₃' * (s₁' * s))))
    (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯)

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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
e_s :
  (↑(s₄' * (s₃' * (s₁' * s))) : R) =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯) : R)
⊢ s₄' * (s₃' * (s₁' * s)) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯

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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
e_s : (↑s₄' : R) * (↑s₃' : R) * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
⊢ (↑(s₄' * (s₃' * (s₁' * s))) : R) =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯) : 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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
e_s : (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
e_s₁ : (↑s₄' : R) * (r₃' * (↑s₂' : R)) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
e_s₂ e_s₃ : (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
⊢ (↑s₄' : R) * (↑s₃' : R) * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)

Tactic:
rw [mul_assoc (s₄' : R), h₃, ← mul_assoc]

Premises used: mul_assoc, Subtype.val
-- 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
x : OreLocalization S X
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
c :
  ∀ (x : X) (s₂ : ↥S),
    Eq (α := OreLocalization S X) ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) r₁ s)
      ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) (r₂ • r₁)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
⊢ Eq (α := OreLocalization S X) ((fun (x1 : R) (x2 : ↥S) ↦ smul'' x1 x2 x) r₁ s)
    ((fun (x1 : R) (x2 : ↥S) ↦ smul'' x1 x2 x) (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))

Tactic:
cases x with | _ x 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
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
c :
  Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
⊢ Eq (α := OreLocalization S X) ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) r₁ s)
    ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) (r₂ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))

Tactic:
change OreLocalization.smul' r₁ s x s₂ = OreLocalization.smul' (r₂ * r₁) ⟨_, hs⟩ x s₂

Premises used: _private.0.OreLocalization.smul', HMul.hMul, Subtype.mk
-- 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
c :
  ∀ (r₁' : R) (s₁' : ↥S) (h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)),
    Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
      (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
⊢ Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)

Tactic:
rcases oreCondition r₁ s₂ with ⟨r₁', s₁', h₁⟩

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
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)
c :
  Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
⊢ Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)

Tactic:
rw [smul'_char _ _ _ _ _ _ h₁]

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
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)
c :
  ∀ (r₂' : R) (s₂' : ↥S) (h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)),
    Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
      (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
⊢ Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)

Tactic:
rcases oreCondition (r₂ * r₁) s₂ with ⟨r₂', s₂', h₂⟩

Premises used: HMul.hMul, 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
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)
c :
  Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (r₂' • x /ₒ (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
⊢ Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)

Tactic:
rw [smul'_char _ _ _ _ _ _ h₂]

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
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)
c :
  ∀ (r₃' : R) (s₃' : ↥S) (h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)),
    Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
      (r₂' • x /ₒ (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:
rcases oreCondition (s₂' * r₂) (s₁') with ⟨r₃', s₃', h₃⟩

Premises used: HMul.hMul, OreLocalization.oreCondition, Subtype.val
-- 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)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
rw₂ : (↑s₃' : R) * ((↑s₂' : R) * r₂ * r₁) = r₃' * r₁' * (↑s₂ : R)
rw₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) * r₁ = r₃' * r₁' * (↑s₂ : R)
rw₄ : r₃' * (↑s₁' : R) * r₁ = r₃' * r₁' * (↑s₂ : R)
rw₅ : r₃' * ((↑s₁' : R) * r₁) = r₃' * r₁' * (↑s₂ : R)
rw₆ : r₃' * (r₁' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₇ rw₈ : r₃' * (r₁' * (↑s₂ : R)) = r₃' * (r₁' * (↑s₂ : R))
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)

Tactic:
rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
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)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)

Tactic:
have : s₃' * r₂' * s₂ = r₃' * r₁' * s₂ := by
      rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
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 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
c :
  ∀ (s₄' : ↥S) (h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')),
    Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
      (r₂' • x /ₒ (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:
rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩

Premises used: OreLocalization.ore_right_cancel
-- 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 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
rw : (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * (r₂ * (↑s : R)) ∈ S
⊢ (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S

Tactic:
rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← 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
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 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
⊢ (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * (r₂ * (↑s : R)) ∈ S

Tactic:
mul_mem (s₄' * s₃' * s₂').2 hs

Premises used: HMul.hMul, Subtype.property, MulMemClass.mul_mem
-- 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 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
⊢ (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * (r₂ * (↑s : R)) ∈ S

Tactic:
exact mul_mem (s₄' * s₃' * s₂').2 hs

Premises used: HMul.hMul, Subtype.property, MulMemClass.mul_mem
-- 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 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
⊢ (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S

Tactic:
have : (s₄' * r₃') * (s₁' * s) ∈ S := by
      rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]
      exact mul_mem (s₄' * s₃' * s₂').2 hs