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
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)
this : (↑s₃' : R) * 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 c : ∀ (s₄' : ↥S) (h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * 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 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
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)
this : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
⊢ (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
have rw : (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * (r₂ * (↑s : R)) ∈ S
Tactic: rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, 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)
this : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * 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) * (↑s : R)) ∈ S
Tactic: have : (s₄' * r₃') * (s₁' * s) ∈ S := by
      rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]
      exact mul_mem (s₄' * s₃' * s₂').2 hs
-- 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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
⊢ 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 : Eq (α := OreLocalization S X)
  (((↑s₄' : R) * r₃') • r₁' • x /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₁' * s) : R)) this)
  ((s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs)))
Tactic: rw [OreLocalization.expand' (r₂' • x) _ (s₄' * s₃'), OreLocalization.expand _ _ _ 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
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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
⊢ Eq (α := OreLocalization S X)
    (((↑s₄' : R) * r₃') • r₁' • x /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * r₃' * (↑(s₁' * s) : R)) this)
    ((s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs)))
have c : Eq (α := OreLocalization S X)
  (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ
    Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) sorry)
  (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ (s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))))
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
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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
⊢ Eq (α := OreLocalization S X)
    (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯)
    (((↑s₄' : R) * (r₃' * r₁')) • x /ₒ (s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))))
have c : Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) sorry =
  s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
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
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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯ =
    s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))
have c : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) sorry) : R) =
  (↑(s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))) : 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
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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑s₄' : R) * (r₃' * ((↑s₁' : R) * (↑s : R)))) ⋯) : R) =
    (↑(s₄' * (s₃' * (s₂' * Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s : R)) hs))) : R)
have c : (↑s₄' : R) * r₃' * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * 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
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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
⊢ (↑s₄' : R) * r₃' * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
have c : (↑s₄' : R) * (r₃' * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
Tactic: rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← 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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c : (↑s₄' : R) * (r₃' * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
⊢ (↑s₄' : R) * r₃' * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
have c₁ : (↑s₄' : R) * ((↑s₃' : R) * ((↑s₂' : R) * r₂)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
Tactic: rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← 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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c : (↑s₄' : R) * (r₃' * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
c₁ : (↑s₄' : R) * ((↑s₃' : R) * ((↑s₂' : R) * r₂)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
⊢ (↑s₄' : R) * r₃' * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
have c₂ : (↑s₄' : R) * (↑s₃' : R) * ((↑s₂' : R) * r₂) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
Tactic: rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← 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)
this_1 : (↑s₃' : R) * r₂' * (↑s₂ : R) = r₃' * r₁' * (↑s₂ : R)
s₄' : ↥S
h₄ : (↑s₄' : R) * ((↑s₃' : R) * r₂') = (↑s₄' : R) * (r₃' * r₁')
this : (↑s₄' : R) * r₃' * ((↑s₁' : R) * (↑s : R)) ∈ S
c : (↑s₄' : R) * (r₃' * (↑s₁' : R)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
c₁ : (↑s₄' : R) * ((↑s₃' : R) * ((↑s₂' : R) * r₂)) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
c₂ : (↑s₄' : R) * (↑s₃' : R) * ((↑s₂' : R) * r₂) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
⊢ (↑s₄' : R) * r₃' * (↑s₁' : R) * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
have c₃ : (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R) = (↑s₄' : R) * (↑s₃' : R) * (↑s₂' : R) * r₂ * (↑s : R)
Tactic: rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← 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
r : R
hr : r ∈ S
⊢ Eq (α := OreLocalization S R) (r /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) 1
have rw : ∃ (u : ↥S),
  ∃ (v : R),
    HSMul.hSMul (β := R) u 1 = v • r ∧ (↑u : R) * (↑1 : R) = v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) : R)
Tactic: rw [OreLocalization.one_def, oreDiv_eq_iff]
-- 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
x : OreLocalization S X
⊢ HSMul.hSMul (α := OreLocalization S R) 1 x = x
have c : ∀ (r : X) (s : ↥S), HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) 1 (r /ₒ s) = r /ₒ s
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 : OreLocalization S R
⊢ x * 1 = x
have c : ∀ (r : R) (s : ↥S), HMul.hMul (α := OreLocalization S R) (r /ₒ s) 1 = r /ₒ s
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_2
inst_2 : MulAction R X
x y : OreLocalization S R
z : OreLocalization S X
⊢ (x * y) • z = x • y • z
have c : ∀ (r₁ : R) (s₁ : ↥S), (r₁ /ₒ s₁ * y) • z = HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (y • z)
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_2
inst_2 : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
⊢ (r₁ /ₒ s₁ * y) • z = HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (y • z)
have c : ∀ (r₂ : R) (s₂ : ↥S),
  HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) • z =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (HSMul.hSMul (α := OreLocalization S R) (r₂ /ₒ s₂) z)
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_2
inst_2 : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) • z =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁) (HSMul.hSMul (α := OreLocalization S R) (r₂ /ₒ s₂) z)
have c : ∀ (r₃ : X) (s₃ : ↥S),
  HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
Tactic: cases z with | _ r₃ s₃
Cleared hypotheses: z
-- 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
⊢ HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (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₁)),
  HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (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_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)
ha' : HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ HSMul.hSMul (β := OreLocalization S X) (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
  HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
    (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
Tactic: rw [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_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)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
have c : ∀ (rb : R) (sb : ↥S) (hb : (↑sb : R) * r₂ = rb * (↑s₃ : R))
  (hb' :
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)),
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
Tactic: rcases oreDivSMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩
-- 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)
hb' : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (r₁ /ₒ s₁)
      (HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃))
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
Tactic: rw [hb']
-- 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)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
have c : ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * ra = rc * (↑sb : R)),
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
Tactic: rcases oreCondition ra sb with ⟨rc, sc, hc⟩
-- 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) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ 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 [oreDiv_smul_char (ra * r₂) r₃ (sa * s₁) s₃ (rc * rb) sc]
-- 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 :
  (rc * rb) • r₃ /ₒ (sc * (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (ra * r₂ /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₁ /ₒ s₁) (rb • r₃ /ₒ (sb * s₂))
have c₁ : (↑sc : R) * (ra * r₂) = rc * rb * (↑s₃ : R)
Tactic: rw [oreDiv_smul_char (ra * r₂) r₃ (sa * s₁) s₃ (rc * rb) sc]
-- 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 : R) * (ra * r₂) = rc * rb * (↑s₃ : R)
have c : (↑sc : R) * ra * 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)
c : (↑sc : R) * ra * r₂ = rc * rb * (↑s₃ : R)
⊢ (↑sc : R) * (ra * r₂) = rc * rb * (↑s₃ : R)
have c₁ : rc * (↑sb : R) * 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)
c : (↑sc : R) * ra * r₂ = rc * rb * (↑s₃ : R)
c₁ : rc * (↑sb : R) * r₂ = rc * rb * (↑s₃ : R)
⊢ (↑sc : R) * (ra * r₂) = rc * rb * (↑s₃ : R)
have c₂ : rc * ((↑sb : R) * 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)
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)
⊢ (↑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]