awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : OreLocalization S M
x : OreLocalization S X
⊢ (r • m) • x = r • m • x
have rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = r • m • x
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]
-- 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 : OreLocalization S M
x : OreLocalization S X
rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = r • m • x
⊢ (r • m) • x = r • m • x
have rw₁ : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x =
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) (m • x)
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]
-- 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 : OreLocalization S M
x : OreLocalization S X
rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = r • m • x
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) (m • x)
⊢ (r • m) • x = r • m • x
have rw₂ : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = (HSMul.hSMul (β := M) r 1 /ₒ 1 * m) • x
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]
-- 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 : OreLocalization S M
x : OreLocalization S X
rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = r • m • x
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) (m • x)
rw₂ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = (HSMul.hSMul (β := M) r 1 /ₒ 1 * m) • x
⊢ (r • m) • x = r • m • x
have rw₃ : (HSMul.hSMul (β := M) r 1 /ₒ 1 * m) • x = (HSMul.hSMul (β := M) r 1 /ₒ 1 * m) • x
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]
-- 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 M M
r : R
x : OreLocalization S M
y : OreLocalization S X
⊢ r • x • y = x • r • y
have c : ∀ (r₁ : M) (s₁ : ↥S),
  r • HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) y = HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (r • y)
Tactic: cases x with | _ r₁ s₁
Cleared hypotheses: x
-- 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 M M
r : R
y : OreLocalization S X
r₁ : M
s₁ : ↥S
⊢ r • HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) y = HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (r • y)
have c : ∀ (r₂ : X) (s₂ : ↥S),
  r • HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (HSMul.hSMul (β := OreLocalization S X) r (r₂ /ₒ s₂))
Tactic: cases y with | _ r₂ s₂
Cleared hypotheses: y
-- 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 M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r • HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (HSMul.hSMul (β := OreLocalization S X) r (r₂ /ₒ s₂))
have c : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 * r₁ /ₒ s₁) (r₂ /ₒ s₂) =
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r₁ * HSMul.hSMul (β := M) r 1 /ₒ s₁) (r₂ /ₒ s₂)
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, smul_smul, smul_smul,
      mul_div_one, oreDiv_mul_char _ _ _ _ (r • 1) s₁ (by simp), mul_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 : SMul.{u_1, u_3} Rᵐᵒᵖ M
inst_14 : SMul.{u_1, u_4} Rᵐᵒᵖ X
inst_15 : IsScalarTower.{u_1, u_3, u_3} Rᵐᵒᵖ M M
inst_16 : IsScalarTower.{u_1, u_3, u_4} Rᵐᵒᵖ M X
inst_17 : IsCentralScalar R M
r : R
x : OreLocalization S X
⊢ MulOpposite.op r • x = r • x
have rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (MulOpposite.op r) 1 /ₒ 1) x = r • x
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, op_smul_eq_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 : SMul.{u_1, u_3} Rᵐᵒᵖ M
inst_14 : SMul.{u_1, u_4} Rᵐᵒᵖ X
inst_15 : IsScalarTower.{u_1, u_3, u_3} Rᵐᵒᵖ M M
inst_16 : IsScalarTower.{u_1, u_3, u_4} Rᵐᵒᵖ M X
inst_17 : IsCentralScalar R M
r : R
x : OreLocalization S X
rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (MulOpposite.op r) 1 /ₒ 1) x = r • x
⊢ MulOpposite.op r • x = r • x
have rw₁ : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (MulOpposite.op r) 1 /ₒ 1) x =
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, op_smul_eq_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 : SMul.{u_1, u_3} Rᵐᵒᵖ M
inst_14 : SMul.{u_1, u_4} Rᵐᵒᵖ X
inst_15 : IsScalarTower.{u_1, u_3, u_3} Rᵐᵒᵖ M M
inst_16 : IsScalarTower.{u_1, u_3, u_4} Rᵐᵒᵖ M X
inst_17 : IsCentralScalar R M
r : R
x : OreLocalization S X
rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (MulOpposite.op r) 1 /ₒ 1) x = r • x
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (MulOpposite.op r) 1 /ₒ 1) x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x
⊢ MulOpposite.op r • x = r • x
have rw₂ : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x =
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x
Tactic: rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, op_smul_eq_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R_1 : 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_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 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_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
s₁ s₂ : R
x : OreLocalization S X
⊢ (s₁ * s₂) • x = s₁ • s₂ • x
have rw : (s₁ • s₂) • x = s₁ • s₂ • x
Tactic: rw [← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R_1 : 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_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 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_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
s₁ s₂ : R
x : OreLocalization S X
rw : (s₁ • s₂) • x = s₁ • s₂ • x
⊢ (s₁ * s₂) • x = s₁ • s₂ • x
have rw₁ : s₁ • s₂ • x = s₁ • s₂ • x
Tactic: rw [← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R_1 : 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_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 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_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
x : X
s : ↥S
⊢ HSMul.hSMul (α := R) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s
have rw : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X)
    (HSMul.hSMul.{u_5, u_3, u_3} (α := R) (β := M) 1 1 /ₒ 1) (x /ₒ s) =
  x /ₒ s
Tactic: rw [← smul_one_oreDiv_one_smul, one_smul, ← OreLocalization.one_def, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R_1 : 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_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 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_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
x : X
s : ↥S
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X)
      (HSMul.hSMul.{u_5, u_3, u_3} (α := R) (β := M) 1 1 /ₒ 1) (x /ₒ s) =
    x /ₒ s
⊢ HSMul.hSMul (α := R) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s
have rw₁ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (1 /ₒ 1) (x /ₒ s) = x /ₒ s
Tactic: rw [← smul_one_oreDiv_one_smul, one_smul, ← OreLocalization.one_def, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R_1 : 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_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 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_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
x : X
s : ↥S
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X)
      (HSMul.hSMul.{u_5, u_3, u_3} (α := R) (β := M) 1 1 /ₒ 1) (x /ₒ s) =
    x /ₒ s
rw₁ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (1 /ₒ 1) (x /ₒ s) = x /ₒ s
⊢ HSMul.hSMul (α := R) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s
have rw₂ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s
Tactic: rw [← smul_one_oreDiv_one_smul, one_smul, ← OreLocalization.one_def, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R_1 : 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_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 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_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
x : X
s : ↥S
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X)
      (HSMul.hSMul.{u_5, u_3, u_3} (α := R) (β := M) 1 1 /ₒ 1) (x /ₒ s) =
    x /ₒ s
rw₁ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (1 /ₒ 1) (x /ₒ s) = x /ₒ s
rw₂ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s
⊢ HSMul.hSMul (α := R) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s
have rw₃ : Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s)
Tactic: rw [← smul_one_oreDiv_one_smul, one_smul, ← OreLocalization.one_def, 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 : X
⊢ HSMul.hSMul (β := OreLocalization S X) r (x /ₒ 1) = r • x /ₒ 1
have rw : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 /ₒ 1) (x /ₒ 1) = r • x /ₒ 1
Tactic: rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, 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 : X
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 /ₒ 1) (x /ₒ 1) =
    r • x /ₒ 1
