awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
g : α
⊢ Function.Surjective (β := β) fun (x : β) ↦ g • x

Tactic:
(MulAction.bijective g).surjective

Premises used: MulAction.bijective, Function.Bijective.surjective
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
g : α
x y : β
h : g • x = g • y
⊢ x = y

Tactic:
MulAction.injective g h

Premises used: MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
g : α
x y : β
⊢ g • x = g • y ↔ x = y

Tactic:
(MulAction.injective g).eq_iff

Premises used: Function.Injective.eq_iff, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
g : α
x y : β
⊢ g • x = y ↔ x = g⁻¹ • y

Tactic:
(MulAction.toPerm g).apply_eq_iff_eq_symm_apply

Premises used: MulAction.toPerm, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
⊢ IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1

Tactic:
⟨fun H _ _ ↦ IsCancelSMul.eq_one_of_smul, fun H ↦ ⟨fun g h x ↦ ?_⟩⟩

Premises used: Iff.intro, IsCancelSMul.mk, IsCancelSMul.eq_one_of_smul
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
refine : ∀ (H : ∀ (g : α) (x : β), g • x = x → g = 1) (g h : α) (x : β), g • x = h • x → g = h
⊢ IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1

Tactic:
refine ⟨fun H _ _ ↦ IsCancelSMul.eq_one_of_smul, fun H ↦ ⟨fun g h x ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
rw : (g⁻¹ * h) • x = x → g⁻¹ * h = 1
⊢ g • x = h • x → g = h

Tactic:
rw [smul_eq_iff_eq_inv_smul, eq_comm, ← mul_smul, ← inv_mul_eq_one (G := α)]

Premises used: eq_comm, smul_eq_iff_eq_inv_smul, SemigroupAction.mul_smul, inv_mul_eq_one
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ (g⁻¹ * h) • x = x → g⁻¹ * h = 1

Tactic:
H (g⁻¹ * h) x

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ (g⁻¹ * h) • x = x → g⁻¹ * h = 1

Tactic:
exact H (g⁻¹ * h) x

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
c : α
x : β
inst_2 : Invertible c
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • x = x

Tactic:
inv_smul_smul (unitOfInvertible c) _

Premises used: inv_smul_smul, unitOfInvertible
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
c : α
x : β
inst_2 : Invertible c
⊢ c • @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • x = x

Tactic:
smul_inv_smul (unitOfInvertible c) _

Premises used: smul_inv_smul, unitOfInvertible
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
c : α
x y : β
inst_2 : Invertible c
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • x = y ↔ x = c • y

Tactic:
inv_smul_eq_iff (g := unitOfInvertible c)

Premises used: inv_smul_eq_iff
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
c : α
x y : β
inst_2 : Invertible c
⊢ c • x = y ↔ x = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • y

Tactic:
smul_eq_iff_eq_inv_smul (g := unitOfInvertible c)

Premises used: unitOfInvertible, smul_eq_iff_eq_inv_smul
-- Module: Mathlib.Algebra.Group.Action.Basic
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
change : Eq (α := (a : A) → B) (fun (a : A) ↦ f ((x * y)⁻¹ • a)) fun (a : A) ↦ f (y⁻¹ • x⁻¹ • a)
⊢ (x * y) • f = x • y • f

