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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : (↑u : R) * (↑(r₂, s₂).snd : R) = v * (↑(r₁, s₁).snd : R)
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : (↑u' : R) * (↑(r₃, s₃).snd : R) = v' * (↑(r₂, s₂).snd : R)
refine_2 :
  ∀ (r' : R) (s' : ↥S) (h : (↑s' : R) * v' = r' * (↑u : R)),
    ∃ (u : ↥S),
      ∃ (v : R), u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ (↑u : R) * (↑(r₃, s₃).snd : R) = v * (↑(r₁, s₁).snd : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ (↑u : R) * (↑(r₃, s₃).snd : R) = v * (↑(r₁, s₁).snd : R)

Tactic:
rcases oreCondition v' u 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
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : (↑u : R) * (↑(r₂, s₂).snd : R) = v * (↑(r₁, s₁).snd : R)
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : (↑u' : R) * (↑(r₃, s₃).snd : R) = v' * (↑(r₂, s₂).snd : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : ∃ (u : ↥S), ∃ (v : R), u • r₃ = v • r₁ ∧ (↑u : R) * (↑s₃ : R) = v * (↑s₁ : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ (↑u : R) * (↑(r₃, s₃).snd : R) = v * (↑(r₁, s₁).snd : R)

Tactic:
dsimp only at *
-- 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
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r₃ = v • r₁ ∧ (↑u : R) * (↑s₃ : R) = v * (↑s₁ : R)

Tactic:
⟨s' * u', r' * v, ?_, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro
-- 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
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (s' * u') • r₃ = (r' * v) • r₁
refine_2₁ : (↑(s' * u') : R) * (↑s₃ : R) = r' * v * (↑s₁ : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r₃ = v • r₁ ∧ (↑u : R) * (↑s₃ : R) = v * (↑s₁ : R)

Tactic:
refine ⟨s' * u', r' * v, ?_, ?_⟩
-- 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
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁
⊢ (s' * u') • r₃ = (r' * v) • r₁

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *

Premises used: mul_assoc, Submonoid.smul_def, SemigroupAction.mul_smul, 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))
⊢ (↑(s' * u') : R) * (↑s₃ : R) = r' * v * (↑s₁ : R)

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *

Premises used: mul_assoc, Submonoid.smul_def, SemigroupAction.mul_smul, 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) • v' • r₂ = r' • v • r₁
refine_2₁ : ((↑s' : R) * v') • r₂ = r' • v • r₁
refine_2₂ : (r' * (↑u : R)) • r₂ = r' • v • r₁
refine_2₃ : r' • (↑u : R) • r₂ = r' • v • r₁
refine_2₄ refine_2₅ : r' • v • r₁ = r' • v • r₁
⊢ (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁

Tactic:
rw [hur₂, smul_smul, h, mul_smul, hur₁]

Premises used: smul_smul, 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) * (v' * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
refine_2₁ : (↑s' : R) * v' * (↑s₂ : R) = r' * (v * (↑s₁ : R))
refine_2₂ : r' * (↑u : R) * (↑s₂ : R) = r' * (v * (↑s₁ : R))
refine_2₃ : r' * ((↑u : R) * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
refine_2₄ refine_2₅ : r' * (v * (↑s₁ : R)) = r' * (v * (↑s₁ : R))
⊢ (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))

Tactic:
rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]

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
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
a : ∀ (a : Prod.{u_2, u_1} X ↥S), β ⟦a⟧
⊢ ∀ (q : OreLocalization S X), β q

Tactic:
apply Quotient.ind

Premises used: Quotient.ind
-- 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
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
r : X
s : ↥S
⊢ β ⟦(r, s)⟧

Tactic:
c r s

Premises used: Quotient.mk', 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
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
r : X
s : ↥S
⊢ β ⟦(r, s)⟧

Tactic:
exact c 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₂ : X
s₁ s₂ : ↥S
⊢ Eq (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) ↔
    ∃ (u : ↥S), ∃ (v : R), u • r₂ = v • r₁ ∧ (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)

Tactic:
Quotient.eq''

Premises used: OreLocalization, Quotient.eq'', Quotient.mk', 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 : X
s : ↥S
t : R
hst : t * (↑s : R) ∈ S
a : (r, s) ≈ (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst)
⊢ Eq (α := OreLocalization S X) (r /ₒ s) (t • r /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst)

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- 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
t : R
hst : t * (↑s : R) ∈ S
rw : s • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = (↑s : R) • t • (r, s).fst
rw₁ rw₂ : (↑s : R) • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = (↑s : R) • t • (r, s).fst
⊢ s • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = ((↑s : R) * t) • (r, s).fst

Tactic:
rw [mul_smul, Submonoid.smul_def]

Premises used: Submonoid.smul_def, 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 : X
s : ↥S
t : R
hst : t * (↑s : R) ∈ S
rw rw₁ : (↑s : R) * t * (↑s : R) = (↑s : R) * t * (↑(r, s).snd : R)
⊢ (↑s : R) * (↑(t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).snd : R) =
    (↑s : R) * t * (↑(r, s).snd : R)

Tactic:
rw [← 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 : X
s : ↥S
t : R
hst : t * (↑s : R) ∈ S
⊢ (r, s) ≈ (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst)

Tactic:
exact ⟨s, s * t, by rw [mul_smul, Submonoid.smul_def], by rw [← 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 : X
s s' : ↥S
norm_cast : (↑(s' * s) : R) ∈ S
⊢ (↑s' : R) * (↑s : R) ∈ S

Tactic:
norm_cast
-- 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
⊢ (↑(s' * s) : R) ∈ S

Tactic:
apply SetLike.coe_mem

Premises used: SetLike.coe_mem
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
rcases :
  ∀ (r₁' : R) (t' : ↥S) (hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)),
    Eq (α := OreLocalization S R) (r₁ * r * r₂ /ₒ s) (r₁ * r' * r₂ /ₒ s)
⊢ Eq (α := OreLocalization S R) (r₁ * r * r₂ /ₒ s) (r₁ * r' * r₂ /ₒ s)

Tactic:
rcases oreCondition r₁ t with ⟨r₁', t', hr₁⟩

Premises used: OreLocalization.oreCondition
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
rw : Eq (α := OreLocalization S R) (t' • (r₁ * r * r₂) /ₒ (t' * s)) (t' • (r₁ * r' * r₂) /ₒ (t' * s))
⊢ Eq (α := OreLocalization S R) (r₁ * r * r₂ /ₒ s) (r₁ * r' * r₂ /ₒ s)

Tactic:
rw [OreLocalization.expand' _ s t', OreLocalization.expand' _ s t']

Premises used: OreLocalization.expand'
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
e_r : t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
⊢ Eq (α := OreLocalization S R) (t' • (r₁ * r * r₂) /ₒ (t' * s)) (t' • (r₁ * r' * r₂) /ₒ (t' * s))

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * 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
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
rw rw₁ : r₁' * (↑t : R) * r * r₂ = r₁' * (↑t : R) * r * r₂
⊢ (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂

Tactic:
rw [hr₁]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ r₁' * (↑t : R) * r * r₂ = r₁' * ((↑t : R) * r) * 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
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
rw rw₁ : r₁' * ((↑t : R) * r') * r₂ = r₁' * ((↑t : R) * r') * r₂
⊢ r₁' * ((↑t : R) * r) * r₂ = r₁' * ((↑t : R) * r') * r₂

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ r₁' * ((↑t : R) * r') * r₂ = r₁' * (↑t : R) * r' * 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
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
rw rw₁ : r₁' * (↑t : R) * r' * r₂ = r₁' * (↑t : R) * r' * r₂
⊢ r₁' * (↑t : R) * r' * r₂ = (↑t' : R) * r₁ * r' * r₂

Tactic:
rw [hr₁]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ (↑t' : R) * r₁ * r' * r₂ = (↑t' : R) * (r₁ * r' * 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
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
calc₁ : (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
calc₂ : r₁' * (↑t : R) * r * r₂ = r₁' * ((↑t : R) * r) * r₂
calc₃ : r₁' * ((↑t : R) * r) * r₂ = r₁' * ((↑t : R) * r') * r₂
calc₄ : r₁' * ((↑t : R) * r') * r₂ = r₁' * (↑t : R) * r' * r₂
calc₅ : r₁' * (↑t : R) * r' * r₂ = (↑t' : R) * r₁ * r' * r₂
calc₆ : (↑t' : R) * r₁ * r' * r₂ = (↑t' : R) * (r₁ * r' * r₂)
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)

Tactic:
calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← mul_assoc]

Premises used: HMul.hMul, 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₂ : (↑u : R) * (↑(r₂, s₂).snd : R) = v * (↑(r₁, s₁).snd : R)
dsimp : P r₁ s₁ = P r₂ s₂
⊢ Eq.{u_2} (α := C) ((fun (p : Prod.{u_3, u_1} X ↥S) ↦ P p.fst p.snd) (r₁, s₁))
    ((fun (p : Prod.{u_3, u_1} X ↥S) ↦ P p.fst p.snd) (r₂, s₂))

Tactic:
dsimp at *
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
rw : (↑(u * s₂) : R) ∈ S
⊢ v * (↑s₁ : R) ∈ S

Tactic:
rw [← hs₂, ← S.coe_mul]

Premises used: 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
⊢ (↑(u * s₂) : R) ∈ S

Tactic:
SetLike.coe_mem (u * s₂)

Premises used: HMul.hMul, SetLike.coe_mem
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
⊢ (↑(u * s₂) : R) ∈ S

Tactic:
exact SetLike.coe_mem (u * s₂)

Premises used: HMul.hMul, SetLike.coe_mem
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
⊢ v * (↑s₁ : R) ∈ S

Tactic:
have s₁vS : v * s₁ ∈ S := by
      rw [← hs₂, ← S.coe_mul]
      exact SetLike.coe_mem (u * s₂)
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
s₁vS : v * (↑s₁ : R) ∈ S
a : (↑(u * s₂) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) : R)
⊢ u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS

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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
s₁vS : v * (↑s₁ : R) ∈ S
⊢ (↑(u * s₂) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) : R)

Tactic:
simp [hs₂]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
s₁vS : v * (↑s₁ : R) ∈ S
⊢ u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS

Tactic:
replace hs₂ : u * s₂ = ⟨_, s₁vS⟩ := by ext; simp [hs₂]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
norm_cast : (↑(u * s₂) : R) ∈ S
⊢ (↑u : R) * (↑s₂ : R) ∈ S

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
rwa rwa₁ rwa₂ rwa₃ : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) : R) ∈ S
⊢ (↑(u * s₂) : R) ∈ S

Tactic:
rwa [hs₂]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
rw :
  P (u • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) =
    P ((↑u : R) • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑u : R) * (↑s₂ : R)) ⋯)
⊢ P r₁ s₁ = P r₂ s₂

Tactic:
rw [hP r₁ v s₁ s₁vS, hP r₂ u s₂ (by norm_cast; rwa [hs₂]), ← hr₂]

Premises used: 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
simp : P (u • r₂) (u * s₂) = P ((↑u : R) • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑u : R) * (↑s₂ : R)) ⋯)
⊢ P (u • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) =
    P ((↑u : R) • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑u : R) * (↑s₂ : R)) ⋯)

Tactic:
simp only [← hs₂]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
⊢ P (u • r₂) (u * s₂) = P ((↑u : R) • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑u : R) * (↑s₂ : R)) ⋯)

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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
r : X
s : ↥S
⊢ liftExpand P hP (r /ₒ s) = P r s

Tactic:
rfl

Premises used: OreLocalization.liftExpand, rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * (↑s₁ : R) ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * (↑s₂ : R) ∈ S),
    P r₁ s₁ r₂ s₂ =
      P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (t₂ • r₂)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
r₁ : X
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * (↑s₂ : R) ∈ S
⊢ 1 * (↑s₁ : R) ∈ S

Tactic:
simp