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_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
⊢ P r₁ s₁ r₂ s₂ =
    P (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (1 * (↑s₁ : R)) ⋯) (t₂ • r₂)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)

Tactic:
have := hP r₁ 1 s₁ (by simp) r₂ t₂ s₂ ht₂
-- 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
this :
  P r₁ s₁ r₂ s₂ =
    P (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (1 * (↑s₁ : R)) ⋯) (t₂ • r₂)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
⊢ P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)

Tactic:
simp [this]
-- 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
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
h :
  ∀ (x : OreLocalization S X),
    Eq.{u_2} (α := C) ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) r₁ s₁ x)
      ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) (t₁ • r₁)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) x)
⊢ Eq (α := OreLocalization S X → C)
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) r₁ s₁)
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) (t₁ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁))

Tactic:
ext x
-- 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
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
x : OreLocalization S X
h :
  ∀ (r₂ : X) (s₂ : ↥S),
    Eq.{u_2} (α := C) ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) r₁ s₁ (r₂ /ₒ s₂))
      ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) (t₁ • r₁)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (r₂ /ₒ s₂))
⊢ Eq.{u_2} (α := C) ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) r₁ s₁ x)
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) (t₁ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) 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_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
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
r₂ : X
s₂ : ↥S
h :
  liftExpand (P r₁ s₁) ⋯ (r₂ /ₒ s₂) =
    liftExpand (P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁)) ⋯ (r₂ /ₒ s₂)
⊢ Eq.{u_2} (α := C) ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) r₁ s₁ (r₂ /ₒ s₂))
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) (t₁ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (r₂ /ₒ s₂))

Tactic:
dsimp only
-- 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
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
r₂ : X
s₂ : ↥S
⊢ 1 * (↑s₂ : R) ∈ S

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_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
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
r₂ : X
s₂ : ↥S
h :
  P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 r₂)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (1 * (↑s₂ : R)) ⋯) =
    P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) r₂ s₂
⊢ liftExpand (P r₁ s₁) ⋯ (r₂ /ₒ s₂) =
    liftExpand (P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁)) ⋯ (r₂ /ₒ s₂)

Tactic:
rw [liftExpand_of, liftExpand_of, hP r₁ t₁ s₁ ht₁ r₂ 1 s₂ (by simp)]

Premises used: OreLocalization.liftExpand_of, 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_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
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
r₂ : X
s₂ : ↥S
⊢ P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 r₂)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (1 * (↑s₂ : R)) ⋯) =
    P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) r₂ s₂

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_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
s₂ : ↥S
⊢ lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂

Tactic:
rfl

Premises used: OreLocalization.lift₂Expand, 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_2
inst_2 : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
⊢ (↑(oreDenom r₁ s₂) : R) * r₁ = oreNum r₁ s₂ * (↑s₂ : R)

Tactic:
have h₀ := ore_eq 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
h₀ : (↑(oreDenom r₁ s₂) : R) * r₁ = oreNum r₁ s₂ * (↑s₂ : R)
set :
  let v₀ := oreNum r₁ s₂;
  ∀ (h₀ : (↑(oreDenom r₁ s₂) : R) * r₁ = v₀ * (↑s₂ : R)),
    Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)) (v • r₂ /ₒ (u * s₁))
⊢ Eq (α := OreLocalization S X) (oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)) (v • r₂ /ₒ (u * s₁))

Tactic:
set v₀ := oreNum r₁ s₂

Premises used: OreLocalization.oreNum
-- 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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
h₀ : (↑(oreDenom r₁ s₂) : R) * r₁ = v₀ * (↑s₂ : R)
set :
  let u₀ := oreDenom r₁ s₂;
  ∀ (h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)), Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)) (v • r₂ /ₒ (u * s₁))

Tactic:
set u₀ := oreDenom r₁ s₂

Premises used: OreLocalization.oreDenom
-- 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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
rcases :
  ∀ (r₃ : R) (s₃ : ↥S) (h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)),
    Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))

Tactic:
rcases oreCondition (u₀ : R) u 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
rw : r₃ * (v * (↑s₂ : R)) = r₃ * ((↑u : R) * r₁)
rw₁ rw₂ : r₃ * ((↑u : R) * r₁) = r₃ * ((↑u : R) * r₁)
⊢ r₃ * v * (↑s₂ : R) = r₃ * ((↑u : R) * r₁)

