awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : CommGroup β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
x : α × β
s : Set α
f : F
h :
  ∀ (a : α) (b : β),
    (a, b) ∈ HSMul.hSMul (β := Set (α × β)) x (graphOn (⇑f : (a : α) → β) s) ↔
      Membership.mem (γ := Set (α × β))
        (graphOn
          (fun (a : α) ↦
            HMul.hMul (β := β) (HDiv.hDiv (β := β) x.2 ((f : (a : α) → β) x.1 : β)) ((f : (a : α) → β) a : β))
          (x.1 • s))
        (a, b)
⊢ HSMul.hSMul (β := Set (α × β)) x (graphOn (⇑f : (a : α) → β) s) =
    graphOn
      (fun (a : α) ↦ HMul.hMul (β := β) (HDiv.hDiv (β := β) x.2 ((f : (a : α) → β) x.1 : β)) ((f : (a : α) → β) a : β))
      (x.1 • s)

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : CommGroup β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
x : α × β
s : Set α
f : F
a : α
b : β
⊢ (a, b) ∈ HSMul.hSMul (β := Set (α × β)) x (graphOn (⇑f : (a : α) → β) s) ↔
    Membership.mem (γ := Set (α × β))
      (graphOn
        (fun (a : α) ↦
          HMul.hMul (β := β) (HDiv.hDiv (β := β) x.2 ((f : (a : α) → β) x.1 : β)) ((f : (a : α) → β) a : β))
        (x.1 • s))
      (a, b)

Tactic:
simp [mem_smul_set_iff_inv_smul_mem, inv_mul_eq_iff_eq_mul, mul_left_comm _ _⁻¹,
    eq_inv_mul_iff_mul_eq, ← mul_div_right_comm, div_eq_iff_eq_mul, mul_comm b]

Premises used: mul_left_comm, eq_inv_mul_iff_mul_eq, mul_div_right_comm, Inv.inv, div_eq_iff_eq_mul, mul_comm, Set.mem_smul_set_iff_inv_smul_mem, inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : CommGroup β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
x : α × β
f : F
⊢ HSMul.hSMul (β := Set (α × β)) x (graphOn (⇑f : (a : α) → β) univ) =
    graphOn
      (fun (a : α) ↦ HMul.hMul (β := β) (HDiv.hDiv (β := β) x.2 ((f : (a : α) → β) x.1 : β)) ((f : (a : α) → β) a : β))
      univ

Tactic:
simp [smul_graphOn]

Premises used: Set.smul_graphOn
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : CommGroup α
a : α
s : Set α
b : α
t : Set α
simp_rw :
  HDiv.hDiv (α := Set α) ((fun (x : α) ↦ a • x) '' s) ((fun (x : α) ↦ b • x) '' t) =
    (fun (x : α) ↦ (a / b) • x) '' (s / t)
simp_rw₁ :
  HDiv.hDiv (α := Set α) ((fun (a_1 : α) ↦ a * a_1) '' s) ((fun (a : α) ↦ b * a) '' t) =
    (fun (a_1 : α) ↦ a / b * a_1) '' (s / t)
simp_rw₂ : {a} * s / ({b} * t) = {a / b} * (s / t)
simp_rw₃ : HDiv.hDiv (α := Set α) {a} {b} * (s / t) = {a / b} * (s / t)
⊢ a • s / b • t = (a / b) • (s / t)

Tactic:
simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
    singleton_div_singleton]

Premises used: Set.image_smul, Set.singleton_div_singleton, mul_div_mul_comm, smul_eq_mul, Set.singleton_mul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ (a • s).Finite ↔ s.Finite

Tactic:
finite_image_iff (MulAction.injective _).injOn

Premises used: Function.Injective.injOn, Set.finite_image_iff, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ (a • s).Infinite ↔ s.Infinite

Tactic:
infinite_image_iff (MulAction.injective _).injOn

Premises used: Function.Injective.injOn, Set.infinite_image_iff, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M_1 : Type u_1
G : Type u_2
α_1 : Type u_3
β : Type u_4
M : Type u_5
α : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Subsingleton α
x y : α
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := M) 1 x = y

Tactic:
simp only [one_smul, Subsingleton.elim x y]

