awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
⊢ HSMul.hSMul (β := Set β) a univ = univ

Tactic:
image_univ_of_surjective <| MulAction.surjective₀ ha

Premises used: MulAction.surjective₀, Set.image_univ_of_surjective
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
s : Set α
hs : ¬s ⊆ 0
⊢ HSMul.hSMul (β := Set β) s univ = univ

Tactic:
let ⟨a, ha, ha₀⟩ := not_subset.1 hs
  eq_univ_of_forall fun b ↦ ⟨a, ha, a⁻¹ • b, trivial, smul_inv_smul₀ ha₀ _⟩

Premises used: trivial, _private.0.Set.smul_univ₀.match_1, smul_inv_smul₀, Set.univ, Inv.inv, Set.eq_univ_of_forall, And.intro, Set.not_subset, Exists.intro, Iff.mp, HSMul.hSMul, Eq
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
s : Set α
hs : s.Nontrivial
⊢ HSMul.hSMul (β := Set β) s univ = univ

Tactic:
smul_univ₀ hs.not_subset_singleton

Premises used: Set.smul_univ₀, Set.Nontrivial.not_subset_singleton
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
inl : (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
inr : ∀ (ha : a ≠ 0), (a •> s)⁻¹ = s⁻¹ <• a⁻¹
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
inl : (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹
inl₁ : ∀ (hs : s.Nonempty), (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
inr : ∀ (x : α), x ∈ (a •> s)⁻¹ ↔ x ∈ s⁻¹ <• a⁻¹
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x : α
⊢ x ∈ (a •> s)⁻¹ ↔ x ∈ s⁻¹ <• a⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀, *]

Premises used: Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
inl : (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
inr : ∀ (ha : a ≠ 0), (s <• a)⁻¹ = a⁻¹ •> s⁻¹
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
inl : (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹
inl₁ : ∀ (hs : s.Nonempty), (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
inr : ∀ (x : α), x ∈ (s <• a)⁻¹ ↔ x ∈ a⁻¹ •> s⁻¹
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x : α
⊢ x ∈ (s <• a)⁻¹ ↔ x ∈ a⁻¹ •> s⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀, *]

Premises used: Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
β : Type u_4
inst : SMul M β
α : Type u_5
inst_1 : Monoid M
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
a : M
c : β
rw : (HSMul.hSMul (β := α) a 0, a • c) = (0, a • c)
rw₁ rw₂ : Eq (α := α × β) (0, a • c) (0, a • c)
⊢ HSMul.hSMul (β := α × β) a (0, c) = (0, a • c)

Tactic:
rw [Prod.smul_mk, smul_zero]

Premises used: smul_zero, Prod.smul_mk
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
β : Type u_5
inst_1 : Monoid M
inst_2 : AddMonoid β
inst_3 : DistribMulAction M β
a : M
b : α
rw : (a • b, HSMul.hSMul (β := β) a 0) = (a • b, 0)
rw₁ rw₂ : Eq (α := α × β) (a • b, 0) (a • b, 0)
⊢ HSMul.hSMul (β := α × β) a (b, 0) = (a • b, 0)

Tactic:
rw [Prod.smul_mk, smul_zero]

Premises used: smul_zero, Prod.smul_mk
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : Zero N
inst_2 : SMulZeroClass R M
inst_3 : SMulZeroClass R N
x : R
fst : (HSMul.hSMul (β := M × N) x 0).1 = 0.1
snd : (HSMul.hSMul (β := M × N) x 0).2 = 0.2
⊢ HSMul.hSMul (β := M × N) x 0 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : Zero N
inst_2 : SMulZeroClass R M
inst_3 : SMulZeroClass R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 0).1 = 0.1

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : Zero N
inst_2 : SMulZeroClass R M
inst_3 : SMulZeroClass R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 0).1 = 0.1

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : Zero N
inst_2 : SMulZeroClass R M
inst_3 : SMulZeroClass R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 0).2 = 0.2

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : Zero N
inst_2 : SMulZeroClass R M
inst_3 : SMulZeroClass R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 0).2 = 0.2

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : DistribSMul R M
inst_3 : DistribSMul R N
x : R
x_1 x_2 : M × N
fst : (x • (x_1 + x_2)).1 = (x • x_1 + x • x_2).1
snd : (x • (x_1 + x_2)).2 = (x • x_1 + x • x_2).2
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : DistribSMul R M
inst_3 : DistribSMul R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 + x_2)).1 = (x • x_1 + x • x_2).1

Tactic:
smul_add ..

Premises used: smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : DistribSMul R M
inst_3 : DistribSMul R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 + x_2)).1 = (x • x_1 + x • x_2).1

Tactic:
exact smul_add ..

Premises used: smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : DistribSMul R M
inst_3 : DistribSMul R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 + x_2)).2 = (x • x_1 + x • x_2).2

Tactic:
smul_add ..

Premises used: smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : DistribSMul R M
inst_3 : DistribSMul R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 + x_2)).2 = (x • x_1 + x • x_2).2

Tactic:
exact smul_add ..

Premises used: smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
fst : (HSMul.hSMul (β := M × N) x 1).1 = 1.1
snd : (HSMul.hSMul (β := M × N) x 1).2 = 1.2
⊢ HSMul.hSMul (β := M × N) x 1 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 1).1 = 1.1

Tactic:
smul_one _

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 1).1 = 1.1

Tactic:
exact smul_one _

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 1).2 = 1.2

Tactic:
smul_one _

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
⊢ (HSMul.hSMul (β := M × N) x 1).2 = 1.2

