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₂ : 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 * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂)) =
    rc • rb • r₃ /ₒ (sc * sa * s₁)

Tactic:
apply oreDiv_smul_char

Premises used: 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) * (↑sa : R) * r₁ = rc * (↑(sb * s₂) : R)
c₁ : (↑sc : R) * (↑sa : R) * r₁ = rc * ((↑sb : R) * (↑s₂ : R))
c₂ : (↑sc : R) * (↑sa : R) * r₁ = rc * (↑sb : R) * (↑s₂ : R)
c₃ : (↑sc : R) * (↑sa : R) * r₁ = (↑sc : R) * ra * (↑s₂ : R)
c₄ : (↑sc : R) * (↑sa : R) * r₁ = (↑sc : R) * (ra * (↑s₂ : R))
c₅ : (↑sc : R) * (↑sa : R) * r₁ = (↑sc : R) * ((↑sa : R) * r₁)
c₆ c₇ : (↑sc : R) * ((↑sa : R) * r₁) = (↑sc : R) * ((↑sa : R) * r₁)
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)

Tactic:
rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, 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 y z : OreLocalization S R
⊢ x * y * z = x * (y * z)

Tactic:
OreLocalization.mul_smul x y z

Premises used: OreLocalization.mul_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
s s' : ↥S
⊢ (↑1 : R) * (↑s : R) = 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
s s' : ↥S
⊢ HMul.hMul (α := OreLocalization S R) ((↑s : R) /ₒ s') ((↑s' : R) /ₒ s) = 1

Tactic:
simp [oreDiv_mul_char (s : R) s' s' s 1 1 (by simp)]

Premises used: OreLocalization.oreDiv_mul_char, OfNat.ofNat, 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 : X
s t : ↥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 t : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (1 /ₒ t) (r /ₒ s) = r /ₒ (s * t)

Tactic:
simp [oreDiv_smul_char 1 r t s 1 s (by simp)]

Premises used: 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
r : R
s t : ↥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
r : R
s t : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (1 /ₒ t) (r /ₒ s) = r /ₒ (s * t)

Tactic:
simp [oreDiv_mul_char 1 r t s 1 s (by simp)]

Premises used: OreLocalization.oreDiv_mul_char, 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
r : X
s t : ↥S
⊢ (↑1 : R) * (↑s : R) = 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 t : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((↑s : R) /ₒ t) (r /ₒ s) = r /ₒ t

Tactic:
simp [oreDiv_smul_char s.1 r t s 1 1 (by simp)]

Premises used: OreLocalization.oreDiv_smul_char, OfNat.ofNat, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
s t : ↥S
⊢ (↑1 : R) * (↑s : R) = 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
r : R
s t : ↥S
⊢ HMul.hMul (α := OreLocalization S R) ((↑s : R) /ₒ t) (r /ₒ s) = r /ₒ t

Tactic:
simp [oreDiv_mul_char s.1 r t s 1 1 (by simp)]

Premises used: OreLocalization.oreDiv_mul_char, OfNat.ofNat, 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 t : ↥S
⊢ (↑1 : R) * (r₁ * (↑s : R)) = r₁ * (↑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₁ : R
r₂ : X
s t : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ * (↑s : R) /ₒ t) (r₂ /ₒ s) = r₁ • r₂ /ₒ t

Tactic:
simp [oreDiv_smul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

Premises used: HMul.hMul, OreLocalization.oreDiv_smul_char, OfNat.ofNat, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s t : ↥S
⊢ (↑1 : R) * (r₁ * (↑s : R)) = r₁ * (↑s : 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₂ : R
s t : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r₁ * (↑s : R) /ₒ t) (r₂ /ₒ s) = r₁ * r₂ /ₒ t

Tactic:
simp [oreDiv_mul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

Premises used: HMul.hMul, OreLocalization.oreDiv_mul_char, OfNat.ofNat, 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
p : R
r : X
s : ↥S
⊢ (↑1 : R) * p = p * (↑1 : 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
p : R
r : X
s : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (p /ₒ s) (r /ₒ 1) = p • r /ₒ s

Tactic:
simp [oreDiv_smul_char p r s 1 p 1 (by simp)]

Premises used: 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
p r : R
s : ↥S
⊢ (↑1 : R) * p = p * (↑1 : R)

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

Tactic:
simp [oreDiv_mul_char p r s 1 p 1 (by simp)]

Premises used: OreLocalization.oreDiv_mul_char, 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.78480
inst_2 : MulAction R X
⊢ Eq.{u_1 + 1} (α := OreLocalization S R) (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.78480
inst_2 : MulAction R X
⊢ Eq.{u_1 + 1} (α := OreLocalization S R) (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
⊢ Eq (α := OreLocalization S R) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R)
    (r /ₒ 1 : OreLocalization S R)

Tactic:
rfl

Premises used: Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
s : ↥S
⊢ IsUnit (M := OreLocalization S R) ((numeratorHom : (a : R) → OreLocalization S R) (↑s : R) : OreLocalization S R)

Tactic:
⟨numeratorUnit s, rfl⟩

Premises used: IsUnit, OreLocalization.numeratorUnit, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
simp :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T) =
    HMul.hMul (α := T) (β := T)
      ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) : T)
      ((f : (a : R) → T) (t * r) : T)
⊢ Eq.{u_2 + 1} (α := T)
    ((fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      r s)
    ((fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))

Tactic:
simp only [smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
⊢ (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) t : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)

Tactic:
simp only [← hf, map_mul]

Premises used: map_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
⊢ (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) t : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)

Tactic:
have : (fS ⟨t * s, ht⟩ : T) = f t * fS s := by
        simp only [← hf, map_mul]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
this :
  (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) t : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
rw :
  (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) *
    HMul.hMul (α := T) ((f : (a : R) → T) t : T)
      (HMul.hMul (β := T)
        (↑(HMul.hMul (α := Tˣ) (β := Tˣ) ((fS : (a : ↥S) → Tˣ) s : Tˣ) (((fS : (a : ↥S) → Tˣ) s)⁻¹ : Tˣ)) : T)
        ((f : (a : R) → T) r : T))
| HMul.hMul (α := T) (β := T)
    ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) : T)
    ((f : (a : R) → T) (t * r) : T)