Premises used: one_smul, Subsingleton.elim
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
inst_1 : IsPretransitive M α
x y : α
⊢ ∃ (m : M), m • x = y

Tactic:
IsPretransitive.exists_smul_eq x y

Premises used: MulAction.IsPretransitive.exists_smul_eq
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
inst_1 : IsPretransitive M α
x : α
⊢ Surjective.{u_1 + 1, u_3 + 1} (β := α) fun (c : M) ↦ c • x

Tactic:
exists_smul_eq M x

Premises used: MulAction.exists_smul_eq, Function.Surjective
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : IsPretransitive M α
inst_2 : Group G
⊢ IsPretransitive G G

Tactic:
⟨fun x y ↦ ⟨y * x⁻¹, inv_mul_cancel_right _ _⟩⟩

Premises used: HMul.hMul, MulAction.IsPretransitive.mk, Inv.inv, Exists.intro, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : IsPretransitive M α
inst_2 : Group G
⊢ IsPretransitive Gᵐᵒᵖ G

Tactic:
⟨fun x y ↦ ⟨.op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩

Premises used: HMul.hMul, MulAction.IsPretransitive.mk, Inv.inv, Exists.intro, mul_inv_cancel_left, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
exists_smul_eq : ∀ (x y : X), ∃ (g : G), g • x = y
⊢ IsPretransitive G X

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
x y : X
exists_smul_eq : ∀ (g : G), ∃ (g_1 : G), g_1 • g • x₀ = y
⊢ ∃ (g : G), g • x = y

Tactic:
rcases ha x with ⟨g, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
y : X
g : G
exists_smul_eq : ∀ (h : G), ∃ (g_1 : G), g_1 • g • x₀ = h • x₀
⊢ ∃ (g_1 : G), g_1 • g • x₀ = y

Tactic:
rcases ha y with ⟨h, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
g h : G
⊢ (h * g⁻¹) • g • x₀ = h • x₀

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
g h : G
⊢ ∃ (g_1 : G), g_1 • g • x₀ = h • x₀

Tactic:
exact ⟨h * g⁻¹, by simp [mul_smul]⟩
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M : Type u_5
N : Type u_6
α : Type u_7
inst : Monoid N
inst_1 : SMul M N
inst_2 : MulAction N α
inst_3 : SMul M α
inst_4 : IsScalarTower M N α
inst_5 : IsPretransitive M α
⊢ IsPretransitive N α

Tactic:
of_smul_eq (fun x : M ↦ x • 1) (smul_one_smul N _ _)

Premises used: MulAction.IsPretransitive.of_smul_eq, smul_one_smul, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid α
inst_1 : MulAction α β
inst_2 : MulAction.IsPretransitive α β
⊢ AddAction.IsPretransitive.{u_3, u_4} (Additive α) β

Tactic:
⟨@MulAction.exists_smul_eq α _ _ _⟩

Premises used: MulAction.exists_smul_eq, AddAction.IsPretransitive.mk
-- Module: Mathlib.Algebra.Group.Action.Pretransitive
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : AddMonoid α
inst_1 : AddAction α β
inst_2 : AddAction.IsPretransitive α β
⊢ MulAction.IsPretransitive.{u_3, u_4} (Multiplicative α) β

Tactic:
⟨@AddAction.exists_vadd_eq α _ _ _⟩

Premises used: AddAction.exists_vadd_eq, MulAction.IsPretransitive.mk
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
x_1 : M
x_2 : N
x_3 : α × β
fst : ((x_1 • x_2) • x_3).1 = (x_1 • x_2 • x_3).1
snd : ((x_1 • x_2) • x_3).2 = (x_1 • x_2 • x_3).2
⊢ (x_1 • x_2) • x_3 = x_1 • x_2 • x_3

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ ((x_1 • x_2) • x_3).1 = (x_1 • x_2 • x_3).1

Tactic:
smul_assoc ..

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ ((x_1 • x_2) • x_3).1 = (x_1 • x_2 • x_3).1

Tactic:
exact smul_assoc ..

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ ((x_1 • x_2) • x_3).2 = (x_1 • x_2 • x_3).2

Tactic:
smul_assoc ..

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ ((x_1 • x_2) • x_3).2 = (x_1 • x_2 • x_3).2