Tactic:
exact smul_one _

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
x_1 x_2 : M × N
fst : (x • (x_1 * x_2)).1 = (x • x_1 * x • x_2).1
snd : (x • (x_1 * x_2)).2 = (x • x_1 * x • x_2).2
⊢ x • (x_1 * x_2) = x • x_1 * x • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 * x_2)).1 = (x • x_1 * x • x_2).1

Tactic:
smul_mul' ..

Premises used: smul_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 * x_2)).1 = (x • x_1 * x • x_2).1

Tactic:
exact smul_mul' ..

Premises used: smul_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 * x_2)).2 = (x • x_1 * x • x_2).2

Tactic:
smul_mul' ..

Premises used: smul_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
x_1 x_2 : M × N
⊢ (x • (x_1 * x_2)).2 = (x • x_1 * x • x_2).2

Tactic:
exact smul_mul' ..

Premises used: smul_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMulWithZero R M
inst_4 : SMulWithZero R N
x : M × N
fst : (HSMul.hSMul (α := R) 0 x).1 = 0.1
snd : (HSMul.hSMul (α := R) 0 x).2 = 0.2
⊢ HSMul.hSMul (α := R) 0 x = 0

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMulWithZero R M
inst_4 : SMulWithZero R N
x : M × N
⊢ (HSMul.hSMul (α := R) 0 x).1 = 0.1

Tactic:
zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMulWithZero R M
inst_4 : SMulWithZero R N
x : M × N
⊢ (HSMul.hSMul (α := R) 0 x).1 = 0.1

Tactic:
exact zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMulWithZero R M
inst_4 : SMulWithZero R N
x : M × N
⊢ (HSMul.hSMul (α := R) 0 x).2 = 0.2

Tactic:
zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMulWithZero R M
inst_4 : SMulWithZero R N
x : M × N
⊢ (HSMul.hSMul (α := R) 0 x).2 = 0.2

Tactic:
exact zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
change : mn.1 • HSMul.hSMul (β := α) mn.2 0 = 0
⊢ HSMul.hSMul (β := α) mn 0 = 0

Tactic:
change mn.1 • mn.2 • 0 = (0 : α)

Premises used: Prod.fst, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
rw : HSMul.hSMul (β := α) mn.1 0 = 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := α) 0 0
⊢ mn.1 • HSMul.hSMul (β := α) mn.2 0 = 0

Tactic:
rw [smul_zero, smul_zero]

Premises used: DistribMulAction.smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
a a' : α
change : mn.1 • mn.2 • (a + a') = mn • a + mn • a'
⊢ mn • (a + a') = mn • a + mn • a'

Tactic:
change mn.1 • mn.2 • _ = (_ : α)

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
a a' : α
rw : mn.1 • mn.2 • a + mn.1 • mn.2 • a' = mn • a + mn • a'
⊢ mn.1 • mn.2 • (a + a') = mn • a + mn • a'

Tactic:
rw [smul_add, smul_add]

Premises used: DistribMulAction.smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • mn.2 • a + mn.1 • mn.2 • a' = mn • a + mn • a'

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
dsimp : prodOfSMulCommClass M N α = x
⊢ (fun (_insts : (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) ↦
        have this := ⋯;
        (prodOfSMulCommClass M N α : DistribMulAction (M × N) α))
      ((fun (x : DistribMulAction (M × N) α) ↦
          (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
              (compHom (M := M × N) α (MonoidHom.inl M N))
              (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
                (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯) :
            (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α))
        x) =
    x

Tactic:
dsimp only
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
smul : ∀ (m : M) (n : N) (a : α), SMul.smul (m, n) a = SMul.smul (m, n) a
⊢ prodOfSMulCommClass M N α = x

Tactic:
ext ⟨m, n⟩ a
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
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.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
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 [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.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
dsimp :
  Eq (α := (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
      (compHom (M := M × N) α (MonoidHom.inl M N))
      (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯))
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) fst
      (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd))
⊢ Eq (α := (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    ((fun (x : DistribMulAction (M × N) α) ↦
        (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
            (compHom (M := M × N) α (MonoidHom.inl M N))
            (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
              (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯) :
          (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α))
      ((fun (_insts : (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) ↦
          have this := ⋯;
          (prodOfSMulCommClass M N α : DistribMulAction (M × N) α))
        (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) fst
          (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd))))
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) fst
      (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd))

Tactic:
dsimp only
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
h : compHom (M := M × N) α (MonoidHom.inl M N) = fst
h₁ :
  HEq (α := (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯ :
      (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (β := (x : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd)
⊢ Eq (α := (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
      (compHom (M := M × N) α (MonoidHom.inl M N))
      (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯))
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) fst
      (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd))

Tactic:
congr 1
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction 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) = fst

Tactic:
ext m a
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
m : M
a : α
rw : SMul.smul m (HSMul.hSMul.{u_2, u_3, u_3} (α := N) 1 a)
| SMul.smul m a

Tactic:
rw [← one_smul N a]

Premises used: one_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
m : M
a : α
h : SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_3, u_3} (α := N) 1 a)
⊢ SMul.smul m a = SMul.smul m a

Tactic:
conv_rhs => rw [← one_smul N a]

Premises used: one_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_3, u_3} (α := N) 1 a)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
h :
  Eq (α := DistribMulAction N α → Prop) (fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
    fun (x : DistribMulAction N α) ↦ SMulCommClass M N α
h₁ : compHom (M := M × N) α (MonoidHom.inr M N) = x
h₂ : HEq (α := SMulCommClass M N α) ⋯ snd
⊢ HEq (α := (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯ :
      (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (β := (x : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd)

Tactic:
congr 1