awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * r₂ = rb * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ra = rc * (↑sb : R)
c : (↑sc : R) * ra * r₂ = rc * rb * (↑s₃ : R)
c₁ : rc * (↑sb : R) * r₂ = rc * rb * (↑s₃ : R)
c₂ : rc * ((↑sb : R) * r₂) = rc * rb * (↑s₃ : R)
c₃ : rc * (rb * (↑s₃ : R)) = rc * rb * (↑s₃ : R)
⊢ (↑sc : R) * (ra * r₂) = rc * rb * (↑s₃ : R)
have c₄ : rc * rb * (↑s₃ : R) = rc * rb * (↑s₃ : R)
Tactic: rw [← mul_assoc _ ra, hc, mul_assoc, hb, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ (rc * rb) • r₃ /ₒ (sc * (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
have c : rc • rb • r₃ /ₒ (sc * sa * s₁) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
Tactic: rw [← mul_assoc, mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ rc • rb • r₃ /ₒ (sc * sa * s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂)) =
  rc • rb • r₃ /ₒ (sc * sa * s₁)
Tactic: symm
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂)) =
    rc • rb • r₃ /ₒ (sc * sa * s₁)
have c : (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
Tactic: apply oreDiv_smul_char
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
have c : (↑sc : R) * (↑sa : R) * r₁ = rc * (↑(sb * s₂) : R)
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
have c₁ : (↑sc : R) * (↑sa : R) * r₁ = rc * ((↑sb : R) * (↑s₂ : R))
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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))
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
have c₂ : (↑sc : R) * (↑sa : R) * r₁ = rc * (↑sb : R) * (↑s₂ : R)
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
have c₃ : (↑sc : R) * (↑sa : R) * r₁ = (↑sc : R) * ra * (↑s₂ : R)
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
have c₄ : (↑sc : R) * (↑sa : R) * r₁ = (↑sc : R) * (ra * (↑s₂ : R))
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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))
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
have c₅ : (↑sc : R) * (↑sa : R) * r₁ = (↑sc : R) * ((↑sa : R) * r₁)
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₁)
⊢ (↑(sc * sa) : R) * r₁ = rc * (↑(sb * s₂) : R)
have c₆ : (↑sc : R) * ((↑sa : R) * r₁) = (↑sc : R) * ((↑sa : R) * r₁)
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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
⊢ 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))
have 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)
Tactic: simp only [smul_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (hypothesis)
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
⊢ 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)
have 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)
Tactic: have : (fS ⟨t * s, ht⟩ : T) = f t * fS s := by
        simp only [← hf, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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ˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) : T)
    ((f : (a : R) → T) (t * r) : T)
have 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))
Tactic: rw [map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
| (↑((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))
have 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)
Tactic: rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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ˣ) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht))⁻¹ : T) : T)
    ((f : (a : R) → T) (t * r) : T)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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) (β := 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ 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
have rw : HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) 1)⁻¹ : T) : T) ((f : (a : R) → T) 1 : T) = 1
Tactic: rw [OreLocalization.one_def, liftExpand_of]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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
⊢ 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)
have 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))
      sorry (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))
        sorry (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))
        sorry y)
Tactic: cases x with | _ r₁ s₁
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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
⊢ 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)
have 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))
      sorry (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))
        sorry (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))
        sorry (r₂ /ₒ s₂))
Tactic: cases y with | _ r₂ s₂
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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
⊢ 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₂))
have 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))
      sorry (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))
        sorry (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))
        sorry (r₂ /ₒ s₂))
Tactic: rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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
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₂))
have c : liftExpand
    (fun (r : R) (s : ↥S) ↦
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
    sorry (ra * r₂ /ₒ (sa * 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))
      sorry (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))
      sorry (r₂ /ₒ s₂))
Tactic: rw [ha']