awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
r s : R₀
x : OreLocalization S X
⊢ (r + s) • x = r • x + s • x

Tactic:
simp only [← smul_one_oreDiv_one_smul, add_smul, ← add_oreDiv]

Premises used: OreLocalization.smul_one_oreDiv_one_smul, add_smul, OreLocalization.add_oreDiv
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
rw : HSMul.hSMul (α := OreLocalization S R) (HSMul.hSMul.{u_3, u_1, u_1} (α := R₀) (β := R) 0 1 /ₒ 1) x = 0
rw₁ : HSMul.hSMul (α := OreLocalization S R) (0 /ₒ 1) x = 0
rw₂ : HSMul.hSMul (α := OreLocalization S R) 0 x = 0
rw₃ rw₄ : Eq (α := OreLocalization S X) 0 0
⊢ HSMul.hSMul (α := R₀) 0 x = 0

Tactic:
rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]

Premises used: OreLocalization.smul_one_oreDiv_one_smul, zero_smul, OreLocalization.zero_oreDiv
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst_1 : Semiring R
S : Submonoid R
inst_2 : OreSet S
X : Type u_2
inst_3 : AddCommMonoid X
inst_4 : Module R X
n : ℕ
x : OreLocalization S X
inst : Module ℕ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Tactic:
congr($(AddCommMonoid.uniqueNatModule.2 inst).smul n x)

Premises used: congrArg, id, AddCommMonoid.uniqueNatModule, Unique.uniq, SMul.smul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst_1 : Semiring R
S : Submonoid R
inst_2 : OreSet S
X : Type u_2
inst_3 : AddCommMonoid X
inst_4 : Module R X
n : ℕ
x : OreLocalization S X
inst : Module ℕ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Tactic:
exact congr($(AddCommMonoid.uniqueNatModule.2 inst).smul n x)
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
⊢ Eq.{u_1 + 1} (α := OreLocalization S R) (OneHom.toFun (↑numeratorHom : OneHom R (OreLocalization S R)) 0) 0

Tactic:
OreLocalization.zero_def

Premises used: Set.Mem, OreLocalization.zero_def, Quotient.mk', OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
⊢ Eq.{u_1 + 1} (α := OreLocalization S R) (OneHom.toFun (↑numeratorHom : OneHom R (OreLocalization S R)) 0) 0

Tactic:
exact OreLocalization.zero_def

Premises used: OreLocalization.zero_def
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
⊢ Eq.{u_1 + 1} (α := OreLocalization S R) (OneHom.toFun (↑numeratorHom : OneHom R (OreLocalization S R)) 0) 0

Tactic:
with_unfolding_all exact OreLocalization.zero_def

Premises used: OreLocalization.zero_def
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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 : CommSemiring R₀
inst_5 : Algebra R₀ R
r : R₀
x : OreLocalization S R
c :
  ∀ (r₁ : R) (s₁ : ↥S),
    HMul.hMul (α := OreLocalization S R) (β := OreLocalization S R)
        (((RingHom.comp numeratorRingHom (algebraMap R₀ R) : RingHom.{u_3, u_1} R₀ (OreLocalization S R)) :
              (a : R₀) → OreLocalization S R)
            r :
          OreLocalization S R)
        (r₁ /ₒ s₁) =
      HMul.hMul (α := OreLocalization S R) (β := OreLocalization S R) (r₁ /ₒ s₁)
        (((RingHom.comp numeratorRingHom (algebraMap R₀ R) : RingHom.{u_3, u_1} R₀ (OreLocalization S R)) :
              (a : R₀) → OreLocalization S R)
            r :
          OreLocalization S R)
⊢ HMul.hMul (α := OreLocalization S R)
      (((RingHom.comp numeratorRingHom (algebraMap R₀ R) : RingHom.{u_3, u_1} R₀ (OreLocalization S R)) :
            (a : R₀) → OreLocalization S R)
          r :
        OreLocalization S R)
      x =
    HMul.hMul (β := OreLocalization S R) x
      (((RingHom.comp numeratorRingHom (algebraMap R₀ R) : RingHom.{u_3, u_1} R₀ (OreLocalization S R)) :
            (a : R₀) → OreLocalization S R)
          r :
        OreLocalization S R)