Tactic:
rw [map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]

Premises used: map_mul, Units.val_one, mul_inv_cancel, DFunLike.coe, one_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
this :
  (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) t : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
rw :
  HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T)
      (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) *
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
| (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) *
    HMul.hMul (α := T) ((f : (a : R) → T) t : T)
      (HMul.hMul (β := T)
        (↑(HMul.hMul (α := Tˣ) (β := Tˣ) ((fS : (a : ↥S) → Tˣ) s : Tˣ) (((fS : (a : ↥S) → Tˣ) s)⁻¹ : Tˣ)) : T)
        ((f : (a : R) → T) r : T))

Tactic:
rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]

Premises used: Units.val, mul_assoc, DFunLike.coe, Units.val_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
this :
  (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) t : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
rw :
  HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T)
      (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) *
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
| HMul.hMul (α := T) (β := T)
    ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) : T)
    ((f : (a : R) → T) (t * r) : T)

Tactic:
rw [map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]
        rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]

Premises used: Units.val, mul_assoc, map_mul, Units.val_one, mul_inv_cancel, DFunLike.coe, Units.val_mul, one_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
this :
  (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) t : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
conv_rhs :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T) =
    HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T)
        (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) *
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
⊢ HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T) =
    HMul.hMul (α := T) (β := T)
      ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) : T)
      ((f : (a : R) → T) (t * r) : T)

Tactic:
conv_rhs =>
        rw [map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]
        rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]

Premises used: Units.val, mul_assoc, map_mul, Units.val_one, mul_inv_cancel, DFunLike.coe, Units.val_mul, one_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * (↑s : R) ∈ S
this :
  (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) t : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
⊢ HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T) =
    HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T)
        (↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)) : T) *
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)

Tactic:
simp only [one_mul, Units.inv_mul]

Premises used: Units.inv_mul, one_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
rw : HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) 1)⁻¹ : T) : T) ((f : (a : R) → T) 1 : T) = 1
⊢ Eq.{u_2 + 1} (α := T)
    (liftExpand (S := S)
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ 1)
    1

Tactic:
rw [OreLocalization.one_def, liftExpand_of]

Premises used: OreLocalization.liftExpand_of, OreLocalization.one_def
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
⊢ HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) 1)⁻¹ : T) : T) ((f : (a : R) → T) 1 : T) = 1

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.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x y : OreLocalization S R
c :
  ∀ (r₁ : R) (s₁ : ↥S),
    liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁ * y) =
      HMul.hMul (α := T)
        (liftExpand
          (fun (r : R) (s : ↥S) ↦
            HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
          ⋯ (r₁ /ₒ s₁))
        (liftExpand
          (fun (r : R) (s : ↥S) ↦
            HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
          ⋯ y)
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (x * y) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ x)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ y)

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.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
y : OreLocalization S R
r₁ : R
s₁ : ↥S
c :
  ∀ (r₂ : R) (s₂ : ↥S),
    liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
      HMul.hMul (α := T)
        (liftExpand
          (fun (r : R) (s : ↥S) ↦
            HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
          ⋯ (r₁ /ₒ s₁))
        (liftExpand
          (fun (r : R) (s : ↥S) ↦
            HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
          ⋯ (r₂ /ₒ s₂))
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (r₁ /ₒ s₁ * y) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ y)

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.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
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₁)),
    liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
      HMul.hMul (α := T)
        (liftExpand
          (fun (r : R) (s : ↥S) ↦
            HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
          ⋯ (r₁ /ₒ s₁))
        (liftExpand
          (fun (r : R) (s : ↥S) ↦
            HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
          ⋯ (r₂ /ₒ s₂))
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))

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

Premises used: OreLocalization.oreDivMulChar'