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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
have rcases : ∀ (s₄' : ↥S) (h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)),
  Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
Tactic: rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
⊢ (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
have rw : (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R) * (↑s : R)) ∈ S
Tactic: rw [mul_assoc, ← mul_assoc r₃', ← h₃]
-- 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_2
inst_2 : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
have this₁ : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
Tactic: have : (s₄' * r₃') * (s₂' * s) ∈ S := by
      rw [mul_assoc, ← mul_assoc r₃', ← h₃]
      exact (s₄' * (s₃' * s₁' * s)).2
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
have rw : Eq (α := OreLocalization S X) ((s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)))
  (((↑s₄' : R) * r₃') • r₂' • r₂ • r₁ /ₒ
    Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₂' * s) : R)) this)
Tactic: rw [OreLocalization.expand' _ _ (s₄' * s₃'), OreLocalization.expand _ (s₂' * s) _ this]
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
⊢ Eq (α := OreLocalization S X) ((s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)))
    (((↑s₄' : R) * r₃') • r₂' • r₂ • r₁ /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₂' * s) : R)) this)
have simp : Eq (α := OreLocalization S X) (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ (s₄' * (s₃' * (s₁' * s))))
  (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ
    Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) sorry)
Tactic: simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
⊢ Eq (α := OreLocalization S X) (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ (s₄' * (s₃' * (s₁' * s))))
    (((↑s₄' : R) * (r₃' * (r₂' * r₂))) • r₁ /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯)
have e_s : s₄' * (s₃' * (s₁' * s)) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) sorry
Tactic: congr 1
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
⊢ s₄' * (s₃' * (s₁' * s)) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯
have e_s : (↑(s₄' * (s₃' * (s₁' * s))) : R) =
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) sorry) : R)
Tactic: ext
-- 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
⊢ (↑(s₄' * (s₃' * (s₁' * s))) : R) =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₂' : R) * (↑s : R)))) ⋯) : R)
have e_s : (↑s₄' : R) * (↑s₃' : R) * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
Tactic: simp only [Submonoid.coe_mul, ← 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
⊢ (↑s₄' : R) * (↑s₃' : R) * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
have e_s : (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
Tactic: rw [mul_assoc (s₄' : R), h₃, ← 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
e_s : (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
⊢ (↑s₄' : R) * (↑s₃' : R) * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
have e_s₁ : (↑s₄' : R) * (r₃' * (↑s₂' : R)) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
Tactic: rw [mul_assoc (s₄' : R), h₃, ← 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₁ : X
r₂ : R
s' : ↥S
hs : r₂ * (↑s' : R) ∈ S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)
this_1 : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₁') = (↑s₄' : R) * (r₃' * r₂' * r₂)
this : (↑s₄' : R) * r₃' * ((↑s₂' : R) * (↑s : R)) ∈ S
e_s : (↑s₄' : R) * ((↑s₃' : R) * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
e_s₁ : (↑s₄' : R) * (r₃' * (↑s₂' : R)) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
⊢ (↑s₄' : R) * (↑s₃' : R) * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
have e_s₂ : (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R) = (↑s₄' : R) * r₃' * (↑s₂' : R) * (↑s : R)
Tactic: rw [mul_assoc (s₄' : R), h₃, ← 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
y : OreLocalization S R
x : OreLocalization S X
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
⊢ Eq (α := OreLocalization S X) ((fun (x1 : R) (x2 : ↥S) ↦ smul'' x1 x2 x) r₁ s)
    ((fun (x1 : R) (x2 : ↥S) ↦ smul'' x1 x2 x) (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
have c : ∀ (x : X) (s₂ : ↥S),
  Eq (α := OreLocalization S X) ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) r₁ s)
    ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) (r₂ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
Tactic: cases x with | _ x 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_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
⊢ Eq (α := OreLocalization S X) ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) r₁ s)
    ((fun (x1 : R) (x2 : ↥S) ↦ (smul'' x1 x2 (x /ₒ s₂) : OreLocalization S X)) (r₂ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
have c : Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
  (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
Tactic: change OreLocalization.smul' r₁ s x s₂ = OreLocalization.smul' (r₂ * r₁) ⟨_, hs⟩ x 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_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
⊢ Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
have c : ∀ (r₁' : R) (s₁' : ↥S) (h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)),
  Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
Tactic: rcases oreCondition r₁ s₂ with ⟨r₁', s₁', h₁⟩
-- 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (smul' r₁ s x s₂)
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
have c : Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
  (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
Tactic: rw [smul'_char _ _ _ _ _ _ h₁]
-- 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
have c : ∀ (r₂' : R) (s₂' : ↥S) (h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)),
  Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
Tactic: rcases oreCondition (r₂ * r₁) s₂ with ⟨r₂', s₂', h₂⟩
-- 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (smul' (r₂ * r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs) x s₂)
have c : Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
  (r₂' • x /ₒ (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
Tactic: rw [smul'_char _ _ _ _ _ _ h₂]
-- 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (r₂' • x /ₒ (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
have c : ∀ (r₃' : R) (s₃' : ↥S) (h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)),
  Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (r₂' • x /ₒ (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
Tactic: rcases oreCondition (s₂' * r₂) (s₁') with ⟨r₃', s₃', h₃⟩
-- 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, mul_assoc]
-- 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw₂ : (↑s₃' : R) * ((↑s₂' : R) * r₂ * r₁) = r₃' * r₁' * (↑s₂ : R)
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
rw₂ : (↑s₃' : R) * ((↑s₂' : R) * r₂ * r₁) = r₃' * r₁' * (↑s₂ : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) * r₁ = r₃' * r₁' * (↑s₂ : R)
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
rw₂ : (↑s₃' : R) * ((↑s₂' : R) * r₂ * r₁) = r₃' * r₁' * (↑s₂ : R)
rw₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) * r₁ = r₃' * r₁' * (↑s₂ : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw₄ : r₃' * (↑s₁' : R) * r₁ = r₃' * r₁' * (↑s₂ : R)
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
rw₂ : (↑s₃' : R) * ((↑s₂' : R) * r₂ * r₁) = r₃' * r₁' * (↑s₂ : R)
rw₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) * r₁ = r₃' * r₁' * (↑s₂ : R)
rw₄ : r₃' * (↑s₁' : R) * r₁ = r₃' * r₁' * (↑s₂ : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw₅ : r₃' * ((↑s₁' : R) * r₁) = r₃' * r₁' * (↑s₂ : R)
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
rw₂ : (↑s₃' : R) * ((↑s₂' : R) * r₂ * r₁) = r₃' * r₁' * (↑s₂ : R)
rw₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) * r₁ = r₃' * r₁' * (↑s₂ : R)
rw₄ : r₃' * (↑s₁' : R) * r₁ = r₃' * r₁' * (↑s₂ : R)
rw₅ : r₃' * ((↑s₁' : R) * r₁) = r₃' * r₁' * (↑s₂ : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw₆ : r₃' * (r₁' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, 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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
rw : (↑s₃' : R) * (r₂' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
rw₁ : (↑s₃' : R) * ((↑s₂' : R) * (r₂ * r₁)) = r₃' * r₁' * (↑s₂ : R)
rw₂ : (↑s₃' : R) * ((↑s₂' : R) * r₂ * r₁) = r₃' * r₁' * (↑s₂ : R)
rw₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) * r₁ = r₃' * r₁' * (↑s₂ : R)
rw₄ : r₃' * (↑s₁' : R) * r₁ = r₃' * r₁' * (↑s₂ : R)
rw₅ : r₃' * ((↑s₁' : R) * r₁) = r₃' * r₁' * (↑s₂ : R)
rw₆ : r₃' * (r₁' * (↑s₂ : R)) = r₃' * r₁' * (↑s₂ : R)
⊢ (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
have rw₇ : r₃' * (r₁' * (↑s₂ : R)) = r₃' * (r₁' * (↑s₂ : R))
Tactic: rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, mul_assoc]
-- 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_2
inst_2 : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * (↑s : R) ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : (↑s₁' : R) * r₁ = r₁' * (↑s₂ : R)
r₂' : R
s₂' : ↥S
h₂ : (↑s₂' : R) * (r₂ * r₁) = r₂' * (↑s₂ : R)
r₃' : R
s₃' : ↥S
h₃ : (↑s₃' : R) * ((↑s₂' : R) * r₂) = r₃' * (↑s₁' : R)
⊢ Eq (α := OreLocalization S X) (r₁' • x /ₒ (s₁' * s))
    (r₂' • x /ₒ (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
have this : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
Tactic: have : s₃' * r₂' * s₂ = r₃' * r₁' * s₂ := by
      rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, mul_assoc]