awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
⊢ Eq.{u_5 + 1} (α := α → α) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 x) id

Tactic:
funext <| one_smul _

Premises used: one_smul, funext
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
⊢ Eq.{u_5 + 1} (α := α → α) ((fun (x : α) ↦ a₁ • x) ∘ fun (x : α) ↦ a₂ • x) fun (x : α) ↦ (a₁ * a₂) • x

Tactic:
funext fun _ ↦ (mul_smul _ _ _).symm

Premises used: funext, 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 α
a : M
⊢ Eq.{u_5 + 1} (α := α → α) (fun (x : α) ↦ a • x)^[0] fun (x : α) ↦ HPow.hPow (β := ℕ) a 0 • x

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
a : M
n : ℕ
h : ∀ (x : α), (fun (x : α) ↦ a • x)^[n + 1] x = a ^ (n + 1) • x
⊢ Eq.{u_5 + 1} (α := α → α) (fun (x : α) ↦ a • x)^[n + 1] fun (x : α) ↦ a ^ (n + 1) • x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
a : M
n : ℕ
x : α
⊢ (fun (x : α) ↦ a • x)^[n + 1] x = a ^ (n + 1) • x

Tactic:
simp [smul_iterate, pow_succ, smul_smul]

Premises used: pow_succ, smul_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
α : Type u_5
inst : Monoid M
inst_1 : MulAction M α
a : M
n : ℕ
x : α
rw rw₁ : (fun (x : α) ↦ a ^ n • x) x = a ^ n • x
⊢ (fun (x : α) ↦ a • x)^[n] x = a ^ n • x

Tactic:
rw [smul_iterate]

Premises used: smul_iterate
-- 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 : Monoid M
inst_1 : MulAction M α
a : M
inst_2 : SMul M β
f : β → α
hf : Injective f
smul : ∀ (c : M) (x : β), f (c • x) = c • f x
c₁ c₂ : M
x : β
⊢ f ((c₁ * c₂) • x) = f (c₁ • c₂ • x)

Tactic:
simp only [smul, mul_smul]

Premises used: SemigroupAction.mul_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 : Monoid M
inst_1 : MulAction M α
a : M
inst_2 : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
⊢ ∀ (x y : M) (b : β), (x * y) • b = x • y • b

Tactic:
simp [hf.forall, ← smul, mul_smul]

Premises used: Function.Surjective.forall, SemigroupAction.mul_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 : Monoid M
inst_1 : MulAction M α
a : M
inst_2 : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
⊢ ∀ (b : β), HSMul.hSMul.{u_1, u_6, u_6} (α := M) 1 b = b

Tactic:
simp [hf.forall, ← smul]

Premises used: Function.Surjective.forall
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₄ rw₅ : s • r • x = s • r • x
⊢ r • s • x = s • r • x

Tactic:
rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]

Premises used: smul_assoc, one_smul, HSMul.hSMul, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
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
⊢ HPow.hPow (β := ℕ) (r • x) 0 = HPow.hPow (β := ℕ) r 0 • HPow.hPow (β := ℕ) x 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Action.Defs
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)
rw₄ rw₅ : r ^ (n + 1) • x ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']

Premises used: smul_mul_smul_comm, pow_succ'
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₂ rw₃ : a = a
⊢ g⁻¹ • g • a = a

Tactic:
rw [smul_smul, inv_mul_cancel, one_smul]

Premises used: inv_mul_cancel, smul_smul, one_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₂ rw₃ : a = a
⊢ g • g⁻¹ • a = a

Tactic:
rw [smul_smul, mul_inv_cancel, one_smul]

Premises used: smul_smul, one_smul, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₁ rw₂ : a = a
⊢ a = g • b

Tactic:
rw [← h, smul_inv_smul]

Premises used: smul_inv_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₁ rw₂ : b = b
⊢ g⁻¹ • a = b

