awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * (↑s₁ : R) ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * (↑s₂ : R) ∈ S),
    P r₁ s₁ r₂ s₂ =
      P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (t₂ • r₂)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
r₁ : X
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * (↑s₂ : R) ∈ S
⊢ P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ • r₂) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
have this : P r₁ s₁ r₂ s₂ =
  P (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (1 * (↑s₁ : R)) sorry) (t₂ • r₂)
    (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
Tactic: have := hP r₁ 1 s₁ (by simp) r₂ t₂ s₂ ht₂
-- 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 → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * (↑s₁ : R) ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * (↑s₂ : R) ∈ S),
    P r₁ s₁ r₂ s₂ =
      P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (t₂ • r₂)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
⊢ Eq (α := OreLocalization S X → C)
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) r₁ s₁)
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) (t₁ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁))
have h : ∀ (x : OreLocalization S X),
  Eq.{u_2} (α := C) ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) sorry : OreLocalization S X → C)) r₁ s₁ x)
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) sorry : OreLocalization S X → C)) (t₁ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) x)
Tactic: ext 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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * (↑s₁ : R) ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * (↑s₂ : R) ∈ S),
    P r₁ s₁ r₂ s₂ =
      P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (t₂ • r₂)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
x : OreLocalization S X
⊢ Eq.{u_2} (α := C) ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) r₁ s₁ x)
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) ⋯ : OreLocalization S X → C)) (t₁ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) x)
have h : ∀ (r₂ : X) (s₂ : ↥S),
  Eq.{u_2} (α := C) ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) sorry : OreLocalization S X → C)) r₁ s₁ (r₂ /ₒ s₂))
    ((fun (r₁ : X) (s₁ : ↥S) ↦ (liftExpand (P r₁ s₁) sorry : OreLocalization S X → C)) (t₁ • r₁)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (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_3
inst_2 : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * (↑s₁ : R) ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * (↑s₂ : R) ∈ S),
    P r₁ s₁ r₂ s₂ =
      P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (t₂ • r₂)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₂ * (↑s₂ : R)) ht₂)
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * (↑s₁ : R) ∈ S
r₂ : X
s₂ : ↥S
⊢ liftExpand (P r₁ s₁) ⋯ (r₂ /ₒ s₂) =
    liftExpand (P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁)) ⋯ (r₂ /ₒ s₂)
have h : P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 r₂)
    (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (1 * (↑s₂ : R)) sorry) =
  P (t₁ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (t₁ * (↑s₁ : R)) ht₁) r₂ s₂
Tactic: rw [liftExpand_of, liftExpand_of, hP r₁ t₁ s₁ ht₁ r₂ 1 s₂ (by simp)]
-- 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)) (v • r₂ /ₒ (u * s₁))
have h₀ : (↑(oreDenom r₁ s₂) : R) * r₁ = oreNum r₁ s₂ * (↑s₂ : R)
Tactic: have h₀ := ore_eq r₁ 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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
h₀ : (↑(oreDenom r₁ s₂) : R) * r₁ = oreNum r₁ s₂ * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)) (v • r₂ /ₒ (u * s₁))
have set : let v₀ := oreNum r₁ s₂;
∀ (h₀ : (↑(oreDenom r₁ s₂) : R) * r₁ = v₀ * (↑s₂ : R)),
  Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)) (v • r₂ /ₒ (u * s₁))
Tactic: set v₀ := oreNum r₁ s₂
Cleared hypotheses: 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
h₀ : (↑(oreDenom r₁ s₂) : R) * r₁ = v₀ * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)) (v • r₂ /ₒ (u * s₁))
have set : let u₀ := oreDenom r₁ s₂;
∀ (h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)), Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
Tactic: set u₀ := oreDenom r₁ s₂
Cleared hypotheses: 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
have rcases : ∀ (r₃ : R) (s₃ : ↥S) (h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)),
  Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