Tactic:
induction x using OreLocalization.ind with | _ r₁ s₁
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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 : CommSemiring R₀
inst_5 : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
c :
  HMul.hMul (α := OreLocalization S R) (β := OreLocalization S R)
      ((algebraMap R₀ R : (a : R₀) → R) r /ₒ 1 : OreLocalization S R) (r₁ /ₒ s₁) =
    HMul.hMul (β := R) r₁ ((algebraMap R₀ R : (a : R₀) → R) r : R) /ₒ s₁
c₁ :
  Eq (α := OreLocalization S R) (HMul.hMul (α := R) ((algebraMap R₀ R : (a : R₀) → R) r : R) r₁ /ₒ (s₁ * 1))
    (HMul.hMul (β := R) r₁ ((algebraMap R₀ R : (a : R₀) → R) r : R) /ₒ s₁)
c₂ :
  Eq (α := OreLocalization S R) (HMul.hMul (β := R) r₁ ((algebraMap R₀ R : (a : R₀) → R) r : R) /ₒ (s₁ * 1))
    (HMul.hMul (β := R) r₁ ((algebraMap R₀ R : (a : R₀) → R) r : R) /ₒ s₁)
c₃ c₄ :
  Eq (α := OreLocalization S R) (HMul.hMul (β := R) r₁ ((algebraMap R₀ R : (a : R₀) → R) r : R) /ₒ s₁)
    (HMul.hMul (β := R) r₁ ((algebraMap R₀ R : (a : R₀) → R) r : R) /ₒ s₁)
⊢ HMul.hMul (α := OreLocalization S R) (β := OreLocalization S R)
      ((algebraMap R₀ R : (a : R₀) → R) r /ₒ 1 : OreLocalization S R) (r₁ /ₒ s₁) =
    HMul.hMul (α := OreLocalization S R) (β := OreLocalization S R) (r₁ /ₒ s₁)
      ((algebraMap R₀ R : (a : R₀) → R) r /ₒ 1 : OreLocalization S R)

Tactic:
rw [mul_div_one, oreDiv_mul_char _ _ _ _ (algebraMap R₀ R r) s₁ (Algebra.commutes _ _).symm,
      Algebra.commutes, mul_one]

Premises used: Algebra.algebraMap, OreLocalization.mul_div_one, OreLocalization.oreDiv_mul_char, mul_one, Eq.symm, DFunLike.coe, Algebra.commutes
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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 : CommSemiring R₀
inst_5 : Algebra R₀ R
r : R₀
x : OreLocalization S R
rw : r • x = HSMul.hSMul (β := R) r 1 /ₒ 1 * x
rw₁ : r • x = HSMul.hSMul (α := OreLocalization S R) (HSMul.hSMul (β := R) r 1 /ₒ 1) x
rw₂ rw₃ : r • x = r • x
⊢ r • x = HMul.hMul (α := OreLocalization S R) ((algebraMap R₀ R : (a : R₀) → R) r /ₒ 1 : OreLocalization S R) x

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← smul_eq_mul, smul_one_oreDiv_one_smul]

Premises used: Algebra.algebraMap_eq_smul_one, OreLocalization.smul_one_oreDiv_one_smul, smul_eq_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
simp : Eq.{u_3 + 1} (α := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) 0 : T) (0 : T)
⊢ OneHom.toFun (M := OreLocalization S R) (↑(universalMulHom (↑f : R →* T) fS hf) : OneHom (OreLocalization S R) T) 0 =
    0

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]

Premises used: RingHom.toMonoidHom_eq_coe, MonoidHom.toOneHom_coe, OneHom.toFun_eq_coe
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
rw : HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) 1)⁻¹ : T) : T) (((↑f : R →* T) : (a : R) → T) 0 : T) = 0
⊢ Eq.{u_3 + 1} (α := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) 0 : T) (0 : T)

Tactic:
rw [OreLocalization.zero_def, universalMulHom_apply]

Premises used: OreLocalization.zero_def, OreLocalization.universalMulHom_apply
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
⊢ HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) 1)⁻¹ : T) : T) (((↑f : R →* T) : (a : R) → T) 0 : T) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x y : OreLocalization S R
simp :
  (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (x + y) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) x : T)
      ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) y : T)