Tactic:
change (fun a => f ((x * y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))

Premises used: HMul.hMul, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.Group.Action.Basic
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
⊢ Eq (α := (a : A) → B) (fun (a : A) ↦ f ((x * y)⁻¹ • a)) fun (a : A) ↦ f (y⁻¹ • x⁻¹ • a)

Tactic:
simp only [mul_smul, mul_inv_rev]

Premises used: mul_inv_rev, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Basic
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
change : (fun (x : A) ↦ f (HSMul.hSMul.{u_7, u_8, u_8} (α := G) 1⁻¹ x)) = f
⊢ HSMul.hSMul (α := G) 1 f = f

Tactic:
change (fun x => f ((1 : G)⁻¹ • x)) = f

Premises used: Inv.inv, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Basic
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
⊢ (fun (x : A) ↦ f (HSMul.hSMul.{u_7, u_8, u_8} (α := G) 1⁻¹ x)) = f

Tactic:
simp only [inv_one, one_smul]

Premises used: inv_one, one_smul
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
m : α
hm : IsUnit m
⊢ IsUnit m

Tactic:
hm
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
m : α
hm : IsUnit m
lift : ∀ (m : αˣ), Function.Bijective (β := β) fun (a : β) ↦ (↑m : α) • a
⊢ Function.Bijective (β := β) fun (a : β) ↦ m • a

Tactic:
lift m to αˣ using hm
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
m : αˣ
⊢ Function.Bijective (β := β) fun (a : β) ↦ (↑m : α) • a

Tactic:
MulAction.bijective m

Premises used: MulAction.bijective
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
m : αˣ
⊢ Function.Bijective (β := β) fun (a : β) ↦ (↑m : α) • a

Tactic:
exact MulAction.bijective m

Premises used: MulAction.bijective
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : MulAction α β
a : α
ha : IsUnit a
x y : β
⊢ a • x = a • y ↔ x = y

Tactic:
let ⟨u, hu⟩ := ha
  hu ▸ smul_left_cancel_iff u

Premises used: Eq.rec, _private.0.IsUnit.smul_left_cancel.match_1, Iff, HSMul.hSMul, Eq, smul_left_cancel_iff
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction α β
inst_3 : SMulCommClass α β β
inst_4 : IsScalarTower α β β
g : α
m : β
⊢ IsUnit (g • m) ↔ IsUnit m

Tactic:
⟨fun h => inv_smul_smul g m ▸ h.smul g⁻¹, IsUnit.smul g⟩

Premises used: Eq.rec, inv_smul_smul, Inv.inv, Iff.intro, IsUnit.smul
-- Module: Mathlib.Algebra.Group.Action.Basic
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 : MulAction M α
y₁ y₂ : α
H : Eq (α := M → α) ((fun (y : α) (x : M) ↦ x • y) y₁) ((fun (y : α) (x : M) ↦ x • y) y₂)
⊢ Eq.{u_5 + 1} (α := α) ((fun (y : α) (x : M) ↦ x • y) y₁ 1) ((fun (y : α) (x : M) ↦ x • y) y₂ 1)

Tactic:
congr_fun H 1

Premises used: congr_fun, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Basic
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 : MulAction M α
y₁ y₂ : α
H : Eq (α := M → α) ((fun (y : α) (x : M) ↦ x • y) y₁) ((fun (y : α) (x : M) ↦ x • y) y₂)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := M) 1 y₁ = HSMul.hSMul.{u_2, u_5, u_5} (α := M) 1 y₂

Tactic:
convert! congr_fun H 1

Premises used: congr_fun, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
M : Type u_2
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
x : M
y : α
⊢ (toFun M α : (a : α) → M → α) y x = x • y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Basic
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 : B →* A
hf : Injective.{u_4 + 1, u_3 + 1} (α := B) (β := A) (⇑f : (a : B) → A)
smul : ∀ (c : M) (x : B), (f : (a : B) → A) (c • x) = HSMul.hSMul (β := A) c ((f : (a : B) → A) x : A)
c : M
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : B) → A) (HSMul.hSMul (β := B) c 1) : A) ((f : (a : B) → A) 1 : A)

Tactic:
simp only [smul, f.map_one, smul_one]

Premises used: MulDistribMulAction.smul_one, MonoidHom.map_one
-- Module: Mathlib.Algebra.Group.Action.Basic
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 : B →* A
hf : Injective.{u_4 + 1, u_3 + 1} (α := B) (β := A) (⇑f : (a : B) → A)
smul : ∀ (c : M) (x : B), (f : (a : B) → A) (c • x) = HSMul.hSMul (β := A) c ((f : (a : B) → A) x : A)
c : M
x y : B
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : B) → A) (c • (x * y)) : A) ((f : (a : B) → A) (c • x * c • y) : A)

Tactic:
simp only [smul, f.map_mul, smul_mul']

Premises used: MonoidHom.map_mul, smul_mul'
-- Module: Mathlib.Algebra.Group.Action.Basic
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)
rw₂ rw₃ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 1 : B) ((f : (a : A) → B) 1 : B)
⊢ HSMul.hSMul (β := B) c 1 = 1

Tactic:
rw [← f.map_one, ← smul, smul_one]

Premises used: MulDistribMulAction.smul_one, MonoidHom.map_one
-- Module: Mathlib.Algebra.Group.Action.Basic
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
⊢ ∀ (x y : B), c • (x * y) = c • x * c • y

