awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 (α := (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)
have h : Eq (α := MulAction N α → Prop) (fun (x : MulAction N α) ↦ SMulCommClass M N α) fun (x : MulAction N α) ↦
  SMulCommClass M N α
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 α
⊢ 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)
have h₁ : compHom (M := M × N) α (MonoidHom.inr M N) = hN
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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
⊢ 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)
have h₂ : HEq (α := SMulCommClass M N α) sorry snd
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 α
⊢ Eq (α := MulAction N α → Prop) (fun (x : MulAction N α) ↦ SMulCommClass M N α) fun (x : MulAction N α) ↦
    SMulCommClass M N α
have h : ∀ (x : MulAction N α), SMulCommClass M N α = SMulCommClass M N α
Tactic: funext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 α
⊢ SMulCommClass M N α = SMulCommClass M N α
have h : compHom (M := M × N) α (MonoidHom.inl M N) = hM
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 α
⊢ compHom (M := M × N) α (MonoidHom.inl M N) = hM
have h : ∀ (m : M) (a : α), SMul.smul m a = SMul.smul m a
Tactic: ext m a
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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
have rw : SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
Tactic: rw [← hN.one_smul a]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 a
have h : SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
Tactic: conv_rhs => rw [← hN.one_smul a]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 α
⊢ compHom (M := M × N) α (MonoidHom.inr M N) = hN
have h : ∀ (n : N) (a : α), SMul.smul n a = SMul.smul n a
Tactic: ext n a
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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
have rw : HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (SMul.smul n a)
Tactic: rw [← hM.one_smul (SMul.smul n a)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
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 = SMul.smul n a
have h : SMul.smul n a = HSMul.hSMul.{u_1, u_5, u_5} (α := M) 1 (SMul.smul n a)
Tactic: conv_rhs => rw [← hM.one_smul (SMul.smul n a)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ (a • b) • x = a • b • x
have mk : ∀ (fst : ι) (snd : α fst), (a • b) • mk (β := fun (i : ι) ↦ α i) fst snd = a • b • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ (a • b) • mk (β := fun (i : ι) ↦ α i) fst snd = a • b • mk (β := fun (i : ι) ↦ α i) fst snd
have mk : mk (β := fun (i : ι) ↦ α i) fst ((a • b) • snd) = a • b • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ (a • b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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))
⊢ (a • b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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))
⊢ (a • b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ a • b • x = b • a • x
have mk : ∀ (fst : ι) (snd : α fst), a • b • mk (β := fun (i : ι) ↦ α i) fst snd = b • a • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ a • b • mk (β := fun (i : ι) ↦ α i) fst snd = b • a • mk (β := fun (i : ι) ↦ α i) fst snd
have mk : mk (β := fun (i : ι) ↦ α i) ((b • mk (β := fun (i : ι) ↦ α i) fst snd).fst (β := fun (i : ι) ↦ α i))
    (a • (b • mk (β := fun (i : ι) ↦ α i) fst snd).snd (β := fun (i : ι) ↦ α i)) =
  b • a • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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))
⊢ a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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))
⊢ a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = b • a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ MulOpposite.op a • x = a • x
have mk : ∀ (fst : ι) (snd : α fst),
  MulOpposite.op a • mk (β := fun (i : ι) ↦ α i) fst snd = a • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ MulOpposite.op a • mk (β := fun (i : ι) ↦ α i) fst snd = a • mk (β := fun (i : ι) ↦ α i) fst snd
have mk : mk (β := fun (i : ι) ↦ α i) fst (MulOpposite.op a • snd) = a • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: rw [smul_mk, smul_mk, op_smul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ MulOpposite.op a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have mk₁ : Sigma.mk (β := fun (i : ι) ↦ α i) fst (MulOpposite.op a • snd) = Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)
Tactic: rw [smul_mk, smul_mk, op_smul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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)
⊢ MulOpposite.op a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have mk₂ : Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd) = Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • snd)
Tactic: rw [smul_mk, smul_mk, op_smul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ (a * b) • x = a • b • x
have mk : ∀ (fst : ι) (snd : α fst), (a * b) • mk (β := fun (i : ι) ↦ α i) fst snd = a • b • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ (a * b) • mk (β := fun (i : ι) ↦ α i) fst snd = a • b • mk (β := fun (i : ι) ↦ α i) fst snd
have mk : mk (β := fun (i : ι) ↦ α i) fst ((a * b) • snd) = a • b • mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: rw [smul_mk, smul_mk, smul_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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
⊢ (a * b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
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))
⊢ (a * b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have 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))
Tactic: rw [smul_mk, smul_mk, smul_mk, mul_smul]