awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
inst_4 : SMulCommClass M N N
r : M
x : N
n : ℕ
rw : r • x * (r • x) ^ n = r ^ (n + 1) • x ^ (n + 1)
rw₁ : r • x * r ^ n • x ^ n = r ^ (n + 1) • x ^ (n + 1)
rw₂ : (r * r ^ n) • (x * x ^ n) = r ^ (n + 1) • x ^ (n + 1)
rw₃ : r ^ (n + 1) • (x * x ^ n) = r ^ (n + 1) • x ^ (n + 1)
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
have rw₄ : r ^ (n + 1) • x ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
Tactic: rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a : α
⊢ g⁻¹ • g • a = a
have rw : (g⁻¹ * g) • a = a
Tactic: rw [smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a : α
rw : (g⁻¹ * g) • a = a
⊢ g⁻¹ • g • a = a
have rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := G) 1 a = a
Tactic: rw [smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a : α
rw : (g⁻¹ * g) • a = a
rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := G) 1 a = a
⊢ g⁻¹ • g • a = a
have rw₂ : a = a
Tactic: rw [smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a : α
⊢ g • g⁻¹ • a = a
have rw : (g * g⁻¹) • a = a
Tactic: rw [smul_smul, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a : α
rw : (g * g⁻¹) • a = a
⊢ g • g⁻¹ • a = a
have rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := G) 1 a = a
Tactic: rw [smul_smul, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a : α
rw : (g * g⁻¹) • a = a
rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := G) 1 a = a
⊢ g • g⁻¹ • a = a
have rw₂ : a = a
Tactic: rw [smul_smul, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = g • b
have rw : a = g • g⁻¹ • a
Tactic: rw [← h, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
rw : a = g • g⁻¹ • a
⊢ a = g • b
have rw₁ : a = a
Tactic: rw [← h, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : a = g • b
⊢ g⁻¹ • a = b
have rw : g⁻¹ • g • b = b
Tactic: rw [h, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : a = g • b
rw : g⁻¹ • g • b = b
⊢ g⁻¹ • a = b
have rw₁ : b = b
Tactic: rw [h, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ g • a = b
have rw : g • g⁻¹ • b = b
Tactic: rw [h, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
rw : g • g⁻¹ • b = b
⊢ g • a = b
have rw₁ : b = b
Tactic: rw [h, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = g⁻¹ • b
have rw : a = g⁻¹ • g • a
Tactic: rw [← h, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
α : Type u_5
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
h : g • a = b
rw : a = g⁻¹ • g • a
⊢ a = g⁻¹ • b
have rw₁ : a = a
Tactic: rw [← h, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
g : G
a : H
⊢ g • a * g⁻¹ • a⁻¹ = 1
have rw : (g * g⁻¹) • (a * a⁻¹) = 1
Tactic: rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
g : G
a : H
rw : (g * g⁻¹) • (a * a⁻¹) = 1
⊢ g • a * g⁻¹ • a⁻¹ = 1
have rw₁ : HSMul.hSMul.{u_3, u_4, u_4} (α := G) 1 (a * a⁻¹) = 1
Tactic: rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
g : G
a : H
rw : (g * g⁻¹) • (a * a⁻¹) = 1
rw₁ : HSMul.hSMul.{u_3, u_4, u_4} (α := G) 1 (a * a⁻¹) = 1
⊢ g • a * g⁻¹ • a⁻¹ = 1
have rw₂ : HSMul.hSMul.{u_3, u_4, u_4} (α := G) (β := H) 1 1 = 1
Tactic: rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
g : G
a : H
rw : (g * g⁻¹) • (a * a⁻¹) = 1
rw₁ : HSMul.hSMul.{u_3, u_4, u_4} (α := G) 1 (a * a⁻¹) = 1
rw₂ : HSMul.hSMul.{u_3, u_4, u_4} (α := G) (β := H) 1 1 = 1
⊢ g • a * g⁻¹ • a⁻¹ = 1
have rw₃ : Eq.{u_4 + 1} (α := H) 1 1
Tactic: rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
g : G
a : H
n : ℤ
⊢ (g • a) ^ n = g ^ n • a ^ n
have ofNat : ∀ (a_1 : ℕ), (g • a) ^ Int.ofNat a_1 = g ^ Int.ofNat a_1 • a ^ Int.ofNat a_1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
g : G
a : H
n : ℤ
ofNat : ∀ (a_1 : ℕ), (g • a) ^ Int.ofNat a_1 = g ^ Int.ofNat a_1 • a ^ Int.ofNat a_1
⊢ (g • a) ^ n = g ^ n • a ^ n
have negSucc : ∀ (a_1 : ℕ), (g • a) ^ Int.negSucc a_1 = g ^ Int.negSucc a_1 • a ^ Int.negSucc a_1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
⊢ r • s • x = s • r • x
have rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
⊢ r • s • x = s • r • x
have rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
⊢ r • s • x = s • r • x
have rw₂ : HSMul.hSMul (β := G) r 1 • s • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
rw₂ : HSMul.hSMul (β := G) r 1 • s • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
⊢ r • s • x = s • r • x
have rw₃ : HSMul.hSMul (β := G) r 1 • HSMul.hSMul (β := G) s 1 • x = s • r • HSMul.hSMul (α := G) 1 x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
rw₂ : HSMul.hSMul (β := G) r 1 • s • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
rw₃ : HSMul.hSMul (β := G) r 1 • HSMul.hSMul (β := G) s 1 • x = s • r • HSMul.hSMul (α := G) 1 x
⊢ r • s • x = s • r • x
have rw₄ : HSMul.hSMul (β := G) s 1 • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
rw₂ : HSMul.hSMul (β := G) r 1 • s • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
rw₃ : HSMul.hSMul (β := G) r 1 • HSMul.hSMul (β := G) s 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₄ : HSMul.hSMul (β := G) s 1 • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
⊢ r • s • x = s • r • x
have rw₅ : s • HSMul.hSMul (α := G) 1 (HSMul.hSMul (β := G) r 1 • x) = s • r • HSMul.hSMul (α := G) 1 x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
rw₂ : HSMul.hSMul (β := G) r 1 • s • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
rw₃ : HSMul.hSMul (β := G) r 1 • HSMul.hSMul (β := G) s 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₄ : HSMul.hSMul (β := G) s 1 • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₅ : s • HSMul.hSMul (α := G) 1 (HSMul.hSMul (β := G) r 1 • x) = s • r • HSMul.hSMul (α := G) 1 x
⊢ r • s • x = s • r • x
have rw₆ : s • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
rw₂ : HSMul.hSMul (β := G) r 1 • s • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
rw₃ : HSMul.hSMul (β := G) r 1 • HSMul.hSMul (β := G) s 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₄ : HSMul.hSMul (β := G) s 1 • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₅ : s • HSMul.hSMul (α := G) 1 (HSMul.hSMul (β := G) r 1 • x) = s • r • HSMul.hSMul (α := G) 1 x
rw₆ : s • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
⊢ r • s • x = s • r • x
have rw₇ : s • r • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
A : Type u_9
B : Type u_10
G : Type u_11
inst : CommMonoid G
inst_1 : SMul A G
inst_2 : SMul B G
inst_3 : IsScalarTower A G G
inst_4 : IsScalarTower B G G
r : A
s : B
x : G
rw : r • HSMul.hSMul (α := G) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := G) r 1 • s • x = s • r • x
rw₂ : HSMul.hSMul (β := G) r 1 • s • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
rw₃ : HSMul.hSMul (β := G) r 1 • HSMul.hSMul (β := G) s 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₄ : HSMul.hSMul (β := G) s 1 • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₅ : s • HSMul.hSMul (α := G) 1 (HSMul.hSMul (β := G) r 1 • x) = s • r • HSMul.hSMul (α := G) 1 x
rw₆ : s • HSMul.hSMul (β := G) r 1 • x = s • r • HSMul.hSMul (α := G) 1 x
rw₇ : s • r • HSMul.hSMul (α := G) 1 x = s • r • HSMul.hSMul (α := G) 1 x
⊢ r • s • x = s • r • x
have rw₈ : s • r • x = s • r • x
Tactic: rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
inst_3 : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ (x₁ • y) • z = x₁ • y • z
have rw : x₁ • y * z = x₁ • y • z
Tactic: rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
inst_3 : SMulCommClass R₁ R R
x₁ : R₁
y z : R
rw : x₁ • y * z = x₁ • y • z
⊢ (x₁ • y) • z = x₁ • y • z
have rw₁ : z * x₁ • y = x₁ • y • z
Tactic: rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
inst_3 : SMulCommClass R₁ R R
x₁ : R₁
y z : R
rw : x₁ • y * z = x₁ • y • z
rw₁ : z * x₁ • y = x₁ • y • z
⊢ (x₁ • y) • z = x₁ • y • z
have rw₂ : z • x₁ • y = x₁ • y • z
Tactic: rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
inst_3 : SMulCommClass R₁ R R
x₁ : R₁
y z : R
rw : x₁ • y * z = x₁ • y • z
rw₁ : z * x₁ • y = x₁ • y • z
rw₂ : z • x₁ • y = x₁ • y • z
⊢ (x₁ • y) • z = x₁ • y • z
have rw₃ : x₁ • z • y = x₁ • y • z
Tactic: rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
inst_3 : SMulCommClass R₁ R R
x₁ : R₁
y z : R
rw : x₁ • y * z = x₁ • y • z
rw₁ : z * x₁ • y = x₁ • y • z
rw₂ : z • x₁ • y = x₁ • y • z
rw₃ : x₁ • z • y = x₁ • y • z
⊢ (x₁ • y) • z = x₁ • y • z
have rw₄ : x₁ • (z * y) = x₁ • y • z
Tactic: rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
inst_3 : SMulCommClass R₁ R R
x₁ : R₁
y z : R
rw : x₁ • y * z = x₁ • y • z
rw₁ : z * x₁ • y = x₁ • y • z
rw₂ : z • x₁ • y = x₁ • y • z
rw₃ : x₁ • z • y = x₁ • y • z
rw₄ : x₁ • (z * y) = x₁ • y • z
⊢ (x₁ • y) • z = x₁ • y • z
have rw₅ : x₁ • (y * z) = x₁ • y • z
Tactic: rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
inst_3 : SMulCommClass R₁ R R
x₁ : R₁
y z : R
rw : x₁ • y * z = x₁ • y • z
rw₁ : z * x₁ • y = x₁ • y • z
rw₂ : z • x₁ • y = x₁ • y • z
rw₃ : x₁ • z • y = x₁ • y • z
rw₄ : x₁ • (z * y) = x₁ • y • z
rw₅ : x₁ • (y * z) = x₁ • y • z
⊢ (x₁ • y) • z = x₁ • y • z
have rw₆ : x₁ • y • z = x₁ • y • z
Tactic: rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
α : Type u_5
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
inst_2 : MulAction N α
inst_3 : SMul M α
inst_4 : IsScalarTower M N α
x : M
y : α
⊢ HSMul.hSMul (β := N) x 1 • y = x • y
have rw : x • HSMul.hSMul.{u_10, u_5, u_5} (α := N) 1 y = x • y
Tactic: rw [smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
α : Type u_5
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
inst_2 : MulAction N α
inst_3 : SMul M α
inst_4 : IsScalarTower M N α
x : M
y : α
rw : x • HSMul.hSMul.{u_10, u_5, u_5} (α := N) 1 y = x • y
⊢ HSMul.hSMul (β := N) x 1 • y = x • y
have rw₁ : x • y = x • y
Tactic: rw [smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : MulOneClass N
inst_1 : SMul M N
inst_2 : IsScalarTower M N N
x : M
y : N
⊢ HSMul.hSMul (β := N) x 1 * y = x • y
have rw : x • (1 * y) = x • y
Tactic: rw [smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : MulOneClass N
inst_1 : SMul M N
inst_2 : IsScalarTower M N N
x : M
y : N
rw : x • (1 * y) = x • y
⊢ HSMul.hSMul (β := N) x 1 * y = x • y
have rw₁ : x • y = x • y
Tactic: rw [smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : MulOneClass N
inst_1 : SMul M N
inst_2 : SMulCommClass M N N
x : M
y : N
⊢ y * HSMul.hSMul (β := N) x 1 = x • y
have rw : y • HSMul.hSMul (β := N) x 1 = x • y
Tactic: rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : MulOneClass N
inst_1 : SMul M N
inst_2 : SMulCommClass M N N
x : M
y : N
rw : y • HSMul.hSMul (β := N) x 1 = x • y
⊢ y * HSMul.hSMul (β := N) x 1 = x • y
have rw₁ : x • HSMul.hSMul (β := N) y 1 = x • y
Tactic: rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : MulOneClass N
inst_1 : SMul M N
inst_2 : SMulCommClass M N N
x : M
y : N
rw : y • HSMul.hSMul (β := N) x 1 = x • y
rw₁ : x • HSMul.hSMul (β := N) y 1 = x • y
⊢ y * HSMul.hSMul (β := N) x 1 = x • y
have rw₂ : x • (y * 1) = x • y
Tactic: rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : MulOneClass N
inst_1 : SMul M N
inst_2 : SMulCommClass M N N
x : M
y : N
rw : y • HSMul.hSMul (β := N) x 1 = x • y
rw₁ : x • HSMul.hSMul (β := N) y 1 = x • y
rw₂ : x • (y * 1) = x • y
⊢ y * HSMul.hSMul (β := N) x 1 = x • y
have rw₃ : x • y = x • y
Tactic: rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
h : ∀ (x : M) (y : N), HSMul.hSMul (β := N) x 1 * y = x • y
x : M
y z : N
⊢ (x • y) • z = x • y • z
have rw : (HSMul.hSMul (β := N) x 1 * y) • z = x • y • z
Tactic: rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
h : ∀ (x : M) (y : N), HSMul.hSMul (β := N) x 1 * y = x • y
x : M
y z : N
rw : (HSMul.hSMul (β := N) x 1 * y) • z = x • y • z
⊢ (x • y) • z = x • y • z
have rw₁ : HSMul.hSMul (β := N) x 1 * y * z = x • y • z
Tactic: rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
h : ∀ (x : M) (y : N), HSMul.hSMul (β := N) x 1 * y = x • y
x : M
y z : N
rw : (HSMul.hSMul (β := N) x 1 * y) • z = x • y • z
rw₁ : HSMul.hSMul (β := N) x 1 * y * z = x • y • z
⊢ (x • y) • z = x • y • z
have rw₂ : HSMul.hSMul (β := N) x 1 * (y * z) = x • y • z
Tactic: rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
h : ∀ (x : M) (y : N), HSMul.hSMul (β := N) x 1 * y = x • y
x : M
y z : N
rw : (HSMul.hSMul (β := N) x 1 * y) • z = x • y • z
rw₁ : HSMul.hSMul (β := N) x 1 * y * z = x • y • z
rw₂ : HSMul.hSMul (β := N) x 1 * (y * z) = x • y • z
⊢ (x • y) • z = x • y • z
have rw₃ : x • (y * z) = x • y • z
Tactic: rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
h : ∀ (x : M) (y : N), HSMul.hSMul (β := N) x 1 * y = x • y
x : M
y z : N
rw : (HSMul.hSMul (β := N) x 1 * y) • z = x • y • z
rw₁ : HSMul.hSMul (β := N) x 1 * y * z = x • y • z
rw₂ : HSMul.hSMul (β := N) x 1 * (y * z) = x • y • z
rw₃ : x • (y * z) = x • y • z
⊢ (x • y) • z = x • y • z
have rw₄ : x • (y * z) = x • (y * z)
Tactic: rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
H : ∀ (x : M) (y : N), y * HSMul.hSMul (β := N) x 1 = x • y
x : M
y z : N
⊢ x • y • z = y • x • z
have rw : x • y • z = y • (z * HSMul.hSMul (β := N) x 1)
Tactic: rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
H : ∀ (x : M) (y : N), y * HSMul.hSMul (β := N) x 1 = x • y
x : M
y z : N
rw : x • y • z = y • (z * HSMul.hSMul (β := N) x 1)
⊢ x • y • z = y • x • z
have rw₁ : x • (y * z) = y • (z * HSMul.hSMul (β := N) x 1)
Tactic: rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
H : ∀ (x : M) (y : N), y * HSMul.hSMul (β := N) x 1 = x • y
x : M
y z : N
rw : x • y • z = y • (z * HSMul.hSMul (β := N) x 1)
rw₁ : x • (y * z) = y • (z * HSMul.hSMul (β := N) x 1)
⊢ x • y • z = y • x • z
have rw₂ : y * z * HSMul.hSMul (β := N) x 1 = y • (z * HSMul.hSMul (β := N) x 1)
Tactic: rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
H : ∀ (x : M) (y : N), y * HSMul.hSMul (β := N) x 1 = x • y
x : M
y z : N
rw : x • y • z = y • (z * HSMul.hSMul (β := N) x 1)
rw₁ : x • (y * z) = y • (z * HSMul.hSMul (β := N) x 1)
rw₂ : y * z * HSMul.hSMul (β := N) x 1 = y • (z * HSMul.hSMul (β := N) x 1)
⊢ x • y • z = y • x • z
have rw₃ : y * z * HSMul.hSMul (β := N) x 1 = y * (z * HSMul.hSMul (β := N) x 1)
Tactic: rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]