awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
h : compHom (M := M × N) α (MonoidHom.inl M N) = hM
h₁ :
  HEq (α := (x : MulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯)
    (β := (x : MulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd)
⊢ 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))

Tactic:
congr 1
-- 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 α
h : ∀ (m : M) (a : α), SMul.smul m a = SMul.smul m a
⊢ compHom (M := M × N) α (MonoidHom.inl M N) = hM

Tactic:
ext m 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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
m : M
a : α
rw : SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
| SMul.smul m a

Tactic:
rw [← hN.one_smul a]

Premises used: MulAction.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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
m : M
a : α
h : SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
⊢ SMul.smul m a = SMul.smul m a

Tactic:
conv_rhs => rw [← hN.one_smul a]

Premises used: MulAction.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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 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 α
h :
  Eq (α := MulAction N α → Prop) (fun (x : MulAction N α) ↦ SMulCommClass M N α) fun (x : MulAction N α) ↦
    SMulCommClass M N α
h₁ : compHom (M := M × N) α (MonoidHom.inr M N) = hN
h₂ : HEq (α := SMulCommClass M N α) ⋯ snd
⊢ HEq (α := (x : MulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯)
    (β := (x : MulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd)

Tactic:
congr 1
-- 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 α
h : ∀ (x : MulAction N α), SMulCommClass M N α = SMulCommClass M N α
⊢ Eq (α := MulAction N α → Prop) (fun (x : MulAction N α) ↦ SMulCommClass M N α) fun (x : MulAction N α) ↦
    SMulCommClass M N α

Tactic:
funext
-- 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 α
x : MulAction N α
h : compHom (M := M × N) α (MonoidHom.inl M N) = hM
⊢ SMulCommClass M N α = SMulCommClass M N α

Tactic:
congr
-- 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 α
x : MulAction N α
h : ∀ (m : M) (a : α), SMul.smul m a = SMul.smul m a
⊢ compHom (M := M × N) α (MonoidHom.inl M N) = hM

Tactic:
ext m 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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
x : MulAction N α
m : M
a : α
rw : SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
| SMul.smul m a

Tactic:
rw [← hN.one_smul a]

Premises used: MulAction.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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
x : MulAction N α
m : M
a : α
h : SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
⊢ SMul.smul m a = SMul.smul m a

Tactic:
conv_rhs => rw [← hN.one_smul a]

Premises used: MulAction.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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
x : MulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 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 α
h : ∀ (n : N) (a : α), SMul.smul n a = SMul.smul n a
⊢ compHom (M := M × N) α (MonoidHom.inr M N) = hN

Tactic:
ext 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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
n : N
a : α
rw : HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (SMul.smul n a)
| SMul.smul n a

Tactic:
rw [← hM.one_smul (SMul.smul n a)]

Premises used: MulAction.one_smul, SMul.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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
n : N
a : α
h : SMul.smul n a = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (SMul.smul n a)
⊢ SMul.smul n a = SMul.smul n a

Tactic:
conv_rhs => rw [← hM.one_smul (SMul.smul n a)]

Premises used: MulAction.one_smul, SMul.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
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (SMul.smul 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 α
⊢ HEq (α := SMulCommClass M N α) ⋯ snd

Tactic:
proof_irrel_heq ..

Premises used: proof_irrel_heq
-- 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 α
⊢ HEq (α := SMulCommClass M N α) ⋯ snd

Tactic:
exact proof_irrel_heq ..

Premises used: proof_irrel_heq
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
a : M
x : (i : ι) × α i
⊢ a • x = map (β₁ := fun (i : ι) ↦ α i) (β₂ := α) id (fun (x : ι) (x_1 : α x) ↦ a • x_1) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
a : M
i : ι
b : α i
⊢ a • mk (β := α) i b = mk (β := α) i (a • b)

Tactic:
rfl

Premises used: Sigma.map, rfl
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : (i : ι) → SMul.{u_3, u_4} N (α i)
a_1 : M
i : ι
b_1 : α i
x_1 : (i : ι) × α i
inst_2 : SMul M N
inst_3 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} M N (α i)
a : M
b : N
x : (i : ι) × α i
mk :
  ∀ (fst : ι) (snd : α fst),
    (a • b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
⊢ (a • b) • x = a • b • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : (i : ι) → SMul.{u_3, u_4} N (α i)
a_1 : M
i : ι
b_1 : α i
x : (i : ι) × α i
inst_2 : SMul M N
inst_3 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} M N (α i)
a : M
b : N
fst : ι
snd : α fst
mk : Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a • b) • snd) = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
mk₁ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a • b) • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).fst (β := fun (i : ι) ↦ α i))
      (a • (b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).snd (β := fun (i : ι) ↦ α i))