⊢ OneHom.toFun (↑(universalMulHom (↑f : R →* T) fS hf) : OneHom (OreLocalization S R) T) (x + y) =
    OneHom.toFun (↑(universalMulHom (↑f : R →* T) fS hf) : OneHom (OreLocalization S R) T) x +
      OneHom.toFun (↑(universalMulHom (↑f : R →* T) fS hf) : OneHom (OreLocalization S R) T) y

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]

Premises used: RingHom.toMonoidHom_eq_coe, MonoidHom.toOneHom_coe, OneHom.toFun_eq_coe
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
x y : OreLocalization S R
c :
  ∀ (r₁ : R) (s₁ : ↥S),
    (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁ + y) =
      HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
        ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) y : T)
⊢ (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (x + y) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) x : T)
      ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) y : T)

Tactic:
induction x with | _ r₁ s₁
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
y : OreLocalization S R
r₁ : R
s₁ : ↥S
c :
  ∀ (r₂ : R) (s₂ : ↥S),
    (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T)
        (HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
      HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
        ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)
⊢ (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁ + y) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) y : T)

Tactic:
induction y with | _ r₂ s₂
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
c :
  ∀ (r₃ : R) (s₃ : ↥S) (h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R))
    (h₃' : HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = (s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)),
    (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T)
        (HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
      HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
        ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)
⊢ (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T)
      (HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)

Tactic:
rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨r₃, s₃, h₃, h₃'⟩

Premises used: OreLocalization.oreDivAddChar'
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
h₃' : HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = (s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)
c :
  (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) ((s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)
⊢ (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T)
      (HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)

Tactic:
rw [h₃']
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
c :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (s₃ * s₁))⁻¹ : T) : T)
      ((f : (a : R) → T) ((↑s₃ : R) * r₁ + r₃ * r₂) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
⊢ (universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) ((s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)

Tactic:
simp only [smul_eq_mul, universalMulHom_apply, MonoidHom.coe_coe,
        Submonoid.smul_def]

Premises used: MonoidHom.coe_coe, Submonoid.smul_def, OreLocalization.universalMulHom_apply, smul_eq_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
c :
  HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
      (HMul.hMul (α := T) (β := T) ((f : (a : R) → T) (↑s₃ : R) : T) ((f : (a : R) → T) r₁ : T) +
        HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T)) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
⊢ HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (s₃ * s₁))⁻¹ : T) : T)
      ((f : (a : R) → T) ((↑s₃ : R) * r₁ + r₃ * r₂) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)

Tactic:
simp only [mul_inv_rev, map_mul, map_add, map_mul, Units.val_mul]

Premises used: map_add, map_mul, mul_inv_rev, Units.val_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
c :
  (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) *
        HMul.hMul (β := T)
          (↑(HMul.hMul (α := Tˣ) (β := Tˣ) (((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : Tˣ) ((fS : (a : ↥S) → Tˣ) s₃ : Tˣ)) : T)
          ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
        HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
⊢ HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
      (HMul.hMul (α := T) (β := T) ((f : (a : R) → T) (↑s₃ : R) : T) ((f : (a : R) → T) r₁ : T) +
        HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T)) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)

Tactic:
rw [mul_add, mul_assoc, ← mul_assoc _ (f s₃), hf, ← Units.val_mul]

Premises used: mul_assoc, mul_add, Subtype.val, DFunLike.coe, Units.val_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
c :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
        HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
⊢ (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) *
        HMul.hMul (β := T)
          (↑(HMul.hMul (α := Tˣ) (β := Tˣ) (((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : Tˣ) ((fS : (a : ↥S) → Tˣ) s₃ : Tˣ)) : T)
          ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
        HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)

Tactic:
simp only [one_mul, inv_mul_cancel, Units.val_one]

Premises used: inv_mul_cancel, Units.val_one, one_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
c :
  HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
      HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
⊢ HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
        HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.OreLocalization.Ring
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
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
c :
  HMul.hMul (β := T)
      (HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
        ((f : (a : R) → T) r₃ : T))
      ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
⊢ HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
      HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc