awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
⊢ (sd * sc) • (sb • r₁ + rb • r₂) = ((↑sd : R) * rc) • (sa • r₁ + ra • r₂) ∧
    (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) =
      (↑sd : R) * rc * (↑(sa * s₁) : R)
have h₁ : ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂ ∧
  (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
Tactic: simp only [smul_add, smul_smul, Submonoid.smul_def, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
      ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂ ∧
    (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
have h₁ : ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
  ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
      ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂ ∧
    (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
have h₂ : (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
have h₁ : ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * ((↑sc : R) * rb)) • r₂ =
  ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
Tactic: rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * ((↑sc : R) * rb)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
have h₂ : ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
  ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
Tactic: rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * ((↑sc : R) * rb)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₂ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
have h₃ : ((↑sd : R) * ((↑sc : R) * sb)) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
  ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
Tactic: rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * ((↑sc : R) * rb)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₂ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₃ :
  ((↑sd : R) * ((↑sc : R) * sb)) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
have h₄ : ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
  ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
Tactic: rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * ((↑sc : R) * rb)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₂ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₃ :
  ((↑sd : R) * ((↑sc : R) * sb)) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₄ :
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
have h₅ : ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * rc * ra) • r₂
Tactic: rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * ((↑sc : R) * rb)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₂ :
  ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₃ :
  ((↑sd : R) * ((↑sc : R) * sb)) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₄ :
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
h₅ :
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
    ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * rc * ra) • r₂
⊢ ((↑sd : R) * (↑sc : R) * sb) • r₁ + ((↑sd : R) * (↑sc : R) * rb) • r₂ =
    ((↑sd : R) * rc * (↑sa : R)) • r₁ + ((↑sd : R) * rc * ra) • r₂
have h₆ : ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂ =
  ((↑sd : R) * (rc * (↑sa : R))) • r₁ + ((↑sd : R) * (rc * ra)) • r₂
Tactic: rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
⊢ (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
have h₁ : (↑sd : R) * ((↑sc : R) * (sb * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
Tactic: rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ : (↑sd : R) * ((↑sc : R) * (sb * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
⊢ (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
have h₂ : (↑sd : R) * ((↑sc : R) * sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
Tactic: rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ : (↑sd : R) * ((↑sc : R) * (sb * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₂ : (↑sd : R) * ((↑sc : R) * sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
⊢ (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
have h₃ : (↑sd : R) * (rc * (↑sa : R) * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
Tactic: rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ : (↑sd : R) * ((↑sc : R) * (sb * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₂ : (↑sd : R) * ((↑sc : R) * sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₃ : (↑sd : R) * (rc * (↑sa : R) * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
⊢ (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
have h₄ : (↑sd : R) * (rc * ((↑sa : R) * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
Tactic: rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
h₁ : (↑sd : R) * ((↑sc : R) * (sb * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₂ : (↑sd : R) * ((↑sc : R) * sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₃ : (↑sd : R) * (rc * (↑sa : R) * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
h₄ : (↑sd : R) * (rc * ((↑sa : R) * (↑s₁ : R))) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
⊢ (↑sd : R) * (↑sc : R) * (sb * (↑s₁ : R)) = (↑sd : R) * rc * ((↑sa : R) * (↑s₁ : R))
have h₅ : (↑sd : R) * (rc * ((↑sa : R) * (↑s₁ : R))) = (↑sd : R) * (rc * ((↑sa : R) * (↑s₁ : R)))
Tactic: rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • (r₁, s₁).fst = rb • (r₁', s₁').fst
hb' : (↑sb : R) * (↑(r₁, s₁).snd : R) = rb * (↑(r₁', s₁').snd : R)
⊢ Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)
have rcases : ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)),
  Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)
Tactic: rcases oreCondition (s₁' : R) s₂ with ⟨rc, sc, hc⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • (r₁, s₁).fst = rb • (r₁', s₁').fst
hb' : (↑sb : R) * (↑(r₁, s₁).snd : R) = rb * (↑(r₁', s₁').snd : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)
have rcases : ∀ (rd : R) (sd : ↥S) (hd : (↑sd : R) * rb = rd * (↑sc : R)),
  Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)
Tactic: rcases oreCondition rb sc with ⟨rd, sd, hd⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • (r₁, s₁).fst = rb • (r₁', s₁').fst
hb' : (↑sb : R) * (↑(r₁, s₁).snd : R) = rb * (↑(r₁', s₁').snd : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
⊢ Eq (α := OreLocalization S X) (add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂) (add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂)
have dsimp : Eq (α := OreLocalization S X) (add'' r₁' s₁' r₂ s₂) (add'' r₁ s₁ r₂ s₂)
Tactic: dsimp at *
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
⊢ Eq (α := OreLocalization S X) (add'' r₁' s₁' r₂ s₂) (add'' r₁ s₁ r₂ s₂)
have rw : Eq (α := OreLocalization S X)
  (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) sorry) (add'' r₁ s₁ r₂ s₂)
Tactic: rw [add''_char _ _ _ _ rc sc hc (sc * s₁').2]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
have rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
Tactic: rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
have rw₁ : (↑sd : R) * (rb * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
Tactic: rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
rw₁ : (↑sd : R) * (rb * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
have rw₂ : (↑sd : R) * rb * (↑s₁' : R) = rd * rc * (↑s₂ : R)
Tactic: rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
rw₁ : (↑sd : R) * (rb * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
rw₂ : (↑sd : R) * rb * (↑s₁' : R) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
have rw₃ : rd * (↑sc : R) * (↑s₁' : R) = rd * rc * (↑s₂ : R)
Tactic: rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
rw₁ : (↑sd : R) * (rb * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
rw₂ : (↑sd : R) * rb * (↑s₁' : R) = rd * rc * (↑s₂ : R)
rw₃ : rd * (↑sc : R) * (↑s₁' : R) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
have rw₄ : rd * ((↑sc : R) * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
Tactic: rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
rw₁ : (↑sd : R) * (rb * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
rw₂ : (↑sd : R) * rb * (↑s₁' : R) = rd * rc * (↑s₂ : R)
rw₃ : rd * (↑sc : R) * (↑s₁' : R) = rd * rc * (↑s₂ : R)
rw₄ : rd * ((↑sc : R) * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
have rw₅ : rd * (rc * (↑s₂ : R)) = rd * rc * (↑s₂ : R)
Tactic: rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : (↑sb : R) * (↑s₁ : R) = rb * (↑s₁' : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₁' : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rb = rd * (↑sc : R)
rw : (↑sd : R) * ((↑sb : R) * (↑s₁ : R)) = rd * rc * (↑s₂ : R)
rw₁ : (↑sd : R) * (rb * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
rw₂ : (↑sd : R) * rb * (↑s₁' : R) = rd * rc * (↑s₂ : R)
rw₃ : rd * (↑sc : R) * (↑s₁' : R) = rd * rc * (↑s₂ : R)
rw₄ : rd * ((↑sc : R) * (↑s₁' : R)) = rd * rc * (↑s₂ : R)
rw₅ : rd * (rc * (↑s₂ : R)) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
have rw₆ : rd * rc * (↑s₂ : R) = rd * rc * (↑s₂ : R)
Tactic: rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]