mk₂ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a • b) • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i))
mk₃ mk₄ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • b • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i))
⊢ (a • b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd

Tactic:
rw [smul_mk, smul_mk, smul_mk, smul_assoc]

Premises used: smul_assoc, Sigma.smul_mk
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : (i : ι) → SMul.{u_3, u_4} N (α i)
a_1 : M
i : ι
b_1 : α i
x_1 : (i : ι) × α i
inst_2 : ∀ (i : ι), SMulCommClass.{u_2, u_3, u_4} M N (α i)
a : M
b : N
x : (i : ι) × α i
mk :
  ∀ (fst : ι) (snd : α fst),
    a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
⊢ a • b • x = b • a • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : (i : ι) → SMul.{u_3, u_4} N (α i)
a_1 : M
i : ι
b_1 : α i
x : (i : ι) × α i
inst_2 : ∀ (i : ι), SMulCommClass.{u_2, u_3, u_4} M N (α i)
a : M
b : N
fst : ι
snd : α fst
mk :
  Sigma.mk (β := fun (i : ι) ↦ α i) ((b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).fst (β := fun (i : ι) ↦ α i))
      (a • (b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).snd (β := fun (i : ι) ↦ α i)) =
    b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
mk₁ :
  Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i)) =
    b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
mk₂ :
  Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i)) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).fst (β := fun (i : ι) ↦ α i))
      (b • (a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).snd (β := fun (i : ι) ↦ α i))
mk₃ :
  Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i)) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)).fst (β := fun (i : ι) ↦ α i))
      (b • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)).snd (β := fun (i : ι) ↦ α i))
mk₄ mk₅ :
  Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (b • a • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)).fst (β := fun (i : ι) ↦ α i))
      (b • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)).snd (β := fun (i : ι) ↦ α i))
⊢ a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd

Tactic:
rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]

Premises used: Sigma.smul_mk, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : (i : ι) → SMul.{u_3, u_4} N (α i)
a_1 : M
i : ι
b : α i
x_1 : (i : ι) × α i
inst_2 : (i : ι) → SMul.{u_2, u_4} Mᵐᵒᵖ (α i)
inst_3 : ∀ (i : ι), IsCentralScalar.{u_2, u_4} M (α i)
a : M
x : (i : ι) × α i
mk :
  ∀ (fst : ι) (snd : α fst),
    MulOpposite.op a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
⊢ MulOpposite.op a • x = a • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : (i : ι) → SMul.{u_3, u_4} N (α i)
a_1 : M
i : ι
b : α i
x : (i : ι) × α i
inst_2 : (i : ι) → SMul.{u_2, u_4} Mᵐᵒᵖ (α i)
inst_3 : ∀ (i : ι), IsCentralScalar.{u_2, u_4} M (α i)
a : M
fst : ι
snd : α fst
mk : Sigma.mk (β := fun (i : ι) ↦ α i) fst (MulOpposite.op a • snd) = a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
mk₁ : Sigma.mk (β := fun (i : ι) ↦ α i) fst (MulOpposite.op a • snd) = Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)
mk₂ mk₃ : Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd) = Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)
⊢ MulOpposite.op a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd

Tactic:
rw [smul_mk, smul_mk, op_smul_eq_smul]

Premises used: Sigma.smul_mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
i : ι
inst_1 : FaithfulSMul.{u_2, u_4} M (α i)
⊢ FaithfulSMul M ((i : ι) × α i)

Tactic:
⟨fun h => eq_of_smul_eq_smul fun a : α i => heq_iff_eq.1 (Sigma.ext_iff.1 <| h <| mk i a).2⟩

Premises used: FaithfulSMul.eq_of_smul_eq_smul, heq_iff_eq, Sigma.ext_iff, FaithfulSMul.mk, And.right, Iff.mp, Sigma.mk
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : (i : ι) → SMul.{u_3, u_4} N (α i)
a : M
i : ι
b : α i
x : (i : ι) × α i
inst_2 : Nonempty ι
inst_3 : ∀ (i : ι), FaithfulSMul.{u_2, u_4} M (α i)
⊢ FaithfulSMul M ((i : ι) × α i)

Tactic:
(Nonempty.elim ‹_›) fun i => Sigma.FaithfulSMul' i

Premises used: Nonempty.elim, Sigma.FaithfulSMul'
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
a b : M
x : (i : ι) × α i
mk :
  ∀ (fst : ι) (snd : α fst),
    (a * b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
⊢ (a * b) • x = a • b • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
a b : M
fst : ι
snd : α fst
mk : Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a * b) • snd) = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
mk₁ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a * b) • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).fst (β := fun (i : ι) ↦ α i))
      (a • (b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).snd (β := fun (i : ι) ↦ α i))
