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
y z : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)
have c : ∀ (r₂ : X) (s₂ : ↥S), HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)
Tactic: induction y with | _ r₂ s₂
Cleared hypotheses: y
-- 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
z : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)
have c : ∀ (r₃ : X) (s₃ : ↥S),
  HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + r₃ /ₒ s₃ =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
Tactic: induction z with | _ r₃ s₃
Cleared hypotheses: z
-- 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₃ : ↥S
⊢ HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + r₃ /ₒ s₃ =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c : ∀ (ra : R) (sa : ↥S) (ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R))
  (ha' : HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)),
  HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + r₃ /ₒ s₃ =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
Tactic: rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
ha' : HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)
⊢ HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + r₃ /ₒ s₃ =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c : HAdd.hAdd (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
  r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
Tactic: rw [ha']
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
⊢ HAdd.hAdd (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c : ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R))
  (q :
    HAdd.hAdd (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
      (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁))),
  HAdd.hAdd (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
Tactic: rcases oreDivAddChar' (sa • r₁ + ra • r₂) r₃ (sa * s₁) s₃ with ⟨rc, sc, hc, q⟩
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
q :
  HAdd.hAdd (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁))
⊢ HAdd.hAdd (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) (r₃ /ₒ s₃) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c : (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁)) =
  r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
Tactic: rw [q]
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁)) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c : (sc • sa • r₁ + (sc • ra • r₂ + rc • r₃)) /ₒ (sc * (sa * s₁)) =
  r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
Tactic: simp only [smul_add, add_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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ (sc • sa • r₁ + (sc • ra • r₂ + rc • r₃)) /ₒ (sc * (sa * s₁)) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c : r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁)) (rc • r₃ /ₒ (sc * (sa * s₁))) =
  r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
Tactic: simp_rw [← add_oreDiv, ← OreLocalization.expand']
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁)) (rc • r₃ /ₒ (sc * (sa * s₁))) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c : Eq (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁)) (r₂ /ₒ s₂)
Tactic: congr 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
c : Eq (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁)) (r₂ /ₒ s₂)
⊢ r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁)) (rc • r₃ /ₒ (sc * (sa * s₁))) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
have c₁ : Eq (α := OreLocalization S X) (rc • r₃ /ₒ (sc * (sa * s₁))) (r₃ /ₒ s₃)
Tactic: congr 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ Eq (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁)) (r₂ /ₒ s₂)
have c : Eq (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁))
  (ra • r₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) sorry)
Tactic: rw [OreLocalization.expand r₂ s₂ ra (ha.symm ▸ (sa * 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ Eq (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁))
    (ra • r₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯)
have c : sa * s₁ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) sorry
Tactic: congr
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ sa * s₁ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯
have c : (↑(sa * s₁) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) sorry) : R)
Tactic: ext
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ Eq (α := OreLocalization S X) (rc • r₃ /ₒ (sc * (sa * s₁))) (r₃ /ₒ s₃)
have c : Eq (α := OreLocalization S X) (rc • r₃ /ₒ (sc * (sa * s₁)))
  (rc • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) sorry)
