awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.OreSet (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty.{u_1 + 1} (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
have mp : Nonempty.{u_1 + 1} (OreSet S) → ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.OreSet (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
mp : Nonempty.{u_1 + 1} (OreSet S) → ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
⊢ Nonempty.{u_1 + 1} (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
have mpr : (∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)) → Nonempty.{u_1 + 1} (OreSet S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.OreSet (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
S : Submonoid R
H : ∀ (r : R) (s : ↥S), ∃ (r' : R), ∃ (s' : ↥S), (↑s' : R) * r = r' * (↑s : R)
⊢ Nonempty.{u_1 + 1} (OreSet S)
have mpr : ∀ (r' : (r : R) → (s : ↥S) → R) (s' : (r : R) → (s : ↥S) → ↥S)
  (h : ∀ (r : R) (s : ↥S), (↑(s' r s) : R) * r = r' r s * (↑s : R)), Nonempty.{u_1 + 1} (OreSet S)
Tactic: choose r' s' h using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
x : OreLocalization S X
⊢ HSMul.hSMul (α := OreLocalization S R) 0 x = 0
have c : ∀ (r : X) (s : ↥S), HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) 0 (r /ₒ s) = 0
Tactic: induction x with | _ r s
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r : X
s : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) 0 (r /ₒ s) = 0
have c : Eq (α := OreLocalization S X) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 r /ₒ HMul.hMul (α := ↥S) 1 1) 0
Tactic: rw [OreLocalization.zero_def, oreDiv_smul_char 0 r 1 s 0 1 (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
y z : OreLocalization S R
x : OreLocalization S X
⊢ (y + z) • x = y • x + z • x
have c : ∀ (r₁ : X) (s₁ : ↥S),
  HSMul.hSMul (β := OreLocalization S X) (y + z) (r₁ /ₒ s₁) =
    HSMul.hSMul (β := OreLocalization S X) y (r₁ /ₒ s₁) + HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)
Tactic: induction x with | _ r₁ s₁
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
y z : OreLocalization S R
r₁ : X
s₁ : ↥S
⊢ HSMul.hSMul (β := OreLocalization S X) (y + z) (r₁ /ₒ s₁) =
    HSMul.hSMul (β := OreLocalization S X) y (r₁ /ₒ s₁) + HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)
have c : ∀ (r₂ : R) (s₂ : ↥S),
  HSMul.hSMul (β := OreLocalization S X) (r₂ /ₒ s₂ + z) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)
Tactic: induction y with | _ r₂ s₂
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ HSMul.hSMul (β := OreLocalization S X) (r₂ /ₒ s₂ + z) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁)
have c : ∀ (r₃ : R) (s₃ : ↥S),
  HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
Tactic: induction z with | _ r₃ s₃
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
⊢ HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
have c : ∀ (ra : R) (sa : ↥S) (ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R))
  (q : HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)),
  HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
Tactic: rcases oreDivAddChar' r₂ r₃ s₂ s₃ with ⟨ra, sa, ha, q⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
q : HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃) = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ HSMul.hSMul (β := OreLocalization S X) (HAdd.hAdd (α := OreLocalization S R) (r₂ /ₒ s₂) (r₃ /ₒ s₃)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
Tactic: rw [q]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₂ /ₒ s₂) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
Tactic: rw [OreLocalization.expand' r₂ s₂ sa]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
have c : ∀ (rb : R) (sb : ↥S) (hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R))
  (q :
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
      rb • r₁ /ₒ (sb * (sa * s₂))),
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
Tactic: rcases oreDivSMulChar' (sa • r₂) r₁ (sa * s₂) s₁ with ⟨rb, sb, hb, q⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
q :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (sa • r₂ /ₒ (sa * s₂)) (r₁ /ₒ s₁) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
  rb • r₁ /ₒ (sb * (sa * s₂)) + HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
Tactic: rw [q]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
⊢ (↑sb : R) * ra * (↑s₃ : R) ∈ S
have rw : (↑sb : R) * ((↑sa : R) * (↑s₂ : R)) ∈ S
Tactic: rw [mul_assoc, ← ha]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
⊢ (↑sb : R) * ((↑sa : R) * (↑s₂ : R)) ∈ S
have norm_cast : (↑(sb * (sa * s₂)) : R) ∈ S
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
have hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
Tactic: have hs₃rasb : sb * ra * s₃ ∈ S := by
    rw [mul_assoc, ← ha]
    norm_cast
    apply SetLike.coe_mem
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₁ /ₒ s₁)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
  rb • r₁ /ₒ (sb * (sa * s₂)) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      (((↑sb : R) * ra) • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sb : R) * ra * (↑s₃ : R)) hs₃rasb) (r₁ /ₒ s₁)