Tactic:
exact smul_assoc ..

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
x_1 : M
x_2 : N
x_3 : α × β
fst : (x_1 • x_2 • x_3).1 = (x_2 • x_1 • x_3).1
snd : (x_1 • x_2 • x_3).2 = (x_2 • x_1 • x_3).2
⊢ x_1 • x_2 • x_3 = x_2 • x_1 • x_3

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ (x_1 • x_2 • x_3).1 = (x_2 • x_1 • x_3).1

Tactic:
smul_comm ..

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ (x_1 • x_2 • x_3).1 = (x_2 • x_1 • x_3).1

Tactic:
exact smul_comm ..

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ (x_1 • x_2 • x_3).2 = (x_2 • x_1 • x_3).2

Tactic:
smul_comm ..

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ (x_1 • x_2 • x_3).2 = (x_2 • x_1 • x_3).2

Tactic:
exact smul_comm ..

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
x : α × β
inst_4 : FaithfulSMul M α
inst_5 : Nonempty β
m₁ m₂ : M
h : ∀ (a : α × β), m₁ • a = m₂ • a
b : β
a : α
⊢ m₁ • a = m₂ • a

Tactic:
injection h (a, b)

Premises used: Prod.mk
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
x : α × β
inst_4 : Nonempty α
inst_5 : FaithfulSMul M β
m₁ m₂ : M
h : ∀ (a : α × β), m₁ • a = m₂ • a
a : α
b : β
⊢ m₁ • b = m₂ • b

Tactic:
injection h (a, b)

Premises used: Prod.mk
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Mul N
inst_1 : Mul P
inst_2 : SMul M N
inst_3 : SMul M P
inst_4 : SMulCommClass M N N
inst_5 : SMulCommClass M P P
c : M
x y : N × P
⊢ c • x • y = x • c • y

Tactic:
simp [smul_def, mul_def, mul_smul_comm]

Premises used: Prod.mul_def, Prod.smul_def, mul_smul_comm
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Mul N
inst_1 : Mul P
inst_2 : SMul M N
inst_3 : SMul M P
inst_4 : IsScalarTower M N N
inst_5 : IsScalarTower M P P
c : M
x y : N × P
⊢ (c • x) • y = c • x • y

Tactic:
simp [smul_def, mul_def, smul_mul_assoc]

Premises used: smul_mul_assoc, Prod.mul_def, Prod.smul_def
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x x_1 : M
x_2 : α × β
fst : ((x * x_1) • x_2).1 = (x • x_1 • x_2).1
snd : ((x * x_1) • x_2).2 = (x • x_1 • x_2).2
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x x_1 : M
x_2 : α × β
⊢ ((x * x_1) • x_2).1 = (x • x_1 • x_2).1

Tactic:
mul_smul ..

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x x_1 : M
x_2 : α × β
⊢ ((x * x_1) • x_2).1 = (x • x_1 • x_2).1

Tactic:
exact mul_smul ..

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x x_1 : M
x_2 : α × β
⊢ ((x * x_1) • x_2).2 = (x • x_1 • x_2).2

Tactic:
mul_smul ..

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x x_1 : M
x_2 : α × β
⊢ ((x * x_1) • x_2).2 = (x • x_1 • x_2).2

Tactic:
exact mul_smul ..

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x : α × β
fst : (HSMul.hSMul (α := M) 1 x).1 = x.1
snd : (HSMul.hSMul (α := M) 1 x).2 = x.2
⊢ HSMul.hSMul (α := M) 1 x = x

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x : α × β
⊢ (HSMul.hSMul (α := M) 1 x).1 = x.1

Tactic:
one_smul ..

Premises used: one_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x : α × β
⊢ (HSMul.hSMul (α := M) 1 x).1 = x.1

Tactic:
exact one_smul ..

Premises used: one_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x : α × β
⊢ (HSMul.hSMul (α := M) 1 x).2 = x.2

Tactic:
one_smul ..

Premises used: one_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x : α × β
⊢ (HSMul.hSMul (α := M) 1 x).2 = x.2

Tactic:
exact one_smul ..