Tactic: rw [OreLocalization.expand r₃ s₃ rc (hc.symm ▸ (sc * (sa * 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ Eq (α := OreLocalization S X) (rc • r₃ /ₒ (sc * (sa * s₁)))
    (rc • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) ⋯)
have c : sc * (sa * s₁) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) sorry
Tactic: congr
-- 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₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * (↑(sa * s₁) : R) = rc * (↑s₃ : R)
⊢ sc * (sa * s₁) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) ⋯
have c : (↑(sc * (sa * s₁)) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) sorry) : R)
Tactic: ext
-- 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
s : ↥S
⊢ Eq (α := OreLocalization S X) (0 /ₒ s) 0
have rw : ∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := X) u 0 = HSMul.hSMul (β := X) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑s : R)
Tactic: rw [OreLocalization.zero_def, 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
x : OreLocalization S X
⊢ 0 + x = x
have c : ∀ (r : X) (s : ↥S), HAdd.hAdd (α := OreLocalization S X) 0 (r /ₒ s) = r /ₒ s
Tactic: induction x
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
⊢ HAdd.hAdd (α := OreLocalization S X) 0 (r /ₒ s) = r /ₒ s
have c : Eq (α := OreLocalization S X) ((0 + r) /ₒ s) (r /ₒ s)
Tactic: rw [← zero_oreDiv, add_oreDiv]
-- 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
⊢ x + 0 = x
have c : ∀ (r : X) (s : ↥S), HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) 0 = r /ₒ s
Tactic: induction x
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
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) 0 = r /ₒ s
have c : Eq (α := OreLocalization S X) ((r + 0) /ₒ s) (r /ₒ s)
Tactic: rw [← zero_oreDiv, add_oreDiv]
-- 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 R
⊢ HSMul.hSMul (β := OreLocalization S X) x 0 = 0
have c : ∀ (r : R) (s : ↥S), HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0
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 : R
s : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
Tactic: rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]
-- 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 : R
s : ↥S
c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0
have c₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := X) r 0 /ₒ s) (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]
-- 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 : R
s : ↥S
c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := X) r 0 /ₒ s) (0 /ₒ 1)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0
have c₂ : Eq (α := OreLocalization S X) (0 /ₒ s) (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]
-- 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 : R
s : ↥S
c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := X) r 0 /ₒ s) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S X) (0 /ₒ s) (0 /ₒ 1)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0
have c₃ : Eq (α := OreLocalization S X) 0 (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]
-- 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 : R
s : ↥S
c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := X) r 0 /ₒ s) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S X) (0 /ₒ s) (0 /ₒ 1)
c₃ : Eq (α := OreLocalization S X) 0 (0 /ₒ 1)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r /ₒ s) 0 = 0
have c₄ : Eq (α := OreLocalization S X) 0 0
Tactic: rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]
-- 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
z : OreLocalization S R
x y : OreLocalization S X
⊢ z • (x + y) = z • x + z • y
have c : ∀ (r₁ : X) (s₁ : ↥S), z • (r₁ /ₒ s₁ + y) = HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁) + z • y
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
z : OreLocalization S R
y : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ z • (r₁ /ₒ s₁ + y) = HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁) + z • y
have c : ∀ (r₂ : X) (s₂ : ↥S),
  z • HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HSMul.hSMul (β := OreLocalization S X) z (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.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
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ z • HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HSMul.hSMul (β := OreLocalization S X) z (r₁ /ₒ s₁) + HSMul.hSMul (β := OreLocalization S X) z (r₂ /ₒ s₂)
have c : ∀ (r₃ : R) (s₃ : ↥S),
  HSMul.hSMul (α := OreLocalization S R) (r₃ /ₒ s₃) (HAdd.hAdd (α := OreLocalization S X) (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.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₃ : R
s₃ : ↥S
⊢ HSMul.hSMul (α := OreLocalization S R) (r₃ /ₒ s₃) (HAdd.hAdd (α := OreLocalization S X) (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))
  (ha' : HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)),
  HSMul.hSMul (α := OreLocalization S R) (r₃ /ₒ s₃) (HAdd.hAdd (α := OreLocalization S X) (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, ha'⟩
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
ha' : HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)
⊢ HSMul.hSMul (α := OreLocalization S R) (r₃ /ₒ s₃) (HAdd.hAdd (α := OreLocalization S X) (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) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * 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 [ha']
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * 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) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * 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.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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ ra * (↑s₂ : R) ∈ S
have rw : (↑(sa * s₁) : R) ∈ S
Tactic: rw [← ha]
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (r₂ /ₒ s₂)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃)
      (ra • r₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) sorry)
Tactic: rw [OreLocalization.expand r₂ s₂ ra (by rw [← ha]; apply SetLike.coe_mem)]
-- 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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : (↑(sa * s₁) : R) = ra * (↑s₂ : R)
⊢ HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
      HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃)
        (ra • r₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯)
have c : HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
  HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (sa • r₁ /ₒ (sa * s₁)) +
    HSMul.hSMul (α := OreLocalization S R) (β := OreLocalization S X) (r₃ /ₒ s₃) (ra • r₂ /ₒ (sa * s₁))
Tactic: rw [← Subtype.coe_eq_of_eq_mk ha]