⊢ HSMul.hSMul (β := OreLocalization S X) r (x /ₒ 1) = r • x /ₒ 1
have rw₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := M) r 1 • x /ₒ 1) (r • x /ₒ 1)
Tactic: rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, 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 : X
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 /ₒ 1) (x /ₒ 1) =
    r • x /ₒ 1
rw₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := M) r 1 • x /ₒ 1) (r • x /ₒ 1)
⊢ HSMul.hSMul (β := OreLocalization S X) r (x /ₒ 1) = r • x /ₒ 1
have rw₂ : Eq (α := OreLocalization S X) (r • HSMul.hSMul.{u_3, u_4, u_4} (α := M) 1 x /ₒ 1) (r • x /ₒ 1)
Tactic: rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, 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 : X
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 /ₒ 1) (x /ₒ 1) =
    r • x /ₒ 1
rw₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := M) r 1 • x /ₒ 1) (r • x /ₒ 1)
rw₂ : Eq (α := OreLocalization S X) (r • HSMul.hSMul.{u_3, u_4, u_4} (α := M) 1 x /ₒ 1) (r • x /ₒ 1)
⊢ HSMul.hSMul (β := OreLocalization S X) r (x /ₒ 1) = r • x /ₒ 1
have rw₃ : Eq (α := OreLocalization S X) (r • x /ₒ 1) (r • x /ₒ 1)
Tactic: rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
have rw : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₂ * s₁)) (r₁ * r₂ /ₒ (s₁ * s₂))
Tactic: rw [oreDiv_mul_char r₁ r₂ s₁ s₂ r₁ s₂ (by simp [mul_comm]), mul_comm s₂]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
rw : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₂ * s₁)) (r₁ * r₂ /ₒ (s₁ * s₂))
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
have rw₁ : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₁ * s₂)) (r₁ * r₂ /ₒ (s₁ * s₂))
Tactic: rw [oreDiv_mul_char r₁ r₂ s₁ s₂ r₁ s₂ (by simp [mul_comm]), mul_comm s₂]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
x y : OreLocalization S R
⊢ x * y = y * x
have c : ∀ (r₁ : R) (s₁ : ↥S), r₁ /ₒ s₁ * y = y * (r₁ /ₒ s₁)
Tactic: cases x with | _ r₁ s₁
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ r₁ /ₒ s₁ * y = y * (r₁ /ₒ s₁)
have c : ∀ (r₂ : R) (s₂ : ↥S),
  HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
Tactic: cases y with | _ r₂ s₂
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
have c : r₁ * r₂ /ₒ (s₁ * s₂) = HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
Tactic: rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
c : r₁ * r₂ /ₒ (s₁ * s₂) = HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
have c₁ : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₁ * s₂)) (r₂ * r₁ /ₒ (s₂ * s₁))
Tactic: rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
c : r₁ * r₂ /ₒ (s₁ * s₂) = HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
c₁ : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₁ * s₂)) (r₂ * r₁ /ₒ (s₂ * s₁))
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
have c₂ : Eq (α := OreLocalization S R) (r₂ * r₁ /ₒ (s₁ * s₂)) (r₂ * r₁ /ₒ (s₂ * s₁))
Tactic: rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
c : r₁ * r₂ /ₒ (s₁ * s₂) = HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
c₁ : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₁ * s₂)) (r₂ * r₁ /ₒ (s₂ * s₁))
c₂ : Eq (α := OreLocalization S R) (r₂ * r₁ /ₒ (s₁ * s₂)) (r₂ * r₁ /ₒ (s₂ * s₁))
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
have c₃ : Eq (α := OreLocalization S R) (r₂ * r₁ /ₒ (s₂ * s₁)) (r₂ * r₁ /ₒ (s₂ * s₁))
Tactic: rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
⊢ Surjective (β := OreLocalization S X) fun (x : X) ↦ x /ₒ 1
have refine : ∀ (x : X) (s : ↥S), ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: refine OreLocalization.ind fun x s ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have obtain : ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i = s ^ j),
  ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ ·)
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have inr : ∀
  (this :
    ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i = s ^ j) (hlt : j < i),
      ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s))
  (hlt : i ≤ j), ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: wlog! hlt : j < i generalizing i j