Tactic:
simp only [hf.forall, smul_mul', ← smul, ← f.map_mul, implies_true]

Premises used: Function.Surjective.forall, implies_true, MonoidHom.map_mul, smul_mul'
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
M : Type u_2
A : Type u_3
inst : Monoid M
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
r : M
x : A
n : ℕ
⊢ r • x ^ n = (r • x) ^ n

Tactic:
(MulDistribMulAction.toMonoidHom _ _).map_pow _ _

Premises used: MulDistribMulAction.toMonoidHom, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
M : Type u_2
A : Type u_3
inst : Monoid M
inst_1 : Group A
inst_2 : MulDistribMulAction M A
r : M
x : A
⊢ r • x⁻¹ = (r • x)⁻¹

Tactic:
(MulDistribMulAction.toMonoidHom A r).map_inv x

Premises used: MonoidHom.map_inv, MulDistribMulAction.toMonoidHom
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
M : Type u_2
A : Type u_3
inst : Monoid M
inst_1 : Group A
inst_2 : MulDistribMulAction M A
r : M
x y : A
⊢ r • (x / y) = r • x / r • y

Tactic:
map_div (MulDistribMulAction.toMonoidHom A r) x y

Premises used: map_div, MulDistribMulAction.toMonoidHom
-- Module: Mathlib.Algebra.Group.Action.Basic
Goal:
M : Type u_2
A : Type u_3
inst : Monoid M
inst_1 : Group A
inst_2 : MulDistribMulAction M A
r : M
x : A
z : ℤ
⊢ r • x ^ z = (r • x) ^ z

Tactic:
map_zpow (MulDistribMulAction.toMonoidHom A r) x z

Premises used: map_zpow, MulDistribMulAction.toMonoidHom
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
α : Type u_9
inst : Mul α
a b : α
⊢ a • b = a * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
α : Type u_9
inst : Mul α
a b : α
⊢ MulOpposite.op a • b = b * a

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
α : Type u_5
inst : Mul α
a : αᵐᵒᵖ
b : α
⊢ a • b = b * unop a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMul M β
inst_3 : SMul N β
inst_4 : SMulCommClass M N β
f : α → β
hf : Injective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ f (c₁ • c₂ • x) = f (c₂ • c₁ • x)

Tactic:
simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMul M β
inst_3 : SMul N β
inst_4 : SMulCommClass M N α
f : α → β
hf : Surjective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ c₁ • c₂ • f x = c₂ • c₁ • f x

Tactic:
simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₂ rw₃ : a' • a • b = a' • a • b
⊢ a • a' • b = a' • a • b

Tactic:
rw [← mul_smul, mul_comm, mul_smul]

Premises used: mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
α : Type u_5
M : Type u_9
N : Type u_10
inst : SMul M N
inst_1 : SMul N α
inst_2 : SMul M α
inst_3 : IsScalarTower M N α
x : M
y : N
z : α
⊢ (x • y) • z = x • y • z

Tactic:
IsScalarTower.smul_assoc x y z

Premises used: IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Defs
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 : Semigroup α
⊢ IsScalarTower α α α

Tactic:
⟨mul_assoc⟩

Premises used: mul_assoc, IsScalarTower.mk
-- Module: Mathlib.Algebra.Group.Action.Defs
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 : α
h : ∀ (X : M), MulOpposite.unop (MulOpposite.op X) • a = MulOpposite.op X • a
⊢ MulOpposite.unop m • a = m • a

Tactic:
induction m
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_9
α : Type u_10
inst : SMul M α
inst_1 : SMul.{u_9, u_10} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
a : α
X : M
⊢ MulOpposite.unop (MulOpposite.op X) • a = MulOpposite.op X • a

Tactic:
(IsCentralScalar.op_smul_eq_smul _ a).symm

Premises used: MulOpposite.unop, Eq.symm, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_9
α : Type u_10
inst : SMul M α
inst_1 : SMul.{u_9, u_10} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
a : α
X : M
⊢ MulOpposite.unop (MulOpposite.op X) • a = MulOpposite.op X • a

Tactic:
exact (IsCentralScalar.op_smul_eq_smul _ a).symm

Premises used: Eq.symm, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₂ rw₃ : n • MulOpposite.unop m • a = n • MulOpposite.unop m • a
⊢ m • n • a = n • m • a

Tactic:
rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]