Tactic:
rw [h, inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₁ rw₂ : b = b
⊢ g • a = b

Tactic:
rw [h, smul_inv_smul]

Premises used: smul_inv_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₁ rw₂ : a = a
⊢ a = g⁻¹ • b

Tactic:
rw [← h, inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Mul H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy x (r • a) (r • b)
⊢ SemiconjBy x a b

Tactic:
simpa using h.smul_right r⁻¹

Premises used: Inv.inv, SemiconjBy.smul_right
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Mul H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy (r • x) a b
⊢ SemiconjBy x a b

Tactic:
simpa using h.smul_left r⁻¹

Premises used: Inv.inv, SemiconjBy.smul_left
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_3
H : Type u_4
inst : Group G
g : G
inst_1 : Mul H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
a b : H
⊢ Commute a (g • b) ↔ Commute a b

Tactic:
SemiconjBy.smul_right_iff

Premises used: Commute, SemiconjBy.smul_right_iff
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_3
H : Type u_4
inst : Group G
g : G
inst_1 : Mul H
inst_2 : MulAction G H
inst_3 : SMulCommClass G H H
inst_4 : IsScalarTower G H H
a b : H
⊢ Commute (g • a) b ↔ Commute a b

Tactic:
SemiconjBy.smul_left_iff

Premises used: Commute, SemiconjBy.smul_left_iff
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₃ rw₄ : Eq.{u_4 + 1} (α := H) 1 1
⊢ g • a * g⁻¹ • a⁻¹ = 1

Tactic:
rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]

Premises used: smul_mul_smul_comm, one_smul, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Action.Defs
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
negSucc : ∀ (a_1 : ℕ), (g • a) ^ Int.negSucc a_1 = g ^ Int.negSucc a_1 • a ^ Int.negSucc a_1
⊢ (g • a) ^ n = g ^ n • a ^ n

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.Action.Defs
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
a_1 : ℕ
⊢ (g • a) ^ Int.ofNat a_1 = g ^ Int.ofNat a_1 • a ^ Int.ofNat a_1

Tactic:
simp [smul_pow, smul_inv]

Premises used: smul_pow, smul_inv
-- Module: Mathlib.Algebra.Group.Action.Defs
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
a_1 : ℕ
⊢ (g • a) ^ Int.negSucc a_1 = g ^ Int.negSucc a_1 • a ^ Int.negSucc a_1

Tactic:
simp [smul_pow, smul_inv]

Premises used: smul_pow, smul_inv
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₈ rw₉ : s • r • x = s • r • x
⊢ r • 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]

Premises used: smul_assoc, one_smul, HSMul.hSMul, SMulCommClass.smul_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₆ rw₇ : x₁ • y • z = x₁ • y • z
⊢ (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]

Premises used: mul_comm, smul_eq_mul, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
R₁ : Type u_9
R : Type u_10
inst : Monoid R₁
inst_1 : CommMonoid R
inst_2 : MulAction R₁ R
⊢ SMulCommClass R₁ R R ↔ IsScalarTower R₁ R R

Tactic:
⟨fun _ ↦ IsScalarTower.of_commMonoid R₁ R, fun _ ↦ SMulCommClass.of_commMonoid R₁ R R⟩

Premises used: SMulCommClass.of_commMonoid, Iff.intro, IsScalarTower.of_commMonoid
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₁ rw₂ : x • y = x • y
⊢ HSMul.hSMul (β := N) x 1 • y = x • y

Tactic:
rw [smul_assoc, one_smul]

Premises used: smul_assoc, one_smul
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₁ rw₂ : x • y = x • y
⊢ HSMul.hSMul (β := N) x 1 * y = x • y

Tactic:
rw [smul_mul_assoc, one_mul]

Premises used: smul_mul_assoc, one_mul
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₃ rw₄ : x • y = x • y
⊢ y * HSMul.hSMul (β := N) x 1 = x • y

Tactic:
rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]

Premises used: smul_eq_mul, SMulCommClass.smul_comm, mul_one
-- Module: Mathlib.Algebra.Group.Action.Defs
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
rw₄ rw₅ : x • (y * z) = x • (y * z)
⊢ (x • y) • z = x • y • z

Tactic:
rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]

Premises used: mul_assoc, smul_eq_mul
-- Module: Mathlib.Algebra.Group.Action.Defs
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)
rw₃ : y * z * HSMul.hSMul (β := N) x 1 = y * (z * HSMul.hSMul (β := N) x 1)
rw₄ rw₅ : y * (z * HSMul.hSMul (β := N) x 1) = y * (z * HSMul.hSMul (β := N) x 1)
⊢ x • y • z = y • x • z

Tactic:
rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, smul_eq_mul
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul N P
inst_4 : SMul N Q
inst_5 : Monoid P
inst_6 : MulAction P Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M P Q
inst_9 : IsScalarTower N P Q
m : M
n : N
q : Q
rw : HSMul.hSMul (β := P) (m • n) 1 • q = m • n • q
rw₁ : (m • HSMul.hSMul (β := P) n 1) • q = m • n • q
rw₂ : m • HSMul.hSMul (β := P) n 1 • q = m • n • q
rw₃ rw₄ : m • n • q = m • n • q
⊢ (m • n) • q = m • n • q

Tactic:
rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]

Premises used: smul_one_smul, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower N P Q
m : M
p : P
q : Q
rw : (HSMul.hSMul (β := N) m 1 • p) • q = m • p • q
rw₁ : HSMul.hSMul (β := N) m 1 • p • q = m • p • q
rw₂ rw₃ : m • p • q = m • p • q
⊢ (m • p) • q = m • p • q

Tactic:
rw [← smul_one_smul N m, smul_assoc, smul_one_smul]

Premises used: smul_one_smul, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower M P Q
h : Surjective.{u_9 + 1, u_10 + 1} (β := N) fun (m : M) ↦ HSMul.hSMul (β := N) m 1
n : N
p : P
q : Q
obtain :
  ∀ (m : M),
    HSMul.hSMul.{u_10, u_11, u_11} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) p • q =
      HSMul.hSMul.{u_10, u_12, u_12} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) (p • q)
⊢ (n • p) • q = n • p • q

Tactic:
obtain ⟨m, rfl⟩ := h n

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower M P Q
h : Surjective.{u_9 + 1, u_10 + 1} (β := N) fun (m : M) ↦ HSMul.hSMul (β := N) m 1
p : P
q : Q
m : M
simp_rw simp_rw₁ : (HSMul.hSMul (β := N) m 1 • p) • q = HSMul.hSMul (β := N) m 1 • p • q
simp_rw₂ : (m • p) • q = m • p • q
⊢ HSMul.hSMul.{u_10, u_11, u_11} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) p • q =
    HSMul.hSMul.{u_10, u_12, u_12} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) (p • q)

Tactic:
simp_rw [smul_one_smul, smul_assoc]

Premises used: smul_one_smul, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulDistribMulAction M N
a : M
b₁ b₂ : N
⊢ a • (b₁ * b₂) = a • b₁ * a • b₂

Tactic:
MulDistribMulAction.smul_mul ..

Premises used: MulDistribMulAction.smul_mul
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_11
P : Type u_12
inst : SMul G P
inst_1 : IsLeftCancelSMul G P
a : G
b c : P
⊢ a • b = a • c → b = c

Tactic:
IsLeftCancelSMul.left_cancel' a b c

Premises used: IsLeftCancelSMul.left_cancel'
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_11
P : Type u_12
inst : SMul G P
inst_1 : IsCancelSMul G P
a : G
b c : P
⊢ a • b = a • c → b = c

Tactic:
IsLeftCancelSMul.left_cancel' a b c

Premises used: IsLeftCancelSMul.left_cancel'
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_11
P : Type u_12
inst : SMul G P
inst_1 : IsCancelSMul G P
a b : G
c : P
⊢ a • c = b • c → a = b

Tactic:
IsCancelSMul.right_cancel' a b c

Premises used: IsCancelSMul.right_cancel'
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
G : Type u_11
P : Type u_12
inst : Monoid G
inst_1 : MulAction G P
inst_2 : IsCancelSMul G P
g : G
x : P
h : g • x = x
⊢ g = 1

Tactic:
IsCancelSMul.right_cancel g 1 x ((one_smul G x).symm ▸ h)

Premises used: IsCancelSMul.right_cancel, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Defs
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst : Group G
inst_1 : MulAction G P
a : G
b c : P
h : a • b = a • c
rw : a⁻¹ • a • b = c
rw₁ : a⁻¹ • a • c = c
rw₂ rw₃ : c = c
⊢ b = c

