awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
rw₆ rw₇ : (↑sd : R) * ((↑sc : R) * (↑s₃ : R)) = (↑sd : R) * ((↑sc : R) * (↑s₃ : R))
⊢ rd * rb * (↑s₁ : R) = (↑sd : R) * (↑sc : R) * (↑s₃ : R)

Tactic:
rw [mul_assoc, ← hb', ← mul_assoc, ← hd, mul_assoc, ← hc, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)

Tactic:
have : rd * rb * s₁ = sd * sc * s₃ := by
        rw [mul_assoc, ← hb', ← mul_assoc, ← hd, mul_assoc, ← hc, mul_assoc]
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
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)) ⋯)
⊢ Eq (α := OreLocalization S X) (add'' r₃ s₃ r₁ s₁) (add'' r₃ s₃ r₂ s₂)

Tactic:
rw [add''_char _ _ _ _ rc sc hc (sc * s₃).2]

Premises used: HMul.hMul, _private.0.OreLocalization.add''_char, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
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)) ⋯)
    (((↑sc : R) • r₃ + rc • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑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)) ⋯)

Tactic:
rw [add''_char _ _ _ _ _ _ this.symm (sd * sc * s₃).2]

Premises used: HMul.hMul, _private.0.OreLocalization.add''_char, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)) ⋯)

Tactic:
oreDiv_eq_iff.mpr ?_

Premises used: Iff.mpr, OreLocalization.oreDiv_eq_iff
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
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)) ⋯) : R) =
          v * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((↑sd : R) * (↑sc : R) * (↑s₃ : R)) ⋯) : 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)) ⋯)

Tactic:
refine oreDiv_eq_iff.mpr ?_

Premises used: Iff.mpr, OreLocalization.oreDiv_eq_iff
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
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))
⊢ ∃ (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)

Tactic:
simp only [smul_add]

Premises used: smul_add
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
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))
⊢ ∃ (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:
use sd, 1
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
h : (↑sd : R) • (↑sc : R) • r₃ + (↑sd : R) • rc • r₂ = (↑sd : R) • (↑sc : R) • r₃ + rd • (↑sb : R) • 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))

Tactic:
simp only [one_smul, one_mul, mul_smul, ← hb, Submonoid.smul_def, ← mul_assoc, and_true]

Premises used: and_true, mul_assoc, one_smul, Submonoid.smul_def, SemigroupAction.mul_smul, one_mul
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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 : R) • (↑sc : R) • r₃ + (↑sd : R) • rc • r₂ = (↑sd : R) • (↑sc : R) • r₃ + rd • (↑sb : R) • r₂

Tactic:
simp only [smul_smul, hd]

Premises used: smul_smul
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s s' : ↥S
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') =
    (oreDenom (↑s : R) s' • r + oreNum (↑s : R) s' • r') /ₒ (oreDenom (↑s : R) s' * s)

Tactic:
rfl
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s s' : ↥S
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') =
    (oreDenom (↑s : R) s' • r + oreNum (↑s : R) s' • r') /ₒ (oreDenom (↑s : R) s' * s)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s s' : ↥S
