awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ g • x = h • x → g = h
have rw : (g⁻¹ * h) • x = x → g⁻¹ * h = 1
Tactic: rw [smul_eq_iff_eq_inv_smul, eq_comm, ← mul_smul, ← inv_mul_eq_one (G := α)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
G_1 : Type u_1
M : Type u_2
A_1 : Type u_3
B_1 : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst : DivisionMonoid G
inst_1 : MulAction G A
x y : G
f : A → B
⊢ (x * y) • f = x • y • f
have change : Eq (α := (a : A) → B) (fun (a : A) ↦ f ((x * y)⁻¹ • a)) fun (a : A) ↦ f (y⁻¹ • x⁻¹ • a)
Tactic: change (fun a => f ((x * y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
G_1 : Type u_1
M : Type u_2
A_1 : Type u_3
B_1 : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst : DivisionMonoid G
inst_1 : MulAction G A
f : A → B
⊢ HSMul.hSMul (α := G) 1 f = f
have change : (fun (x : A) ↦ f (HSMul.hSMul.{u_7, u_8, u_8} (α := G) 1⁻¹ x)) = f
Tactic: change (fun x => f ((1 : G)⁻¹ • x)) = f
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
m : α
hm : IsUnit m
⊢ Function.Bijective (β := β) fun (a : β) ↦ m • a
have lift : ∀ (m : αˣ), Function.Bijective (β := β) fun (a : β) ↦ (↑m : α) • a
Tactic: lift m to αˣ using hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
inst_3 : Monoid B
inst_4 : SMul M B
f : A →* B
hf : Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
⊢ HSMul.hSMul (β := B) c 1 = 1
have rw : HSMul.hSMul (β := B) c ((f : (a : A) → B) 1 : B) = (f : (a : A) → B) 1
Tactic: rw [← f.map_one, ← smul, smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
inst_3 : Monoid B
inst_4 : SMul M B
f : A →* B
hf : Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
rw : HSMul.hSMul (β := B) c ((f : (a : A) → B) 1 : B) = (f : (a : A) → B) 1
⊢ HSMul.hSMul (β := B) c 1 = 1
have rw₁ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) (HSMul.hSMul (β := A) c 1) : B) ((f : (a : A) → B) 1 : B)
Tactic: rw [← f.map_one, ← smul, smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
inst_3 : Monoid B
inst_4 : SMul M B
f : A →* B
hf : Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
rw : HSMul.hSMul (β := B) c ((f : (a : A) → B) 1 : B) = (f : (a : A) → B) 1
rw₁ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) (HSMul.hSMul (β := A) c 1) : B) ((f : (a : A) → B) 1 : B)
⊢ HSMul.hSMul (β := B) c 1 = 1
have rw₂ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 1 : B) ((f : (a : A) → B) 1 : B)
Tactic: rw [← f.map_one, ← smul, smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α_1 : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
M : Type u_9
α : Type u_10
inst : CommMonoid M
inst_1 : MulAction M α
a a' : M
b : α
⊢ a • a' • b = a' • a • b
have rw : (a * a') • b = a' • a • b
Tactic: rw [← mul_smul, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α_1 : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
M : Type u_9
α : Type u_10
inst : CommMonoid M
inst_1 : MulAction M α
a a' : M
b : α
rw : (a * a') • b = a' • a • b
⊢ a • a' • b = a' • a • b
have rw₁ : (a' * a) • b = a' • a • b
Tactic: rw [← mul_smul, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α_1 : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
M : Type u_9
α : Type u_10
inst : CommMonoid M
inst_1 : MulAction M α
a a' : M
b : α
rw : (a * a') • b = a' • a • b
rw₁ : (a' * a) • b = a' • a • b
⊢ a • a' • b = a' • a • b
have rw₂ : a' • a • b = a' • a • b
Tactic: rw [← mul_smul, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
α : Type u_10
inst : SMul M α
inst_1 : SMul.{u_9, u_10} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
m : Mᵐᵒᵖ
a : α
⊢ MulOpposite.unop m • a = m • a
have h : ∀ (X : M), MulOpposite.unop (MulOpposite.op X) • a = MulOpposite.op X • a
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul.{u_1, u_5} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
inst_3 : SMul N α
inst_4 : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ m • n • a = n • m • a
have rw : MulOpposite.unop m • n • a = n • m • a
Tactic: rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul.{u_1, u_5} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
inst_3 : SMul N α
inst_4 : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
rw : MulOpposite.unop m • n • a = n • m • a
⊢ m • n • a = n • m • a
have rw₁ : MulOpposite.unop m • n • a = n • MulOpposite.unop m • a
Tactic: rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul.{u_1, u_5} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
inst_3 : SMul N α
inst_4 : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
rw : MulOpposite.unop m • n • a = n • m • a
rw₁ : MulOpposite.unop m • n • a = n • MulOpposite.unop m • a
⊢ m • n • a = n • m • a
have rw₂ : n • MulOpposite.unop m • a = n • MulOpposite.unop m • a
Tactic: rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMul.{u_2, u_5} Nᵐᵒᵖ α
inst_3 : IsCentralScalar N α
inst_4 : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • n • a = n • m • a
have rw : m • n • a = MulOpposite.unop n • m • a
Tactic: rw [← unop_smul_eq_smul n (m • a), ← unop_smul_eq_smul n a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMul.{u_2, u_5} Nᵐᵒᵖ α
inst_3 : IsCentralScalar N α
inst_4 : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
rw : m • n • a = MulOpposite.unop n • m • a
⊢ m • n • a = n • m • a
have rw₁ : m • MulOpposite.unop n • a = MulOpposite.unop n • m • a
Tactic: rw [← unop_smul_eq_smul n (m • a), ← unop_smul_eq_smul n a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMul.{u_2, u_5} Nᵐᵒᵖ α
inst_3 : IsCentralScalar N α
inst_4 : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
rw : m • n • a = MulOpposite.unop n • m • a
rw₁ : m • MulOpposite.unop n • a = MulOpposite.unop n • m • a
⊢ m • n • a = n • m • a
have rw₂ : MulOpposite.unop n • m • a = MulOpposite.unop n • m • a
Tactic: rw [← unop_smul_eq_smul n (m • a), ← unop_smul_eq_smul n a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul.{u_1, u_5} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
inst_3 : SMul M N
inst_4 : SMul.{u_1, u_2} Mᵐᵒᵖ N
inst_5 : IsCentralScalar M N
inst_6 : SMul N α
inst_7 : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = m • n • a
have rw : (m • n) • a = MulOpposite.unop m • n • a
Tactic: rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul.{u_1, u_5} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
inst_3 : SMul M N
inst_4 : SMul.{u_1, u_2} Mᵐᵒᵖ N
inst_5 : IsCentralScalar M N
inst_6 : SMul N α
inst_7 : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
rw : (m • n) • a = MulOpposite.unop m • n • a
⊢ (m • n) • a = m • n • a
have rw₁ : (MulOpposite.unop m • n) • a = MulOpposite.unop m • n • a
Tactic: rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul.{u_1, u_5} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
inst_3 : SMul M N
inst_4 : SMul.{u_1, u_2} Mᵐᵒᵖ N
inst_5 : IsCentralScalar M N
inst_6 : SMul N α
inst_7 : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
rw : (m • n) • a = MulOpposite.unop m • n • a
rw₁ : (MulOpposite.unop m • n) • a = MulOpposite.unop m • n • a
⊢ (m • n) • a = m • n • a
have rw₂ : MulOpposite.unop m • n • a = MulOpposite.unop m • n • a
Tactic: rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul M N
inst_2 : SMul N α
inst_3 : SMul.{u_2, u_5} Nᵐᵒᵖ α
inst_4 : IsCentralScalar N α
inst_5 : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ (m • n) • a = m • n • a
have rw : (m • n) • a = m • MulOpposite.unop n • a
Tactic: rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul M N
inst_2 : SMul N α
inst_3 : SMul.{u_2, u_5} Nᵐᵒᵖ α
inst_4 : IsCentralScalar N α
inst_5 : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
rw : (m • n) • a = m • MulOpposite.unop n • a
⊢ (m • n) • a = m • n • a
have rw₁ : MulOpposite.unop (m • n) • a = m • MulOpposite.unop n • a
Tactic: rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul M N
inst_2 : SMul N α
inst_3 : SMul.{u_2, u_5} Nᵐᵒᵖ α
inst_4 : IsCentralScalar N α
inst_5 : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
rw : (m • n) • a = m • MulOpposite.unop n • a
rw₁ : MulOpposite.unop (m • n) • a = m • MulOpposite.unop n • a
⊢ (m • n) • a = m • n • a
have rw₂ : (m • MulOpposite.unop n) • a = m • MulOpposite.unop n • a
Tactic: rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul M N
inst_2 : SMul N α
inst_3 : SMul.{u_2, u_5} Nᵐᵒᵖ α
inst_4 : IsCentralScalar N α
inst_5 : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
rw : (m • n) • a = m • MulOpposite.unop n • a
rw₁ : MulOpposite.unop (m • n) • a = m • MulOpposite.unop n • a
rw₂ : (m • MulOpposite.unop n) • a = m • MulOpposite.unop n • a
⊢ (m • n) • a = m • n • a
have rw₃ : m • MulOpposite.unop n • a = m • MulOpposite.unop n • a
Tactic: rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul α β
inst_3 : IsScalarTower M α β
g : N → M
⊢ Prop
have haveI : (this : SMul N α) → Prop
Tactic: haveI := comp α g
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul α β
inst_3 : IsScalarTower M α β
g : N → M
this : SMul N α
⊢ Prop
have haveI : (this : SMul N β) → Prop
Tactic: haveI := comp β g
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β δ
inst_3 : SMul α δ
inst_4 : SMul γ δ
inst_5 : IsScalarTower α β δ
inst_6 : IsScalarTower α γ δ
inst_7 : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ (a • b) • c • d = (a • c) • b • d
have rw : a • b • c • d = (a • c) • b • d
Tactic: rw [smul_assoc, smul_assoc, smul_comm b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β δ
inst_3 : SMul α δ
inst_4 : SMul γ δ
inst_5 : IsScalarTower α β δ
inst_6 : IsScalarTower α γ δ
inst_7 : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
rw : a • b • c • d = (a • c) • b • d
⊢ (a • b) • c • d = (a • c) • b • d
have rw₁ : a • b • c • d = a • c • b • d
Tactic: rw [smul_assoc, smul_assoc, smul_comm b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β δ
inst_3 : SMul α δ
inst_4 : SMul γ δ
inst_5 : IsScalarTower α β δ
inst_6 : IsScalarTower α γ δ
inst_7 : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
rw : a • b • c • d = (a • c) • b • d
rw₁ : a • b • c • d = a • c • b • d
⊢ (a • b) • c • d = (a • c) • b • d
have rw₂ : a • c • b • d = a • c • b • d
Tactic: rw [smul_assoc, smul_assoc, smul_comm b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (hypothesis)
Goal:
α : Type u_5
β : Type u_6
inst : Mul α
inst_1 : Mul β
inst_2 : SMul α β
inst_3 : IsScalarTower α β β
inst_4 : IsScalarTower α α β
inst_5 : SMulCommClass α β β
a : α
b : β
c : α
d : β
⊢ a • b * c • d = (a * c) • (b * d)
have this : SMulCommClass β α β
Tactic: have : SMulCommClass β α β := .symm ..
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy x (r • a) (r • b)
have rw : x * r • a = r • b * x
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
rw : x * r • a = r • b * x
⊢ SemiconjBy x (r • a) (r • b)
have rw₁ : r • (x * a) = r • b * x
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
rw : x * r • a = r • b * x
rw₁ : r • (x * a) = r • b * x
⊢ SemiconjBy x (r • a) (r • b)
have rw₂ : r • (x * a) = r • (b * x)
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
rw : x * r • a = r • b * x
rw₁ : r • (x * a) = r • b * x
rw₂ : r • (x * a) = r • (b * x)
⊢ SemiconjBy x (r • a) (r • b)
have rw₃ : r • (b * x) = r • (b * x)
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy (r • x) a b
have rw : r • x * a = b * r • x
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
rw : r • x * a = b * r • x
⊢ SemiconjBy (r • x) a b
have rw₁ : r • x * a = r • (b * x)
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
rw : r • x * a = b * r • x
rw₁ : r • x * a = r • (b * x)
⊢ SemiconjBy (r • x) a b
have rw₂ : r • (x * a) = r • (b * x)
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
rw : r • x * a = b * r • x
rw₁ : r • x * a = r • (b * x)
rw₂ : r • (x * a) = r • (b * x)
⊢ SemiconjBy (r • x) a b
have rw₃ : r • (b * x) = r • (b * x)
Tactic: rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
a : M
n : ℕ
⊢ Eq.{u_5 + 1} (α := α → α) (fun (x : α) ↦ a • x)^[n + 1] fun (x : α) ↦ a ^ (n + 1) • x
have h : ∀ (x : α), (fun (x : α) ↦ a • x)^[n + 1] x = a ^ (n + 1) • x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
a : M
n : ℕ
x : α
⊢ (fun (x : α) ↦ a • x)^[n] x = a ^ n • x
have rw : (fun (x : α) ↦ a ^ n • x) x = a ^ n • x
Tactic: rw [smul_iterate]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : Monoid M_1
inst_1 : MulAction M_1 α
a : M_1
R : Type u_9
M : Type u_10
inst_2 : CommMonoid M
inst_3 : SMul R M
inst_4 : IsScalarTower R M M
r : R
s x : M
⊢ r • s • x = s • r • x
have rw : r • HSMul.hSMul (α := M) 1 (s • x) = s • r • x
Tactic: rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : Monoid M_1
inst_1 : MulAction M_1 α
a : M_1
R : Type u_9
M : Type u_10
inst_2 : CommMonoid M
inst_3 : SMul R M
inst_4 : IsScalarTower R M M
r : R
s x : M
rw : r • HSMul.hSMul (α := M) 1 (s • x) = s • r • x
⊢ r • s • x = s • r • x
have rw₁ : HSMul.hSMul (β := M) r 1 • s • x = s • r • x
Tactic: rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : Monoid M_1
inst_1 : MulAction M_1 α
a : M_1
R : Type u_9
M : Type u_10
inst_2 : CommMonoid M
inst_3 : SMul R M
inst_4 : IsScalarTower R M M
r : R
s x : M
rw : r • HSMul.hSMul (α := M) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := M) r 1 • s • x = s • r • x
⊢ r • s • x = s • r • x
have rw₂ : s • HSMul.hSMul (β := M) r 1 • x = s • r • x
Tactic: rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : Monoid M_1
inst_1 : MulAction M_1 α
a : M_1
R : Type u_9
M : Type u_10
inst_2 : CommMonoid M
inst_3 : SMul R M
inst_4 : IsScalarTower R M M
r : R
s x : M
rw : r • HSMul.hSMul (α := M) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := M) r 1 • s • x = s • r • x
rw₂ : s • HSMul.hSMul (β := M) r 1 • x = s • r • x
⊢ r • s • x = s • r • x
have rw₃ : s • r • HSMul.hSMul (α := M) 1 x = s • r • x
Tactic: rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M_1 : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst : Monoid M_1
inst_1 : MulAction M_1 α
a : M_1
R : Type u_9
M : Type u_10
inst_2 : CommMonoid M
inst_3 : SMul R M
inst_4 : IsScalarTower R M M
r : R
s x : M
rw : r • HSMul.hSMul (α := M) 1 (s • x) = s • r • x
rw₁ : HSMul.hSMul (β := M) r 1 • s • x = s • r • x
rw₂ : s • HSMul.hSMul (β := M) r 1 • x = s • r • x
rw₃ : s • r • HSMul.hSMul (α := M) 1 x = s • r • x
⊢ r • s • x = s • r • x
have rw₄ : s • r • x = s • r • x
Tactic: rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]
-- 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 : ℕ
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
have rw : r • x * (r • x) ^ n = 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:
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)
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
have rw₁ : r • x * r ^ n • x ^ n = 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:
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)
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
have rw₂ : (r * r ^ n) • (x * x ^ n) = 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:
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)
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
have rw₃ : r ^ (n + 1) • (x * x ^ n) = r ^ (n + 1) • x ^ (n + 1)
Tactic: rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']