Tactic:
rw [← inv_smul_smul a b, h, inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
α : Type u_5
f : Function.End α
a : α
⊢ f • a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
α : Type u_5
f g : Function.End α
⊢ f * g = f ∘ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
α : Type u_5
⊢ Eq.{u_5 + 1} (α := Function.End α) 1 id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
α : Type u_6
f : Perm α
a : α
⊢ f • a = (f : (a : α) → α) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α_1 : Type u_5
α : Type u_6
⊢ FaithfulSMul (Perm α) α

Tactic:
⟨Equiv.ext⟩

Premises used: Equiv.ext, FaithfulSMul.mk
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
rw : ∀ (x y : α), ∃ (g : Perm α), g • x = y
⊢ MulAction.IsPretransitive (Perm α) α

Tactic:
rw [MulAction.isPretransitive_iff]

Premises used: MulAction.isPretransitive_iff
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
x y : α
h : swap x y • x = y
⊢ ∃ (g : Perm α), g • x = y

Tactic:
use Equiv.swap x y

Premises used: Equiv.swap
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
x y : α
⊢ swap x y • x = y

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
intro intro₁ : ∀ (x y : α), ∃ (g : Perm α), g • x = y
h : ∀ (x y : α), swap x y • x = y
⊢ ∀ (x y : α), ∃ (g : Perm α), g • x = y

Tactic:
classical
  intro x y
  use Equiv.swap x y
  simp
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
M : Type u_2
inst : Monoid M
f : MulAut M
a : M
⊢ f • a = (f : (a : M) → M) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
M : Type u_2
inst : AddMonoid M
f : AddAut M
a : M
⊢ f • a = (f : (a : M) → M) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
α : Type u_5
inst : Group G
inst_1 : MulAction G α
⊢ Eq (α := (a : G) → Equiv.Perm α) (⇑(toPermHom G α) : (a : G) → Equiv.Perm α) toPerm

Tactic:
rfl

Premises used: MulAction.toPerm, rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
α : Type u_5
inst : Group G
inst_1 : MulAction G α
⊢ Eq.{u_5 + 1} (α := Equiv.Perm α) (toPerm.{u_1, u_5} (α := G) 1) 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
α : Type u_5
inst : AddGroup G
inst_1 : AddAction G α
⊢ Eq (α := (a : G) → Additive (Equiv.Perm α)) (⇑(toPermHom G α) : (a : G) → Additive (Equiv.Perm α)) toPerm

Tactic:
rfl

Premises used: MulAction.toPerm, AddAction.toPerm, rfl
-- Module: Mathlib.Algebra.Group.Action.End
Goal:
G : Type u_1
α : Type u_5
inst : AddGroup G
inst_1 : AddAction G α
⊢ Eq.{u_5 + 1} (α := Equiv.Perm α) (toPerm.{u_1, u_5} (α := G) 0) 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
⊢ IsDecompOn (↑f.toPartialEquiv : X → X) f.source f.witness

Tactic:
f.isDecompOn'.choose_spec

Premises used: Exists.choose_spec, Equidecomp.isDecompOn', Equidecomp.witness
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
x : X
h : x ∈ f.source
⊢ (↑f.toPartialEquiv : X → X) x ∈ f.target

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
toPartialEquiv : PartialEquiv X X
w : Finset G
h : IsDecompOn (↑toPartialEquiv : X → X) toPartialEquiv.source w
_ :
  ∀ ⦃a₂ : Equidecomp X G⦄,
    { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G }.toPartialEquiv = a₂.toPartialEquiv →
      { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G } = a₂
⊢ ∀ ⦃a₂ : Equidecomp X G⦄,
    { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G }.toPartialEquiv = a₂.toPartialEquiv →
      { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G } = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
toPartialEquiv : PartialEquiv X X
w : Finset G
h : IsDecompOn (↑toPartialEquiv : X → X) toPartialEquiv.source w
a₂ : Equidecomp X G
_ :
  { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G }.toPartialEquiv = a₂.toPartialEquiv →
    { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G } = a₂
⊢ { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G }.toPartialEquiv = a₂.toPartialEquiv →
    { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G } = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
toPartialEquiv : PartialEquiv X X
w : Finset G
h : IsDecompOn (↑toPartialEquiv : X → X) toPartialEquiv.source w
a₂ : Equidecomp X G
h_1 : { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G }.toPartialEquiv = a₂.toPartialEquiv
⊢ { toPartialEquiv := toPartialEquiv, isDecompOn' := ⋯ : Equidecomp X G } = a₂

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
rw : ∃ g ∈ S, f a = g • a
⊢ ∃ g ∈ S, f' a = g • a

Tactic:
rw [← hf' ha]
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
⊢ ∃ g ∈ S, f a = g • a

Tactic:
h a (hA' ha)