Premises used: one_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N α
inst_4 : SMulCommClass M N α
x y : M × N
a : α
change : (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
⊢ (x * y) • a = x • y • a

Tactic:
change (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a

Premises used: HMul.hMul, Prod.fst, Prod.snd
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N α
inst_4 : SMulCommClass M N α
x y : M × N
a : α
rw : x.1 • y.1 • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
rw₁ : x.1 • y.1 • x.2 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a
rw₂ rw₃ : x.1 • x.2 • y.1 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a
⊢ (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a

Tactic:
rw [mul_smul, mul_smul, smul_comm y.1 x.2]

Premises used: Prod.fst, SMulCommClass.smul_comm, Prod.snd, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
x : MulAction (M × N) α
instM : MulAction M α := compHom (M := M × N) α (MonoidHom.inl M N)
instN : MulAction N α := compHom (M := M × N) α (MonoidHom.inr M N)
m : M
n : N
a : α
change :
  HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) =
    HSMul.hSMul (α := M × N) (1, n) (HSMul.hSMul (α := M × N) (m, 1) a)
⊢ m • n • a = n • m • a

Tactic:
change (m, (1 : N)) • ((1 : M), n) • a = ((1 : M), n) • (m, (1 : N)) • a

Premises used: Prod.mk, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
x : MulAction (M × N) α
instM : MulAction M α := compHom (M := M × N) α (MonoidHom.inl M N)
instN : MulAction N α := compHom (M := M × N) α (MonoidHom.inr M N)
m : M
n : N
a : α
simp_rw : ((m, 1) * (1, n)) • a = ((1, n) * (m, 1)) • a
simp_rw₁ : (m * 1, 1 * n) • a = (1 * m, n * 1) • a
simp_rw₂ : (m, 1 * n) • a = (1 * m, n) • a
⊢ HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) =
    HSMul.hSMul (α := M × N) (1, n) (HSMul.hSMul (α := M × N) (m, 1) a)

Tactic:
simp_rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul]

Premises used: smul_smul, Prod.mk_mul_mk, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
dsimp :
  prodOfSMulCommClass M N α = { toSemigroupAction := toSemigroupAction, one_smul := one_smul : MulAction (M × N) α }
⊢ (fun (_insts : (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α) ↦
        have this := ⋯;
        (prodOfSMulCommClass M N α : MulAction (M × N) α))
      ((fun (x : MulAction (M × N) α) ↦
          (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α)
              (compHom (M := M × N) α (MonoidHom.inl M N))
              (PSigma.mk (β := fun (x_1 : MulAction N α) ↦ SMulCommClass M N α)
                (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯) :
            (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α))
        { toSemigroupAction := toSemigroupAction, one_smul := one_smul }) =
    { toSemigroupAction := toSemigroupAction, one_smul := one_smul : MulAction (M × N) α }

Tactic:
dsimp only
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
smul : ∀ (m : M) (n : N) (a : α), SMul.smul (m, n) a = SMul.smul (m, n) a
⊢ prodOfSMulCommClass M N α = { toSemigroupAction := toSemigroupAction, one_smul := one_smul : MulAction (M × N) α }

Tactic:
ext ⟨m, n⟩ a
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
m : M
n : N
a : α
smul : HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) = SMul.smul (m, n) a
⊢ SMul.smul (m, n) a = SMul.smul (m, n) a

Tactic:
change (m, (1 : N)) • ((1 : M), n) • a = _

Premises used: Prod.mk, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
m : M
n : N
a : α
smul : (m, n) • a = SMul.smul (m, n) a
⊢ HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) = SMul.smul (m, n) a

Tactic:
rw [← mul_smul, Prod.mk_mul_mk, mul_one, one_mul]

Premises used: Prod.mk_mul_mk, mul_one, SemigroupAction.mul_smul, one_mul
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Prod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
dsimp :
  Eq (α := (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α)
      (compHom (M := M × N) α (MonoidHom.inl M N))
      (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯))
    (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α) hM
      (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd))
⊢ Eq (α := (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α)
    ((fun (x : MulAction (M × N) α) ↦
        (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α)
            (compHom (M := M × N) α (MonoidHom.inl M N))
            (PSigma.mk (β := fun (x_1 : MulAction N α) ↦ SMulCommClass M N α)
              (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯) :
          (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α))
      ((fun (_insts : (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α) ↦
          have this := ⋯;
          (prodOfSMulCommClass M N α : MulAction (M × N) α))
        (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α) hM
          (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd))))
    (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α) hM
      (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd))

Tactic:
dsimp only