awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (hypothesis)
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)
    (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯)
    (add'' r₁ s₁ r₂ s₂)
have this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
Tactic: have : sd * sb * s₁ = rd * rc * s₂ := by
      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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X)
    (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯)
    (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)
  ((((↑sd : R) * (↑sb : R)) • r₁ + (rd * rc) • r₂) /ₒ
    Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) sorry)
Tactic: rw [add''_char _ _ _ _ (rd * rc : R) (sd * sb) this (sd * sb * 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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X)
    (((↑sc : R) • r₁' + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯)
    ((((↑sd : R) * (↑sb : R)) • r₁ + (rd * rc) • r₂) /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯)
have rw : ∃ (u : ↥S),
  ∃ (v : R),
    u • ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = v • ((↑sc : R) • r₁' + rc • r₂) ∧
      (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) sorry) : R) =
        v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) sorry) : R)
Tactic: rw [mul_smul, ← Submonoid.smul_def sb, hb, smul_smul, hd, oreDiv_eq_iff]
-- 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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = v • ((↑sc : R) • r₁' + rc • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
          v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)
have h : ∃ (v : R),
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = v • ((↑sc : R) • r₁' + rc • r₂) ∧
    (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) sorry) : R) =
      v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) sorry) : R)
Tactic: use 1
-- 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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
⊢ ∃ (v : R),
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) =
        v • ((↑sc : R) • r₁' + rc • r₂) ∧
      (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
        v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)
have h : HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = rd • ((↑sc : R) • r₁' + rc • r₂) ∧
  (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) sorry) : R) =
    rd * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) sorry) : R)
Tactic: use rd
-- 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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((rd * (↑sc : R)) • r₁' + (rd * rc) • r₂) = rd • ((↑sc : R) • r₁' + rc • r₂) ∧
    (↑1 : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sb : R) * (↑s₁ : R)) ⋯) : R) =
      rd * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₁' : R)) ⋯) : R)