Tactic: rcases oreCondition (u₀ : R) u 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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
⊢ r₃ * v * (↑s₂ : R) = r₃ * ((↑u : R) * r₁)
have rw : r₃ * (v * (↑s₂ : R)) = r₃ * ((↑u : R) * r₁)
Tactic: rw [mul_assoc, ← huv]
-- 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
rw : r₃ * (v * (↑s₂ : R)) = r₃ * ((↑u : R) * r₁)
⊢ r₃ * v * (↑s₂ : R) = r₃ * ((↑u : R) * r₁)
have rw₁ : r₃ * ((↑u : R) * r₁) = r₃ * ((↑u : R) * r₁)
Tactic: rw [mul_assoc, ← huv]
-- 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
⊢ r₃ * ((↑u : R) * r₁) = (↑s₃ : R) * ((↑u₀ : R) * r₁)
have rw : r₃ * (↑u : R) * r₁ = (↑s₃ : R) * ((↑u₀ : R) * r₁)
Tactic: rw [← mul_assoc, ← 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
rw : r₃ * (↑u : R) * r₁ = (↑s₃ : R) * ((↑u₀ : R) * r₁)
⊢ r₃ * ((↑u : R) * r₁) = (↑s₃ : R) * ((↑u₀ : R) * r₁)
have rw₁ : r₃ * (↑u : R) * r₁ = (↑s₃ : R) * (↑u₀ : R) * r₁
Tactic: rw [← mul_assoc, ← 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
rw : r₃ * (↑u : R) * r₁ = (↑s₃ : R) * ((↑u₀ : R) * r₁)
rw₁ : r₃ * (↑u : R) * r₁ = (↑s₃ : R) * (↑u₀ : R) * r₁
⊢ r₃ * ((↑u : R) * r₁) = (↑s₃ : R) * ((↑u₀ : R) * r₁)
have rw₂ : r₃ * (↑u : R) * r₁ = r₃ * (↑u : R) * r₁
Tactic: rw [← mul_assoc, ← 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
⊢ (↑s₃ : R) * ((↑u₀ : R) * r₁) = (↑s₃ : R) * v₀ * (↑s₂ : R)
have rw : (↑s₃ : R) * ((↑u₀ : R) * r₁) = (↑s₃ : R) * (v₀ * (↑s₂ : R))
Tactic: rw [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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
rw : (↑s₃ : R) * ((↑u₀ : R) * r₁) = (↑s₃ : R) * (v₀ * (↑s₂ : R))
⊢ (↑s₃ : R) * ((↑u₀ : R) * r₁) = (↑s₃ : R) * v₀ * (↑s₂ : R)
have rw₁ : (↑s₃ : R) * (v₀ * (↑s₂ : R)) = (↑s₃ : R) * (v₀ * (↑s₂ : R))
Tactic: rw [mul_assoc, 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
have this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
Tactic: have :=
    calc
      r₃ * v * s₂ = r₃ * (u * r₁) := by rw [mul_assoc, ← huv]
      _ = s₃ * (u₀ * r₁) := by rw [← mul_assoc, ← mul_assoc, h₃]
      _ = s₃ * v₀ * s₂ := by rw [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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
have rcases : ∀ (s₄ : ↥S) (hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)),
  Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
Tactic: rcases ore_right_cancel _ _ _ this with ⟨s₄, 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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ Eq (α := OreLocalization S X) (v₀ • r₂ /ₒ (u₀ * s₁)) (v • r₂ /ₒ (u * s₁))
have symm : Eq (α := OreLocalization S X) (v • r₂ /ₒ (u * s₁)) (v₀ • r₂ /ₒ (u₀ * 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ Eq (α := OreLocalization S X) (v • r₂ /ₒ (u * s₁)) (v₀ • r₂ /ₒ (u₀ * s₁))
have rw : ∃ (u_1 : ↥S), ∃ (v_1 : R), u_1 • v₀ • r₂ = v_1 • v • r₂ ∧ (↑u_1 : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)
Tactic: rw [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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ ∃ (u_1 : ↥S), ∃ (v_1 : R), u_1 • v₀ • r₂ = v_1 • v • r₂ ∧ (↑u_1 : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)
have h : ∃ (v_1 : R), (s₄ * s₃) • v₀ • r₂ = v_1 • v • r₂ ∧ (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)
Tactic: use s₄ * 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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ ∃ (v_1 : R), (s₄ * s₃) • v₀ • r₂ = v_1 • v • r₂ ∧ (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = v_1 * (↑(u * s₁) : R)
have h : (s₄ * s₃) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧ (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = (↑s₄ : R) * r₃ * (↑(u * s₁) : R)
Tactic: use s₄ * r₃
-- 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ (s₄ * s₃) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
    (↑(s₄ * s₃) : R) * (↑(u₀ * s₁) : R) = (↑s₄ : R) * r₃ * (↑(u * s₁) : R)
have h : ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
  (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
Tactic: simp only [Submonoid.coe_mul, 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₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
    (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
have h : ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂
Tactic: constructor
-- 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
h : ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂
⊢ ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂ ∧
    (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
have h₁ : (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
Tactic: constructor
-- 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
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ ((↑s₄ : R) * (↑s₃ : R)) • v₀ • r₂ = ((↑s₄ : R) * r₃) • v • r₂
have h : ((↑s₄ : R) * (r₃ * v)) • r₂ = ((↑s₄ : R) * r₃) • v • r₂
Tactic: rw [smul_smul, mul_assoc (c := v₀), ← 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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : (↑u : R) * r₁ = v * (↑s₂ : R)
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : (↑u₀ : R) * r₁ = v₀ * (↑s₂ : R)
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑u₀ : R) = r₃ * (↑u : R)
this : r₃ * v * (↑s₂ : R) = (↑s₃ : R) * v₀ * (↑s₂ : R)
s₄ : ↥S
hs₄ : (↑s₄ : R) * (r₃ * v) = (↑s₄ : R) * ((↑s₃ : R) * v₀)
⊢ (↑s₄ : R) * (↑s₃ : R) * ((↑u₀ : R) * (↑s₁ : R)) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
have h : (↑s₄ : R) * (r₃ * (↑u : R)) * (↑s₁ : R) = (↑s₄ : R) * r₃ * ((↑u : R) * (↑s₁ : R))
Tactic: rw [← mul_assoc (b := (u₀ : R)), mul_assoc (c := (u₀ : R)), 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
⊢ Eq (α := OreLocalization S X) (smul' r s r₁ s')
    (smul' r s (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs))
have rcases : ∀ (r₁' : R) (s₁' : ↥S) (h₁ : (↑s₁' : R) * r = r₁' * (↑s' : R)),
  Eq (α := OreLocalization S X) (smul' r s r₁ s')
    (smul' r s (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs))
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
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)
⊢ Eq (α := OreLocalization S X) (smul' r s r₁ s')
    (smul' r s (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs))
have rw : Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s))
  (smul' r s (r₂ • r₁) (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
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)
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s))
    (smul' r s (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs))
have rcases : ∀ (r₂' : R) (s₂' : ↥S) (h₂ : (↑s₂' : R) * r = r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)),
  Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s))
    (smul' r s (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs))
Tactic: rcases oreCondition r ⟨_, hs⟩ 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
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)
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s))
    (smul' r s (r₂ • r₁) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs))
have rw : Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * 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
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)
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
have rcases : ∀ (r₃' : R) (s₃' : ↥S) (h₃ : (↑s₃' : R) * (↑s₁' : R) = r₃' * (↑s₂' : R)),
  Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
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
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)
⊢ (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
have rw : r₃' * (r₂' * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (r₂ * (↑s' : R)) hs) : R)) = r₃' * r₂' * r₂ * (↑s' : R)
Tactic: rw [mul_assoc, ← h₁, ← mul_assoc, h₃, mul_assoc, 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)
⊢ Eq (α := OreLocalization S X) (r₁' • r₁ /ₒ (s₁' * s)) (r₂' • r₂ • r₁ /ₒ (s₂' * s))
have this : (↑s₃' : R) * r₁' * (↑s' : R) = r₃' * r₂' * r₂ * (↑s' : R)
Tactic: have : s₃' * r₁' * s' = (r₃' * r₂' * r₂) * s' := by
      rw [mul_assoc, ← h₁, ← mul_assoc, h₃, mul_assoc, h₂]
      simp [mul_assoc]