rb sb : R
h : sb * (↑s : R) = rb * (↑s' : R)
h' : sb * (↑s : R) ∈ S
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') =
    (sb • r + rb • r') /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s : R)) h'

Tactic:
add''_char r s r' s' rb sb h h'

Premises used: _private.0.OreLocalization.add''_char, Quotient.mk', _private.0.OreLocalization.add', OreLocalization.oreDiv, _private.0.OreLocalization.add''
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s s' : ↥S
rb sb : R
h : sb * (↑s : R) = rb * (↑s' : R)
h' : sb * (↑s : R) ∈ S
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') =
    (sb • r + rb • r') /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s : R)) h'

Tactic:
exact add''_char r s r' s' rb sb h h'

Premises used: _private.0.OreLocalization.add''_char
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s s' : ↥S
rb sb : R
h : sb * (↑s : R) = rb * (↑s' : R)
h' : sb * (↑s : R) ∈ S
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') =
    (sb • r + rb • r') /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s : R)) h'

Tactic:
with_unfolding_all exact add''_char r s r' s' rb sb h h'

Premises used: _private.0.OreLocalization.add''_char
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s s' : ↥S
rb : R
sb : ↥S
h : (↑sb : R) * (↑s : R) = rb * (↑s' : R)
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s') = (sb • r + rb • r') /ₒ (sb * s)

Tactic:
oreDiv_add_char' s s' rb sb h (sb * s).2

Premises used: HMul.hMul, OreLocalization.oreDiv_add_char', Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s : ↥S
⊢ (↑1 : R) * (↑s : R) = 1 * (↑s : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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' : X
s : ↥S
⊢ HAdd.hAdd (α := OreLocalization S X) (r /ₒ s) (r' /ₒ s) = (r + r') /ₒ s

Tactic:
simp [oreDiv_add_char s s 1 1 (by simp)]

Premises used: OreLocalization.oreDiv_add_char, OfNat.ofNat
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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
c : ∀ (r₁ : X) (s₁ : ↥S), r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)
⊢ x + y + z = x + (y + z)

Tactic:
induction x with | _ r₁ s₁
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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
c : ∀ (r₂ : X) (s₂ : ↥S), HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)
⊢ r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)

Tactic:
induction y with | _ r₂ s₂
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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
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₃)
⊢ HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)

Tactic:
induction z with | _ r₃ s₃
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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
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₃)
⊢ 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'⟩

Premises used: OreLocalization.oreDivAddChar'
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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₁)
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₃)
⊢ HAdd.hAdd (α := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) + r₃ /ₒ s₃ =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)

Tactic:
rw [ha']
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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)
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₃)
⊢ 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⟩

Premises used: HMul.hMul, HAdd.hAdd, HSMul.hSMul, OreLocalization.oreDivAddChar'
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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₁))
c :
  (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁)) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ 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:
rw [q]
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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 :
  (sc • sa • r₁ + (sc • ra • r₂ + rc • r₃)) /ₒ (sc * (sa * s₁)) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)
⊢ (sc • (sa • r₁ + 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]

Premises used: add_assoc, smul_add
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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 :
  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₃)
⊢ (sc • sa • r₁ + (sc • ra • r₂ + rc • r₃)) /ₒ (sc * (sa * s₁)) =
    r₁ /ₒ s₁ + HAdd.hAdd (α := OreLocalization S X) (r₂ /ₒ s₂) (r₃ /ₒ s₃)

Tactic:
simp_rw [← add_oreDiv, ← OreLocalization.expand']

Premises used: OreLocalization.expand', OreLocalization.add_oreDiv
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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₂)
c₁ : Eq (α := OreLocalization S X) (rc • r₃ /ₒ (sc * (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₃)

Tactic:
congr 2
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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₁))
    (ra • r₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯)
⊢ Eq (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁)) (r₂ /ₒ s₂)

Tactic:
rw [OreLocalization.expand r₂ s₂ ra (ha.symm ▸ (sa * s₁).2)]

Premises used: HMul.hMul, OreLocalization.expand, Eq.rec, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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 : sa * s₁ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯
⊢ Eq (α := OreLocalization S X) (ra • r₂ /ₒ (sa * s₁))
    (ra • r₂ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯)

Tactic:
congr
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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 : (↑(sa * s₁) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯) : R)
⊢ sa * s₁ = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯

Tactic:
ext
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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₁) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯) : R)

Tactic:
ha
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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₁) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (ra * (↑s₂ : R)) ⋯) : R)

Tactic:
exact ha
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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) (rc • r₃ /ₒ (sc * (sa * s₁)))
    (rc • r₃ /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) ⋯)
⊢ Eq (α := OreLocalization S X) (rc • r₃ /ₒ (sc * (sa * s₁))) (r₃ /ₒ s₃)

Tactic:
rw [OreLocalization.expand r₃ s₃ rc (hc.symm ▸ (sc * (sa * s₁)).2)]

Premises used: HMul.hMul, OreLocalization.expand, Eq.rec, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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 : sc * (sa * s₁) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (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)) ⋯)

Tactic:
congr
-- Module: Mathlib.RingTheory.OreLocalization.Basic
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 : (↑(sc * (sa * s₁)) : R) = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) ⋯) : R)
⊢ sc * (sa * s₁) = Subtype.mk (p := fun (x : R) ↦ x ∈ S) (rc * (↑s₃ : R)) ⋯

Tactic:
ext