have h : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * ((↑sc : R) * (↑s₁' : R))
Tactic: simp only [mul_smul, smul_add, one_smul, OneMemClass.coe_one, one_mul, true_and]
-- 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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * ((↑sc : R) * (↑s₁' : R))
have h : rd * rc * (↑s₂ : R) = rd * ((↑sc : R) * (↑s₁' : R))
Tactic: rw [this, 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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
h : rd * rc * (↑s₂ : R) = rd * ((↑sc : R) * (↑s₁' : R))
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * ((↑sc : R) * (↑s₁' : R))
have h₁ : rd * rc * (↑s₂ : R) = rd * (rc * (↑s₂ : R))
Tactic: rw [this, 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)
this : (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * rc * (↑s₂ : R)
h : rd * rc * (↑s₂ : R) = rd * ((↑sc : R) * (↑s₁' : R))
h₁ : rd * rc * (↑s₂ : R) = rd * (rc * (↑s₂ : R))
⊢ (↑sd : R) * (↑sb : R) * (↑s₁ : R) = rd * ((↑sc : R) * (↑s₁' : R))
have h₂ : rd * (rc * (↑s₂ : R)) = rd * (rc * (↑s₂ : R))
Tactic: rw [this, 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
x : OreLocalization S X
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) ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ add' rs.fst rs.snd x) (r₁, s₁))
    ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ add' rs.fst rs.snd x) (r₂, s₂))
have c : ∀ (r₃ : X) (s₃ : ↥S),
  Eq (α := OreLocalization S X)
    ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ (add' rs.fst rs.snd (r₃ /ₒ s₃) : OreLocalization S X)) (r₁, s₁))
    ((fun (rs : Prod.{u_2, u_1} X ↥S) ↦ (add' rs.fst rs.snd (r₃ /ₒ s₃) : OreLocalization S X)) (r₂, s₂))
Tactic: induction x with | _ r₃ s₃
Cleared hypotheses: x
-- 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₂ 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)
r₃ : X
s₃ : ↥S
⊢ Eq (α := OreLocalization S X) (add'' (r₃, s₃).fst (r₃, s₃).snd (r₁, s₁).fst (r₁, s₁).snd)
    (add'' (r₃, s₃).fst (r₃, s₃).snd (r₂, s₂).fst (r₂, s₂).snd)
have c : Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
Tactic: dsimp only 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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
have c : ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)),
  Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ 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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
have c : ∀ (rd : R) (sd : ↥S) (hd : (↑sd : R) * rc = rd * (↑sb : R)),
  Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
Tactic: rcases oreCondition rc sb 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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
have rw : rd * (rb * (↑s₁ : R)) = (↑sd : R) * (↑sc : R) * (↑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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
rw : rd * (rb * (↑s₁ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
have rw₁ : rd * ((↑sb : R) * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
rw : rd * (rb * (↑s₁ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₁ : rd * ((↑sb : R) * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
have rw₂ : rd * (↑sb : R) * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
rw : rd * (rb * (↑s₁ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₁ : rd * ((↑sb : R) * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₂ : rd * (↑sb : R) * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
have rw₃ : (↑sd : R) * rc * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
rw : rd * (rb * (↑s₁ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₁ : rd * ((↑sb : R) * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₂ : rd * (↑sb : R) * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₃ : (↑sd : R) * rc * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
have rw₄ : (↑sd : R) * (rc * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
rw : rd * (rb * (↑s₁ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₁ : rd * ((↑sb : R) * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₂ : rd * (↑sb : R) * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₃ : (↑sd : R) * rc * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₄ : (↑sd : R) * (rc * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
have rw₅ : (↑sd : R) * ((↑sc : R) * (↑s₃ : R)) = (↑sd : R) * (↑sc : R) * (↑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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
rw : rd * (rb * (↑s₁ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₁ : rd * ((↑sb : R) * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₂ : rd * (↑sb : R) * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₃ : (↑sd : R) * rc * (↑s₂ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₄ : (↑sd : R) * (rc * (↑s₂ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
rw₅ : (↑sd : R) * ((↑sc : R) * (↑s₃ : R)) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
have rw₆ : (↑sd : R) * ((↑sc : R) * (↑s₃ : R)) = (↑sd : R) * ((↑sc : R) * (↑s₃ : R))
Tactic: rw [mul_assoc, ← hb', ← mul_assoc, ← hd, mul_assoc, ← hc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (hypothesis)
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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
have this : rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
Tactic: have : rd * rb * s₁ = sd * sc * s₃ := by
        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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
this : rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)
have c : Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁)
  (((↑sc : R) • r₃ + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₃ : R)) sorry)
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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
this : rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁)
    (((↑sc : R) • r₃ + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₃ : R)) ⋯)
have c : Eq (α := OreLocalization S X)
  ((((↑sd : R) * (↑sc : R)) • r₃ + (rd * rb) • r₁) /ₒ
    Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sc : R) * (↑s₃ : R)) sorry)
  (((↑sc : R) • r₃ + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₃ : R)) sorry)
Tactic: rw [add''_char _ _ _ _ _ _ this.symm (sd * 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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
this : rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ Eq (α := OreLocalization S X)
    ((((↑sd : R) * (↑sc : R)) • r₃ + (rd * rb) • r₁) /ₒ
      Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sc : R) * (↑s₃ : R)) ⋯)
    (((↑sc : R) • r₃ + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₃ : R)) ⋯)
have c : ∃ (u : ↥S),
  ∃ (v : R),
    u • ((↑sc : R) • r₃ + rc • r₂) = v • (((↑sd : R) * (↑sc : R)) • r₃ + (rd * rb) • r₁) ∧
      (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₃ : R)) sorry) : R) =
        v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sc : R) * (↑s₃ : R)) sorry) : R)
Tactic: refine oreDiv_eq_iff.mpr ?_
-- 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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
this : rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • ((↑sc : R) • r₃ + rc • r₂) = v • (((↑sd : R) * (↑sc : R)) • r₃ + (rd * rb) • r₁) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sc : R) * (↑s₃ : R)) ⋯) : R) =
          v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sc : R) * (↑s₃ : R)) ⋯) : R)
have c : ∃ (u : ↥S),
  ∃ (v : R),
    u • (↑sc : R) • r₃ + u • rc • r₂ = v • ((↑sd : R) * (↑sc : R)) • r₃ + v • (rd * rb) • r₁ ∧
      (↑u : R) * ((↑sc : R) * (↑s₃ : R)) = v * ((↑sd : R) * (↑sc : R) * (↑s₃ : R))
Tactic: simp only [smul_add]
-- 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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
this : rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (↑sc : R) • r₃ + u • rc • r₂ = v • ((↑sd : R) * (↑sc : R)) • r₃ + v • (rd * rb) • r₁ ∧
        (↑u : R) * ((↑sc : R) * (↑s₃ : R)) = v * ((↑sd : R) * (↑sc : R) * (↑s₃ : R))
have h : sd • (↑sc : R) • r₃ + sd • rc • r₂ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (((↑sd : R) * (↑sc : R)) • r₃) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 ((rd * rb) • r₁) ∧
  (↑sd : R) * ((↑sc : R) * (↑s₃ : R)) = 1 * ((↑sd : R) * (↑sc : R) * (↑s₃ : R))
Tactic: use sd, 1
-- 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₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : (↑sb : R) * (↑s₂ : R) = rb * (↑s₁ : R)
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : (↑sc : R) * (↑s₃ : R) = rc * (↑s₂ : R)
rd : R
sd : ↥S
hd : (↑sd : R) * rc = rd * (↑sb : R)
this : rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)
⊢ sd • (↑sc : R) • r₃ + sd • rc • r₂ =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (((↑sd : R) * (↑sc : R)) • r₃) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 ((rd * rb) • r₁) ∧
    (↑sd : R) * ((↑sc : R) * (↑s₃ : R)) = 1 * ((↑sd : R) * (↑sc : R) * (↑s₃ : R))
have h : (↑sd : R) • (↑sc : R) • r₃ + (↑sd : R) • rc • r₂ = (↑sd : R) • (↑sc : R) • r₃ + rd • (↑sb : R) • r₂
Tactic: simp only [one_smul, one_mul, mul_smul, ← hb, Submonoid.smul_def, ← mul_assoc, and_true]
-- 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
x y z : OreLocalization S X
⊢ x + y + z = x + (y + z)
have c : ∀ (r₁ : X) (s₁ : ↥S), r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)
Tactic: induction x with | _ r₁ s₁
Cleared hypotheses: x