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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) • v' • r₂ = r' • v • r₁
refine_2₁ : ((↑s' : R) * v') • r₂ = r' • v • r₁
⊢ (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁
have refine_2₂ : (r' * (↑u : R)) • r₂ = r' • v • r₁
Tactic: rw [hur₂, smul_smul, h, mul_smul, hur₁]
-- 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) • v' • r₂ = r' • v • r₁
refine_2₁ : ((↑s' : R) * v') • r₂ = r' • v • r₁
refine_2₂ : (r' * (↑u : R)) • r₂ = r' • v • r₁
⊢ (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁
have refine_2₃ : r' • (↑u : R) • r₂ = r' • v • r₁
Tactic: rw [hur₂, smul_smul, h, mul_smul, hur₁]
-- 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) • v' • r₂ = r' • v • r₁
refine_2₁ : ((↑s' : R) * v') • r₂ = r' • v • r₁
refine_2₂ : (r' * (↑u : R)) • r₂ = r' • v • r₁
refine_2₃ : r' • (↑u : R) • r₂ = r' • v • r₁
⊢ (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁
have refine_2₄ : r' • v • r₁ = r' • v • r₁
Tactic: rw [hur₂, smul_smul, h, mul_smul, hur₁]
-- 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
⊢ (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))
have refine_2 : (↑s' : R) * (v' * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
Tactic: rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]
-- 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) * (v' * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
⊢ (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))
have refine_2₁ : (↑s' : R) * v' * (↑s₂ : R) = r' * (v * (↑s₁ : R))
Tactic: rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]
-- 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) * (v' * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
refine_2₁ : (↑s' : R) * v' * (↑s₂ : R) = r' * (v * (↑s₁ : R))
⊢ (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))
have refine_2₂ : r' * (↑u : R) * (↑s₂ : R) = r' * (v * (↑s₁ : R))
Tactic: rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]
-- 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) * (v' * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
refine_2₁ : (↑s' : R) * v' * (↑s₂ : R) = r' * (v * (↑s₁ : R))
refine_2₂ : r' * (↑u : R) * (↑s₂ : R) = r' * (v * (↑s₁ : R))
⊢ (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))
have refine_2₃ : r' * ((↑u : R) * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
Tactic: rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]
-- 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₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) * (v' * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
refine_2₁ : (↑s' : R) * v' * (↑s₂ : R) = r' * (v * (↑s₁ : R))
refine_2₂ : r' * (↑u : R) * (↑s₂ : R) = r' * (v * (↑s₁ : R))
refine_2₃ : r' * ((↑u : R) * (↑s₂ : R)) = r' * (v * (↑s₁ : R))
⊢ (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))
have refine_2₄ : r' * (v * (↑s₁ : R)) = r' * (v * (↑s₁ : R))
Tactic: rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]
-- 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
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
⊢ ∀ (q : OreLocalization S X), β q
have a : ∀ (a : Prod.{u_2, u_1} X ↥S), β ⟦a⟧
Tactic: apply Quotient.ind
-- 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 : X
s : ↥S
t : R
hst : t * (↑s : R) ∈ S
⊢ Eq (α := OreLocalization S X) (r /ₒ s) (t • r /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst)
have a : (r, s) ≈ (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst)
Tactic: apply Quotient.sound
-- 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 : X
s : ↥S
t : R
hst : t * (↑s : R) ∈ S
⊢ s • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = ((↑s : R) * t) • (r, s).fst
have rw : s • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = (↑s : R) • t • (r, s).fst
Tactic: rw [mul_smul, Submonoid.smul_def]
-- 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 : X
s : ↥S
t : R
hst : t * (↑s : R) ∈ S
rw : s • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = (↑s : R) • t • (r, s).fst
⊢ s • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = ((↑s : R) * t) • (r, s).fst
have rw₁ : (↑s : R) • (t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).fst = (↑s : R) • t • (r, s).fst
Tactic: rw [mul_smul, Submonoid.smul_def]
-- 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 : X
s : ↥S
t : R
hst : t * (↑s : R) ∈ S
⊢ (↑s : R) * (↑(t • r, Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) hst).snd : R) =
    (↑s : R) * t * (↑(r, s).snd : R)
have rw : (↑s : R) * t * (↑s : R) = (↑s : R) * t * (↑(r, s).snd : R)
Tactic: rw [← 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 : X
s s' : ↥S
⊢ (↑s' : R) * (↑s : R) ∈ S
have norm_cast : (↑(s' * s) : R) ∈ S
Tactic: norm_cast
-- 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
⊢ Eq (α := OreLocalization S R) (r₁ * r * r₂ /ₒ s) (r₁ * r' * r₂ /ₒ s)
have rcases : ∀ (r₁' : R) (t' : ↥S) (hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)),
  Eq (α := OreLocalization S R) (r₁ * r * r₂ /ₒ s) (r₁ * r' * r₂ /ₒ s)
Tactic: rcases oreCondition r₁ t with ⟨r₁', t', hr₁⟩
-- 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ Eq (α := OreLocalization S R) (r₁ * r * r₂ /ₒ s) (r₁ * r' * r₂ /ₒ s)
have rw : Eq (α := OreLocalization S R) (t' • (r₁ * r * r₂) /ₒ (t' * s)) (t' • (r₁ * r' * r₂) /ₒ (t' * s))
Tactic: rw [OreLocalization.expand' _ s t', OreLocalization.expand' _ s t']
-- 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ Eq (α := OreLocalization S R) (t' • (r₁ * r * r₂) /ₒ (t' * s)) (t' • (r₁ * r' * r₂) /ₒ (t' * s))
have e_r : t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
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
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
have rw : r₁' * (↑t : R) * r * r₂ = r₁' * (↑t : R) * r * r₂
Tactic: rw [hr₁]
-- 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ r₁' * ((↑t : R) * r) * r₂ = r₁' * ((↑t : R) * r') * r₂
have rw : r₁' * ((↑t : R) * r') * r₂ = r₁' * ((↑t : R) * r') * r₂
Tactic: rw [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
r r' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ r₁' * (↑t : R) * r' * r₂ = (↑t' : R) * r₁ * r' * r₂
have rw : r₁' * (↑t : R) * r' * r₂ = r₁' * (↑t : R) * r' * r₂
Tactic: rw [hr₁]
-- 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
have calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
Tactic: calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
have calc₁ : (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
Tactic: calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
calc₁ : (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
have calc₂ : r₁' * (↑t : R) * r * r₂ = r₁' * ((↑t : R) * r) * r₂
Tactic: calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
calc₁ : (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
calc₂ : r₁' * (↑t : R) * r * r₂ = r₁' * ((↑t : R) * r) * r₂
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
have calc₃ : r₁' * ((↑t : R) * r) * r₂ = r₁' * ((↑t : R) * r') * r₂
Tactic: calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
calc₁ : (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
calc₂ : r₁' * (↑t : R) * r * r₂ = r₁' * ((↑t : R) * r) * r₂
calc₃ : r₁' * ((↑t : R) * r) * r₂ = r₁' * ((↑t : R) * r') * r₂
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
have calc₄ : r₁' * ((↑t : R) * r') * r₂ = r₁' * (↑t : R) * r' * r₂
Tactic: calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
calc₁ : (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
calc₂ : r₁' * (↑t : R) * r * r₂ = r₁' * ((↑t : R) * r) * r₂
calc₃ : r₁' * ((↑t : R) * r) * r₂ = r₁' * ((↑t : R) * r') * r₂
calc₄ : r₁' * ((↑t : R) * r') * r₂ = r₁' * (↑t : R) * r' * r₂
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
have calc₅ : r₁' * (↑t : R) * r' * r₂ = (↑t' : R) * r₁ * r' * r₂
Tactic: calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← 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' r₁ r₂ : R
s t : ↥S
h : (↑t : R) * r = (↑t : R) * r'
r₁' : R
t' : ↥S
hr₁ : (↑t' : R) * r₁ = r₁' * (↑t : R)
calc : (↑t' : R) * (r₁ * r * r₂) = (↑t' : R) * r₁ * r * r₂
calc₁ : (↑t' : R) * r₁ * r * r₂ = r₁' * (↑t : R) * r * r₂
calc₂ : r₁' * (↑t : R) * r * r₂ = r₁' * ((↑t : R) * r) * r₂
calc₃ : r₁' * ((↑t : R) * r) * r₂ = r₁' * ((↑t : R) * r') * r₂
calc₄ : r₁' * ((↑t : R) * r') * r₂ = r₁' * (↑t : R) * r' * r₂
calc₅ : r₁' * (↑t : R) * r' * r₂ = (↑t' : R) * r₁ * r' * r₂
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
have calc₆ : (↑t' : R) * r₁ * r' * r₂ = (↑t' : R) * (r₁ * r' * r₂)
Tactic: calc (t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₂ : (↑u : R) * (↑(r₂, s₂).snd : R) = v * (↑(r₁, s₁).snd : R)
⊢ Eq.{u_2} (α := C) ((fun (p : Prod.{u_3, u_1} X ↥S) ↦ P p.fst p.snd) (r₁, s₁))
    ((fun (p : Prod.{u_3, u_1} X ↥S) ↦ P p.fst p.snd) (r₂, s₂))
have dsimp : P r₁ s₁ = P r₂ s₂
Tactic: dsimp at *
-- 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
⊢ v * (↑s₁ : R) ∈ S
have rw : (↑(u * s₂) : R) ∈ S
Tactic: rw [← hs₂, ← S.coe_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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
⊢ P r₁ s₁ = P r₂ s₂
have s₁vS : v * (↑s₁ : R) ∈ S
Tactic: have s₁vS : v * s₁ ∈ S := by
      rw [← hs₂, ← S.coe_mul]
      exact SetLike.coe_mem (u * 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
s₁vS : v * (↑s₁ : R) ∈ S
⊢ u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
have a : (↑(u * s₂) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) : R)
Tactic: ext
-- 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
s₁vS : v * (↑s₁ : R) ∈ S
⊢ P r₁ s₁ = P r₂ s₂
have hs₃ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
Tactic: replace hs₂ : u * s₂ = ⟨_, s₁vS⟩ := by ext; simp [hs₂]
Cleared hypotheses: 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
⊢ (↑u : R) * (↑s₂ : R) ∈ S
have norm_cast : (↑(u * s₂) : R) ∈ S
Tactic: norm_cast
-- 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
⊢ (↑(u * s₂) : R) ∈ S
have rwa : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) : R) ∈ S
Tactic: rwa [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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
⊢ P r₁ s₁ = P r₂ s₂
have rw : P (u • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) =
  P ((↑u : R) • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑u : R) * (↑s₂ : R)) sorry)
Tactic: rw [hP r₁ v s₁ s₁vS, hP r₂ u s₂ (by norm_cast; rwa [hs₂]), ← hr₂]
-- 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP :
  ∀ (r : X) (t : R) (s : ↥S) (ht : t * (↑s : R) ∈ S),
    P r s = P (t • r) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t * (↑s : R)) ht)
x x_1 : Prod.{u_3, u_1} X ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
h : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * (↑s₁ : R) ∈ S
hs₂ : u * s₂ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS
⊢ P (u • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (v * (↑s₁ : R)) s₁vS) =
    P ((↑u : R) • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑u : R) * (↑s₂ : R)) ⋯)
have simp : P (u • r₂) (u * s₂) = P ((↑u : R) • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑u : R) * (↑s₂ : R)) sorry)
Tactic: simp only [← hs₂]