awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : HSMul.hSMul (α := OreLocalization S R) (HSMul.hSMul.{u_3, u_1, u_1} (α := R₀) (β := R) 0 1 /ₒ 1) x = 0
⊢ HSMul.hSMul (α := R₀) 0 x = 0
have rw₁ : HSMul.hSMul (α := OreLocalization S R) (0 /ₒ 1) x = 0
Tactic: rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]
-- 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
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
⊢ HSMul.hSMul (α := R₀) 0 x = 0
have rw₂ : HSMul.hSMul (α := OreLocalization S R) 0 x = 0
Tactic: rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]
-- 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
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
⊢ HSMul.hSMul (α := R₀) 0 x = 0
have rw₃ : Eq (α := OreLocalization S X) 0 0
Tactic: rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]
-- 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 : CommSemiring R₀
inst_5 : Algebra R₀ R
r : R₀
x : 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)
have 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)
Tactic: induction x using OreLocalization.ind 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₀ : Type u_3
inst_4 : CommSemiring R₀
inst_5 : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥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)
have 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₁
Tactic: rw [mul_div_one, oreDiv_mul_char _ _ _ _ (algebraMap R₀ R r) s₁ (Algebra.commutes _ _).symm,
      Algebra.commutes, mul_one]
-- 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 : 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₁
⊢ 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)
have 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₁)
Tactic: rw [mul_div_one, oreDiv_mul_char _ _ _ _ (algebraMap R₀ R r) s₁ (Algebra.commutes _ _).symm,
      Algebra.commutes, mul_one]
-- 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 : 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₁)
⊢ 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)
have 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₁)
Tactic: rw [mul_div_one, oreDiv_mul_char _ _ _ _ (algebraMap R₀ R r) s₁ (Algebra.commutes _ _).symm,
      Algebra.commutes, mul_one]
-- 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 : 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₁)
⊢ 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)
have 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₁)
Tactic: rw [mul_div_one, oreDiv_mul_char _ _ _ _ (algebraMap R₀ R r) s₁ (Algebra.commutes _ _).symm,
      Algebra.commutes, mul_one]
-- 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 : CommSemiring R₀
inst_5 : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = HMul.hMul (α := OreLocalization S R) ((algebraMap R₀ R : (a : R₀) → R) r /ₒ 1 : OreLocalization S R) x
have rw : r • x = HSMul.hSMul (β := R) r 1 /ₒ 1 * x
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_eq_mul, smul_one_oreDiv_one_smul]
-- 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 : CommSemiring R₀
inst_5 : Algebra R₀ R
r : R₀
x : OreLocalization S R
rw : r • x = HSMul.hSMul (β := R) r 1 /ₒ 1 * x
⊢ r • x = HMul.hMul (α := OreLocalization S R) ((algebraMap R₀ R : (a : R₀) → R) r /ₒ 1 : OreLocalization S R) x
have rw₁ : r • x = HSMul.hSMul (α := OreLocalization S R) (HSMul.hSMul (β := R) r 1 /ₒ 1) x
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_eq_mul, smul_one_oreDiv_one_smul]
-- 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 : 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
⊢ r • x = HMul.hMul (α := OreLocalization S R) ((algebraMap R₀ R : (a : R₀) → R) r /ₒ 1 : OreLocalization S R) x
have rw₂ : r • x = r • x
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_eq_mul, smul_one_oreDiv_one_smul]
-- 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
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)
⊢ OneHom.toFun (M := OreLocalization S R) (↑(universalMulHom (↑f : R →* T) fS hf) : OneHom (OreLocalization S R) T) 0 =
    0
have simp : Eq.{u_3 + 1} (α := T) ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) 0 : T) (0 : T)
Tactic: simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
-- 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
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)
⊢ Eq.{u_3 + 1} (α := T) ((universalMulHom (↑f : R →* T) fS ⋯ : (a : OreLocalization S R) → T) 0 : T) (0 : T)
have rw : HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) 1)⁻¹ : T) : T) (((↑f : R →* T) : (a : R) → T) 0 : T) = 0
Tactic: rw [OreLocalization.zero_def, universalMulHom_apply]
-- 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
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
⊢ 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
have simp : (universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (x + y) =
  HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) x : T)
    ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) y : T)
Tactic: simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
-- 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
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
⊢ (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)
have c : ∀ (r₁ : R) (s₁ : ↥S),
  (universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₁ /ₒ s₁ + y) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) y : T)
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
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
⊢ (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)
have c : ∀ (r₂ : R) (s₂ : ↥S),
  (universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T)
      (HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)
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
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
⊢ (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)
have 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 sorry : (a : OreLocalization S R) → T)
      (HAdd.hAdd (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
    HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
      ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)
Tactic: rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨r₃, s₃, h₃, 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
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₁)
⊢ (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)
have c : (universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) ((s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)) =
  HAdd.hAdd (α := T) (β := T) ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₁ /ₒ s₁) : T)
    ((universalMulHom (↑f : R →* T) fS sorry : (a : OreLocalization S R) → T) (r₂ /ₒ s₂) : T)
Tactic: rw [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
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)
⊢ (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)
have 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)
Tactic: simp only [smul_eq_mul, universalMulHom_apply, MonoidHom.coe_coe,
        Submonoid.smul_def]
-- 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
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)
⊢ 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)
have 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)
Tactic: simp only [mul_inv_rev, map_mul, map_add, map_mul, Units.val_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
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)
⊢ 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)
have 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)
Tactic: rw [mul_add, mul_assoc, ← mul_assoc _ (f s₃), hf, ← Units.val_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
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)
⊢ (↑((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)
have 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)
Tactic: simp only [one_mul, inv_mul_cancel, Units.val_one]