Premises used: IsCentralScalar.unop_smul_eq_smul, HSMul.hSMul, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₂ rw₃ : MulOpposite.unop n • m • a = MulOpposite.unop n • m • a
⊢ m • n • a = n • m • a

Tactic:
rw [← unop_smul_eq_smul n (m • a), ← unop_smul_eq_smul n a, smul_comm]

Premises used: IsCentralScalar.unop_smul_eq_smul, HSMul.hSMul, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₂ rw₃ : MulOpposite.unop m • n • a = MulOpposite.unop m • n • a
⊢ (m • n) • a = m • n • a

Tactic:
rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]

Premises used: IsCentralScalar.unop_smul_eq_smul, HSMul.hSMul, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₃ rw₄ : m • MulOpposite.unop n • a = m • MulOpposite.unop n • a
⊢ (m • n) • a = m • n • a

Tactic:
rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]

Premises used: IsCentralScalar.unop_smul_eq_smul, MulOpposite.unop_smul, HSMul.hSMul, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Defs
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
haveI : (this : SMul N α) → Prop
⊢ Prop

Tactic:
haveI := comp α g
-- Module: Mathlib.Algebra.Group.Action.Defs
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 α
haveI : (this : SMul N β) → Prop
⊢ Prop

Tactic:
haveI := comp β g
-- Module: Mathlib.Algebra.Group.Action.Defs
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_1 : SMul N α
this : SMul N β
⊢ Prop

Tactic:
exact IsScalarTower N α β

Premises used: IsScalarTower
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
α : Type u_5
β : Type u_6
inst : Mul β
inst_1 : SMul α β
inst_2 : SMulCommClass α β β
s : α
x y : β
⊢ x * s • y = s • (x * y)

Tactic:
(smul_comm s x y).symm

Premises used: SMulCommClass.smul_comm, Eq.symm
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
α : Type u_5
β : Type u_6
inst : Mul β
inst_1 : SMul α β
inst_2 : IsScalarTower α β β
r : α
x y : β
⊢ r • x * y = r • (x * y)

Tactic:
smul_assoc r x y

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
α : Type u_5
β : Type u_6
inst : DivInvMonoid β
inst_1 : SMul α β
inst_2 : IsScalarTower α β β
r : α
x y : β
⊢ r • x / y = r • (x / y)

Tactic:
simp [div_eq_mul_inv, smul_mul_assoc]

Premises used: smul_mul_assoc, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₂ rw₃ : a • c • b • d = a • c • b • d
⊢ (a • b) • c • d = (a • c) • b • d

Tactic:
rw [smul_assoc, smul_assoc, smul_comm b]

Premises used: smul_assoc, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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 : β
⊢ SMulCommClass β α β

Tactic:
have : SMulCommClass β α β := .symm ..
-- Module: Mathlib.Algebra.Group.Action.Defs
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 : β
this : SMulCommClass β α β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
smul_smul_smul_comm a b c d

Premises used: smul_smul_smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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 : β
this : SMulCommClass β α β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
exact smul_smul_smul_comm a b c d

Premises used: smul_smul_smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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

Tactic:
smul_smul_smul_comm a b c d

Premises used: smul_smul_smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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)
rw₃ rw₄ : r • (b * x) = r • (b * x)
⊢ SemiconjBy x (r • a) (r • b)

Tactic:
rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]

Premises used: SemiconjBy, smul_mul_assoc, SemiconjBy.eq, mul_smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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)
rw₃ rw₄ : r • (b * x) = r • (b * x)
⊢ SemiconjBy (r • x) a b

Tactic:
rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]

Premises used: SemiconjBy, smul_mul_assoc, SemiconjBy.eq, mul_smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
a b : α
h : Commute a b
r : M
⊢ Commute a (r • b)

Tactic:
SemiconjBy.smul_right h r

Premises used: Commute, SemiconjBy.smul_right
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : SMul M α
inst_1 : Mul α
inst_2 : SMulCommClass M α α
inst_3 : IsScalarTower M α α
a b : α
h : Commute a b
r : M
⊢ Commute (r • a) b

Tactic:
SemiconjBy.smul_left h r

Premises used: Commute, SemiconjBy.smul_left
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
b : α
⊢ a₁ • a₂ • b = (a₁ * a₂) • b

Tactic:
(mul_smul _ _ _).symm

Premises used: Eq.symm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
b : α
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 b = b

Tactic:
MulAction.one_smul _

Premises used: MulAction.one_smul