awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
h₁ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
h₂ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₃ :
  HMul.hMul (α := T) (β := T) (1 : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₄ :
  HMul.hMul (α := T) (β := T) ((↑1 : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₅ :
  HMul.hMul (β := T)
      (↑(HMul.hMul (α := Tˣ) (β := Tˣ) (((fS : (a : ↥S) → Tˣ) s)⁻¹ : Tˣ) ((fS : (a : ↥S) → Tˣ) s : Tˣ)) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₆ :
  HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s) : T))
      ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₇ : (↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) *
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * (↑s : M) ∈ S
⊢ Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ oreDenom (HSMul.hSMul (β := M) c 1) s)
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
have rw : Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ (oreDenom (HSMul.hSMul (β := M) c 1) s * 1))
  (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
    oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
Tactic: rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * (↑s : M) ∈ S
rw :
  Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ (oreDenom (HSMul.hSMul (β := M) c 1) s * 1))
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
⊢ Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ oreDenom (HSMul.hSMul (β := M) c 1) s)
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
have rw₁ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
  oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
    oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
Tactic: rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * (↑s : M) ∈ S
rw :
  Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ (oreDenom (HSMul.hSMul (β := M) c 1) s * 1))
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
⊢ Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ oreDenom (HSMul.hSMul (β := M) c 1) s)
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
have rw₂ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
  oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
    (oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) * 1)
Tactic: rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * (↑s : M) ∈ S
rw :
  Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ (oreDenom (HSMul.hSMul (β := M) c 1) s * 1))
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
rw₂ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      (oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) * 1)
⊢ Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ oreDenom (HSMul.hSMul (β := M) c 1) s)
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
have rw₃ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1)
    (t • r /ₒ Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
Tactic: rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * (↑s : M) ∈ S
rw :
  Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ (oreDenom (HSMul.hSMul (β := M) c 1) s * 1))
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
rw₂ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      (oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) * 1)
rw₃ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1)
      (t • r /ₒ Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
⊢ Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ oreDenom (HSMul.hSMul (β := M) c 1) s)
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
have rw₄ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s)
Tactic: rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
x : OreLocalization S X
⊢ HSMul.hSMul (α := OreLocalization S M) (r /ₒ 1) x = r • x
have c : ∀ (r_1 : X) (s : ↥S),
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
r_1 : X
s : ↥S
⊢ HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
have c : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
  oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s
Tactic: rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
r_1 : X
s : ↥S
c :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s
⊢ HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
have c₁ : Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ (oreDenom r s * 1))
  (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
Tactic: rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
r_1 : X
s : ↥S
c :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s
c₁ :
  Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ (oreDenom r s * 1))
    (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
⊢ HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
have c₂ : Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s)
  (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
Tactic: rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
r_1 : X
s : ↥S
c :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s
c₁ :
  Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ (oreDenom r s * 1))
    (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
c₂ :
  Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s)
    (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
⊢ HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
have c₃ : Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s) (oreNum (r * 1) s • r_1 /ₒ oreDenom (r * 1) s)
Tactic: rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
r_1 : X
s : ↥S
c :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s
c₁ :
  Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ (oreDenom r s * 1))
    (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
c₂ :
  Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s)
    (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
c₃ : Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s) (oreNum (r * 1) s • r_1 /ₒ oreDenom (r * 1) s)
⊢ HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
have c₄ : Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s) (oreNum r s • r_1 /ₒ oreDenom r s)
Tactic: rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : OreLocalization S X
⊢ HSMul.hSMul (β := M) r 1 • x = r • x
have c : ∀ (r_1 : X) (s : ↥S),
  HSMul.hSMul (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : OreLocalization S X
⊢ HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x = r • x
have rw : HSMul.hSMul (β := M) r 1 • x = r • x
Tactic: rw [oreDiv_one_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : OreLocalization S X
rw : HSMul.hSMul (β := M) r 1 • x = r • x
⊢ HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x = r • x
have rw₁ : r • x = r • x
Tactic: rw [oreDiv_one_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
⊢ (r • m) • x = r • m • x
have rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (r • m) 1 /ₒ 1) x =
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 * HSMul.hSMul (β := M) m 1 /ₒ 1) x
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul,
      ← mul_smul, mul_div_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ r • m • x = m • r • x
have rw : r • HSMul.hSMul (β := M) m 1 • x = m • r • x
Tactic: rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
rw : r • HSMul.hSMul (β := M) m 1 • x = m • r • x
⊢ r • m • x = m • r • x
have rw₁ : (r • HSMul.hSMul (β := M) m 1) • x = m • r • x
Tactic: rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
rw : r • HSMul.hSMul (β := M) m 1 • x = m • r • x
rw₁ : (r • HSMul.hSMul (β := M) m 1) • x = m • r • x
⊢ r • m • x = m • r • x
have rw₂ : (m • HSMul.hSMul (β := M) r 1) • x = m • r • x
Tactic: rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
rw : r • HSMul.hSMul (β := M) m 1 • x = m • r • x
rw₁ : (r • HSMul.hSMul (β := M) m 1) • x = m • r • x
rw₂ : (m • HSMul.hSMul (β := M) r 1) • x = m • r • x
⊢ r • m • x = m • r • x
have rw₃ : m • HSMul.hSMul (β := M) r 1 • x = m • r • x
Tactic: rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
rw : r • HSMul.hSMul (β := M) m 1 • x = m • r • x
rw₁ : (r • HSMul.hSMul (β := M) m 1) • x = m • r • x
rw₂ : (m • HSMul.hSMul (β := M) r 1) • x = m • r • x
rw₃ : m • HSMul.hSMul (β := M) r 1 • x = m • r • x
⊢ r • m • x = m • r • x
have rw₄ : m • r • x = m • r • x
Tactic: rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]