Tactic:
rw [mul_assoc, ← huv]

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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
rw : r₃ * (↑u : R) * r₁ = (↑s₃ : R) * ((↑u₀ : R) * r₁)
rw₁ : r₃ * (↑u : R) * r₁ = (↑s₃ : R) * (↑u₀ : R) * r₁
rw₂ rw₃ : r₃ * (↑u : R) * r₁ = r₃ * (↑u : R) * r₁
⊢ r₃ * ((↑u : R) * r₁) = (↑s₃ : R) * ((↑u₀ : R) * r₁)

Tactic:
rw [← mul_assoc, ← 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
rw : (↑s₃ : R) * ((↑u₀ : R) * r₁) = (↑s₃ : R) * (v₀ * (↑s₂ : R))
rw₁ rw₂ : (↑s₃ : R) * (v₀ * (↑s₂ : R)) = (↑s₃ : R) * (v₀ * (↑s₂ : R))
⊢ (↑s₃ : R) * ((↑u₀ : R) * r₁) = (↑s₃ : R) * v₀ * (↑s₂ : R)

Tactic:
rw [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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
⊢ r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)

Tactic:
have :=
    calc
      r₃ * v * s₂ = r₃ * (u * r₁) := by rw [mul_assoc, ← huv]
      _ = s₃ * (u₀ * r₁) := by rw [← mul_assoc, ← mul_assoc, h₃]
      _ = s₃ * v₀ * s₂ := by rw [mul_assoc, h₀]
-- 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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
rcases :
  ∀ (s₄ : ↥S) (hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)),
    Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))

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

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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
symm : Eq (α := OreLocalization S X) (v • r₂ /ₒ (u * s₁)) (v₀ • r₂ /ₒ (u₀ * s₁))
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))

Tactic:
symm
-- 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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
rw : ∃ (u_1 : ↥S), ∃ (v_1 : R), u_1 • v₀ • r₂ = v_1 • v • r₂ ∧ (↑u_1 : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)
⊢ Eq (α := OreLocalization S X) (v • r₂ /ₒ (u * s₁)) (v₀ • r₂ /ₒ (u₀ * s₁))

Tactic:
rw [oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff
-- 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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
h : ∃ (v_1 : R), (s₄ * s₃) • v₀ • r₂ = v_1 • v • r₂ ∧ (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)
⊢ ∃ (u_1 : ↥S), ∃ (v_1 : R), u_1 • v₀ • r₂ = v_1 • v • r₂ ∧ (↑u_1 : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)

Tactic:
use s₄ * 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
h :
  (s₄ * s₃) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
    (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = (↑s₄ : R) * r₃ * (↑(u * s₁) : R)
⊢ ∃ (v_1 : R), (s₄ * s₃) • v₀ • r₂ = v_1 • v • r₂ ∧ (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)

Tactic:
use s₄ * r₃
-- 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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
h :
  ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
    (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
⊢ (s₄ * s₃) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
    (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = (↑s₄ : R) * r₃ * (↑(u * s₁) : R)

Tactic:
simp only [Submonoid.coe_mul, Submonoid.smul_def]

Premises used: 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
h : ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂
h₁ : (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
⊢ ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
    (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))

Tactic:
constructor
-- 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₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
h : ((↑s₄ : R) * (r₃ * v)) • r₂ = ((↑s₄ : R) * r₃) • v • r₂
⊢ ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂

Tactic:
rw [smul_smul, mul_assoc (c := v₀), ← hs₄]

Premises used: mul_assoc, smul_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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ ((↑s₄ : R) * (r₃ * v)) • r₂ = ((↑s₄ : R) * r₃) • v • r₂

Tactic:
simp only [smul_smul, mul_assoc]

Premises used: mul_assoc, smul_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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
h : (↑s₄ : R) * (r₃ * (↑u : R)) * (↑s₁ : R) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
⊢ (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))

Tactic:
rw [← mul_assoc (b := (u₀ : R)), mul_assoc (c := (u₀ : R)), h₃]

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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ (↑s₄ : R) * (r₃ * (↑u : R)) * (↑s₁ : R) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))

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

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

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

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

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

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

Premises used: _private.0.OreLocalization.smul'_char