Tactic: rw [OreLocalization.expand _ _ _ hs₃rasb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
        (((↑sb : R) * ra) • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sb : R) * ra * (↑s₃ : R)) hs₃rasb) (r₁ /ₒ s₁)
have ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
Tactic: have ha' : ↑((sb * sa) * s₂) = sb * ra * s₃ := by simp [ha, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
        (((↑sb : R) * ra) • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sb : R) * ra * (↑s₃ : R)) hs₃rasb) (r₁ /ₒ s₁)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
  rb • r₁ /ₒ (sb * (sa * s₂)) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁)
Tactic: rw [← Subtype.coe_eq_of_eq_mk ha']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
        (r₁ /ₒ s₁)
have c : ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R))
  (hc' :
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
        (r₁ /ₒ s₁) =
      rc • r₁ /ₒ (sc * (sb * sa * s₂))),
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
        (r₁ /ₒ s₁)
Tactic: rcases oreDivSMulChar' ((sb * ra) • r₃) r₁ (sb * sa * s₂) s₁ with ⟨rc, sc, hc, hc'⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
        (r₁ /ₒ s₁)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
  HAdd.hAdd (α := OreLocalization S X) (rb • r₁ /ₒ (sb * (sa * s₂))) (rc • r₁ /ₒ (sc * (sb * sa * s₂)))
Tactic: rw [hc']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    HAdd.hAdd (α := OreLocalization S X) (rb • r₁ /ₒ (sb * (sa * s₂))) (rc • r₁ /ₒ (sc * (sb * sa * s₂)))
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
  (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))
Tactic: rw [oreDiv_add_char _ _ 1 sc (by simp [mul_assoc])]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) (r₁ /ₒ s₁) =
    (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
    ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
  (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))
Tactic: rw [OreLocalization.expand' (sa • r₂ + ra • r₃) (sa * s₂) (sc * sb)]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * sa • r₂ = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra) • r₃ = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
    (sc • rb • r₁ + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (rc • r₁)) /ₒ (sc * (sb * (sa * s₂)))
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
    (((↑sc : R) * (↑sb : R) * ((↑sa : R) * r₂) + (↑sc : R) * (↑sb : R) * (ra * r₃)) /ₒ (sc * sb * (sa * s₂)))
    (r₁ /ₒ s₁) =
  ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Tactic: simp only [smul_eq_mul, one_smul, Submonoid.smul_def, mul_add, Submonoid.coe_mul] at hb hc ⊢
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * ((↑sa : R) * r₂) = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra * r₃) = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      (((↑sc : R) * (↑sb : R) * ((↑sa : R) * r₂) + (↑sc : R) * (↑sb : R) * (ra * r₃)) /ₒ (sc * sb * (sa * s₂)))
      (r₁ /ₒ s₁) =
    ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
    (((↑sc : R) * rb + rc) * (↑s₁ : R) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
  ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Tactic: rw [mul_assoc, hb, mul_assoc, ← mul_assoc _ ra, hc, ← mul_assoc, ← add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₂ : R) = ra * (↑s₃ : R)
rb : R
sb : ↥S
hb : (↑sb : R) * ((↑sa : R) * r₂) = rb * (↑s₁ : R)
hs₃rasb : (↑sb : R) * ra * (↑s₃ : R) ∈ S
ha' : (↑(sb * sa * s₂) : R) = (↑sb : R) * ra * (↑s₃ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * ((↑sb : R) * ra * r₃) = rc * (↑s₁ : R)
hc' :
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (((↑sb : R) * ra) • r₃ /ₒ (sb * sa * s₂))
      (r₁ /ₒ s₁) =
    rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X)
      (((↑sc : R) * rb + rc) * (↑s₁ : R) /ₒ (sc * sb * (sa * s₂))) (r₁ /ₒ s₁) =
    ((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
have c : Eq (α := OreLocalization S X) (((↑sc : R) * rb + rc) • r₁ /ₒ (sc * sb * (sa * s₂)))
  (((↑sc : R) • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂))))
Tactic: rw [OreLocalization.smul_cancel']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
R₀ : Type u_3
inst_4 : Semiring R₀
inst_5 : Module R₀ X
inst_6 : Module R₀ R
inst_7 : IsScalarTower R₀ R X
inst_8 : IsScalarTower R₀ R R
x : OreLocalization S X
⊢ HSMul.hSMul (α := R₀) 0 x = 0
have rw : HSMul.hSMul (α := OreLocalization S R) (HSMul.hSMul.{u_3, u_1, u_1} (α := R₀) (β := R) 0 1 /ₒ 1) x = 0
Tactic: rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]