mk₂ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a * b) • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i))
mk₃ mk₄ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • b • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i))
⊢ (a * b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd

Tactic:
rw [smul_mk, smul_mk, smul_mk, mul_smul]

Premises used: Sigma.smul_mk, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
x : (i : ι) × α i
mk :
  ∀ (fst : ι) (snd : α fst),
    HSMul.hSMul (α := M) 1 (Sigma.mk (β := fun (i : ι) ↦ α i) fst snd) = Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
⊢ HSMul.hSMul (α := M) 1 x = x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sigma
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
fst : ι
snd : α fst
mk :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst (HSMul.hSMul.{u_2, u_4, u_4} (α := M) 1 snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
mk₁ mk₂ : Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
⊢ HSMul.hSMul (α := M) 1 (Sigma.mk (β := fun (i : ι) ↦ α i) fst snd) = Sigma.mk (β := fun (i : ι) ↦ α i) fst snd

Tactic:
rw [smul_mk, one_smul]

Premises used: Sigma.smul_mk, one_smul
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
x : α ⊕ β
⊢ a • x = Sum.map (fun (x : α) ↦ a • x) (fun (x : β) ↦ a • x) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
b : α
⊢ HSMul.hSMul (β := α ⊕ β) a (inl b) = inl (a • b)

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
c : β
⊢ HSMul.hSMul (β := α ⊕ β) a (inr c) = inr (a • c)

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
x : α ⊕ β
inl : ∀ (val : α), (HSMul.hSMul (β := α ⊕ β) a (Sum.inl val)).swap = HSMul.hSMul (β := β ⊕ α) a (swap (Sum.inl val))
inr : ∀ (val : β), (HSMul.hSMul (β := α ⊕ β) a (Sum.inr val)).swap = HSMul.hSMul (β := β ⊕ α) a (swap (Sum.inr val))
⊢ (a • x).swap = a • x.swap

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
val : α
⊢ (HSMul.hSMul (β := α ⊕ β) a (inl val)).swap = HSMul.hSMul (β := β ⊕ α) a (swap (inl val))

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
val : β
⊢ (HSMul.hSMul (β := α ⊕ β) a (inr val)).swap = HSMul.hSMul (β := β ⊕ α) a (swap (inr val))

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x_1 : α ⊕ β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
inl : ∀ (val : α), HSMul.hSMul (β := α ⊕ β) (a • b) (Sum.inl val) = a • HSMul.hSMul (β := α ⊕ β) b (Sum.inl val)
inr : ∀ (val : β), HSMul.hSMul (β := α ⊕ β) (a • b) (Sum.inr val) = a • HSMul.hSMul (β := α ⊕ β) b (Sum.inr val)
⊢ (a • b) • x = a • b • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x : α ⊕ β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
a : M
b : N
val : α
⊢ HSMul.hSMul (β := α ⊕ β) (a • b) (inl val) = a • HSMul.hSMul (β := α ⊕ β) b (inl val)

Tactic:
congr_arg inl (smul_assoc _ _ _)

Premises used: Sum.map, smul_assoc, Sum.inl, congr_arg, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x : α ⊕ β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
a : M
b : N
val : β
⊢ HSMul.hSMul (β := α ⊕ β) (a • b) (inr val) = a • HSMul.hSMul (β := α ⊕ β) b (inr val)

Tactic:
congr_arg inr (smul_assoc _ _ _)

Premises used: Sum.map, smul_assoc, congr_arg, Sum.inr, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x : α ⊕ β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
a : M
b : N
val : α
⊢ HSMul.hSMul (β := α ⊕ β) (a • b) (inl val) = a • HSMul.hSMul (β := α ⊕ β) b (inl val)

Tactic:
exacts [congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]

Premises used: smul_assoc, Sum.inl, congr_arg, Sum.inr
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x_1 : α ⊕ β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
a : M
b : N
x : α ⊕ β
inl : ∀ (val : α), a • HSMul.hSMul (β := α ⊕ β) b (Sum.inl val) = b • HSMul.hSMul (β := α ⊕ β) a (Sum.inl val)
inr : ∀ (val : β), a • HSMul.hSMul (β := α ⊕ β) b (Sum.inr val) = b • HSMul.hSMul (β := α ⊕ β) a (Sum.inr val)
⊢ a • b • x = b • a • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x : α ⊕ β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
a : M
b : N
val : α
⊢ a • HSMul.hSMul (β := α ⊕ β) b (inl val) = b • HSMul.hSMul (β := α ⊕ β) a (inl val)

Tactic:
congr_arg inl (smul_comm _ _ _)

Premises used: Sum.map, Sum.inl, congr_arg, SMulCommClass.smul_comm, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x : α ⊕ β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
a : M
b : N
val : β
⊢ a • HSMul.hSMul (β := α ⊕ β) b (inr val) = b • HSMul.hSMul (β := α ⊕ β) a (inr val)

Tactic:
congr_arg inr (smul_comm _ _ _)

Premises used: Sum.map, congr_arg, Sum.inr, SMulCommClass.smul_comm, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x : α ⊕ β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
a : M
b : N
val : α
⊢ a • HSMul.hSMul (β := α ⊕ β) b (inl val) = b • HSMul.hSMul (β := α ⊕ β) a (inl val)

Tactic:
exacts [congr_arg inl (smul_comm _ _ _), congr_arg inr (smul_comm _ _ _)]

Premises used: Sum.inl, congr_arg, Sum.inr, SMulCommClass.smul_comm