awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : G × H
fst : (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).1 = 1.1
snd : (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).2 = 1.2
⊢ (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2) = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : G × H
⊢ (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).1 = 1.1

Tactic:
DivInvMonoid.zpow_zero' _

Premises used: DivInvMonoid.zpow_zero'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : G × H
⊢ (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).1 = 1.1

Tactic:
exact DivInvMonoid.zpow_zero' _

Premises used: DivInvMonoid.zpow_zero'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : G × H
⊢ (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).2 = 1.2

Tactic:
DivInvMonoid.zpow_zero' _

Premises used: DivInvMonoid.zpow_zero'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : G × H
⊢ (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).2 = 1.2

Tactic:
exact DivInvMonoid.zpow_zero' _

Premises used: DivInvMonoid.zpow_zero'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
fst :
  (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).1 =
    ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).1
snd :
  (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).2 =
    ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).2
⊢ (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2) =
    (DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).1 =
    ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).1

Tactic:
DivInvMonoid.zpow_succ' ..

Premises used: DivInvMonoid.zpow_succ'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).1 =
    ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).1

Tactic:
exact DivInvMonoid.zpow_succ' ..

Premises used: DivInvMonoid.zpow_succ'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).2 =
    ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).2

Tactic:
DivInvMonoid.zpow_succ' ..

Premises used: DivInvMonoid.zpow_succ'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).2 =
    ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).2

Tactic:
exact DivInvMonoid.zpow_succ' ..

Premises used: DivInvMonoid.zpow_succ'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
fst :
  (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).1 =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.1
snd :
  (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).2 =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.2
⊢ (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2) =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).1 =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.1

Tactic:
DivInvMonoid.zpow_neg' ..

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).1 =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.1

Tactic:
exact DivInvMonoid.zpow_neg' ..

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).2 =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.2

Tactic:
DivInvMonoid.zpow_neg' ..

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).2 =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.2

Tactic:
exact DivInvMonoid.zpow_neg' ..

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivisionMonoid G
inst_1 : DivisionMonoid H
⊢ ∀ (x : G × H), x⁻¹⁻¹ = x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivisionCommMonoid G
inst_1 : DivisionCommMonoid H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
rw : (fst * g₁, snd * h₁) = (fst, snd) * (g₁, h₁)
⊢ (g₁, h₁) * (fst, snd) = (fst, snd) * (g₁, h₁)

Tactic:
rw [mk_mul_mk, mul_comm g₁, mul_comm h₁]

Premises used: mul_comm, Prod.mk_mul_mk
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivisionCommMonoid G
inst_1 : DivisionCommMonoid H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
⊢ (fst * g₁, snd * h₁) = (fst, snd) * (g₁, h₁)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Group G
inst_1 : Group H
x : G × H
fst : (x⁻¹ * x).1 = 1.1
snd : (x⁻¹ * x).2 = 1.2
⊢ x⁻¹ * x = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Group G
inst_1 : Group H
x : G × H
⊢ (x⁻¹ * x).1 = 1.1

Tactic:
inv_mul_cancel _

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Group G
inst_1 : Group H
x : G × H
⊢ (x⁻¹ * x).1 = 1.1

Tactic:
exact inv_mul_cancel _

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Group G
inst_1 : Group H
x : G × H
⊢ (x⁻¹ * x).2 = 1.2

Tactic:
inv_mul_cancel _

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Group G
inst_1 : Group H
x : G × H
⊢ (x⁻¹ * x).2 = 1.2

Tactic:
exact inv_mul_cancel _

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : LeftCancelMonoid M
inst_1 : LeftCancelMonoid N
x x_1 : M × N
⊢ ∀ ⦃a₂ : M × N⦄, Eq (α := M × N) ((fun (x_2 : M × N) ↦ x * x_2) x_1) ((fun (x_2 : M × N) ↦ x * x_2) a₂) → x_1 = a₂

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : RightCancelMonoid M
inst_1 : RightCancelMonoid N
x x_1 : M × N
⊢ ∀ ⦃a₂ : M × N⦄, Eq (α := M × N) ((fun (x_2 : M × N) ↦ x_2 * x) x_1) ((fun (x_2 : M × N) ↦ x_2 * x) a₂) → x_1 = a₂

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CancelMonoid M
inst_1 : CancelMonoid N
x x_1 : M × N
⊢ ∀ ⦃a₂ : M × N⦄, Eq (α := M × N) ((fun (x_2 : M × N) ↦ x_2 * x) x_1) ((fun (x_2 : M × N) ↦ x_2 * x) a₂) → x_1 = a₂

Tactic:
simp only [mul_left_inj, imp_self, forall_const]

Premises used: mul_left_inj, imp_self, forall_const
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
x x_1 : M × N
m₁ : M
n₁ : N
fst : M
snd : N
rw : (m₁ * fst, n₁ * snd) = (fst, snd) * (m₁, n₁)
rw₁ : (m₁ * fst, n₁ * snd) = (fst * m₁, snd * n₁)
rw₂ : (fst * m₁, n₁ * snd) = (fst * m₁, snd * n₁)
rw₃ rw₄ : (fst * m₁, snd * n₁) = (fst * m₁, snd * n₁)
⊢ (m₁, n₁) * (fst, snd) = (fst, snd) * (m₁, n₁)

Tactic:
rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]

Premises used: mul_comm, Prod.mk_mul_mk
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CancelCommMonoid M
inst_1 : CancelCommMonoid N
x x_1 : M × N
⊢ ∀ ⦃a₂ : M × N⦄, Eq (α := M × N) ((fun (x_2 : M × N) ↦ x * x_2) x_1) ((fun (x_2 : M × N) ↦ x * x_2) a₂) → x_1 = a₂

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommGroup G
inst_1 : CommGroup H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
rw : (g₁ * fst, h₁ * snd) = (fst, snd) * (g₁, h₁)
rw₁ : (g₁ * fst, h₁ * snd) = (fst * g₁, snd * h₁)
rw₂ : (fst * g₁, h₁ * snd) = (fst * g₁, snd * h₁)
rw₃ rw₄ : (fst * g₁, snd * h₁) = (fst * g₁, snd * h₁)
⊢ (g₁, h₁) * (fst, snd) = (fst, snd) * (g₁, h₁)

Tactic:
rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]

Premises used: mul_comm, Prod.mk_mul_mk
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : Mul N
x y z : M × N
hm : SemiconjBy x.1 y.1 z.1
hn : SemiconjBy x.2 y.2 z.2
⊢ SemiconjBy x y z

Tactic:
Prod.ext hm hn

Premises used: SemiconjBy, Prod.ext
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : Mul N
x y z : M × N
⊢ SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2

Tactic:
Prod.ext_iff

Premises used: SemiconjBy, Prod.ext_iff
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : Mul N
x y : M × N
hm : Commute x.1 y.1
hn : Commute x.2 y.2
⊢ Commute x y

Tactic:
SemiconjBy.prod hm hn

Premises used: SemiconjBy.prod, Commute
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : Mul N
x y : M × N
⊢ Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2

Tactic:
semiconjBy_iff

Premises used: Prod.semiconjBy_iff, Commute
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : Mul N
⊢ Eq (α := (a : M × N) → M) (⇑(fst M N) : (a : M × N) → M) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : Mul N
⊢ Eq (α := (a : M × N) → N) (⇑(snd M N) : (a : M × N) → N) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
f : M →ₙ* N
g : M →ₙ* P
⊢ Eq (α := (a : M) → N × P) (⇑(f.prod g) : (a : M) → N × P)
    (Function.prod (α := fun (a : M) ↦ N) (β := fun (a : M) ↦ P) (⇑f : (a : M) → N) (⇑g : (a : M) → P))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
f : M →ₙ* N
g : M →ₙ* P
x : M
⊢ Eq (α := N × P) ((f.prod g : (a : M) → N × P) x : N × P) (((f : (a : M) → N) x, (g : (a : M) → P) x) : N × P)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
f : M →ₙ* N
g : M →ₙ* P
⊢ comp (fst N P) (f.prod g) = f

Tactic:
ext fun _ => rfl

Premises used: MulHom.ext, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
f : M →ₙ* N
g : M →ₙ* P
⊢ comp (snd N P) (f.prod g) = g

Tactic:
ext fun _ => rfl

Premises used: MulHom.ext, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
f : M →ₙ* N × P
x : M
⊢ Eq (α := N × P) (((comp (fst N P) f).prod (comp (snd N P) f) : (a : M) → N × P) x : N × P)
    ((f : (a : M) → N × P) x : N × P)

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Premises used: MulHom.coe_snd, MulHom.coe_fst, MulHom.comp_apply, MulHom.prod_apply
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
M' : Type u_6
N' : Type u_7
inst : Mul M
inst_1 : Mul N
inst_2 : Mul M'
inst_3 : Mul N'
f : M →ₙ* M'
g : N →ₙ* N'
⊢ f.prodMap g = MulHom.prod (f.comp (fst M N)) (g.comp (snd M N))

Tactic:
rfl

Premises used: rfl, MulHom.prodMap
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
M' : Type u_6
N' : Type u_7
inst : Mul M
inst_1 : Mul N
inst_2 : Mul M'
inst_3 : Mul N'
f : M →ₙ* M'
g : N →ₙ* N'
⊢ Eq (α := (a : M × N) → M' × N') (⇑(f.prodMap g) : (a : M × N) → M' × N')
    (Prod.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))

Tactic:
rfl

Premises used: Prod.map, Function.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
inst : Mul M
inst_1 : Mul N
inst_2 : Mul M'
inst_3 : Mul N'
inst_4 : Mul P
f : P →ₙ* M
g : P →ₙ* N
f' : M →ₙ* M'
g' : N →ₙ* N'
⊢ (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

Tactic:
rfl

Premises used: Function.prod, MulHom.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : Mul M
inst_1 : Mul N
inst_2 : CommSemigroup P
f : M →ₙ* P
g : N →ₙ* P
p : M × N
⊢ (f.coprod g : (a : M × N) → P) p = HMul.hMul (α := P) (β := P) ((f : (a : M) → P) p.1 : P) ((g : (a : N) → P) p.2 : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : Mul M
inst_1 : Mul N
inst_2 : CommSemigroup P
Q : Type u_6
inst_3 : CommSemigroup Q
h : P →ₙ* Q
f : M →ₙ* P
g : N →ₙ* P
x : M × N
⊢ Eq.{u_6 + 1} (α := Q) ((h.comp (f.coprod g) : (a : M × N) → Q) x : Q)
    (((h.comp f).coprod (h.comp g) : (a : M × N) → Q) x : Q)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := (a : M × N) → M) (⇑(fst M N) : (a : M × N) → M) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := (a : M × N) → N) (⇑(snd M N) : (a : M × N) → N) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
x : M
⊢ Eq (α := M × N) ((inl M N : (a : M) → M × N) x : M × N) ((x, 1) : M × N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
y : N
⊢ Eq (α := M × N) ((inr M N : (a : N) → M × N) y : M × N) ((1, y) : M × N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := M →* M) (comp (fst M N) (inl M N)) (id M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := M →* N) (comp (snd M N) (inl M N)) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := N →* M) (comp (fst M N) (inr M N)) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := N →* N) (comp (snd M N) (inr M N)) (id N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
m : M
n : N
⊢ Commute (S := M × N) ((inl M N : (a : M) → M × N) m : M × N) ((inr M N : (a : N) → M × N) n : M × N)

Tactic:
Commute.prod (.one_right m) (.one_left n)

Premises used: Commute.prod, Commute.one_right, Commute.one_left
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : M →* N
g : M →* P
⊢ Eq (α := (a : M) → N × P) (⇑(f.prod g) : (a : M) → N × P)
    (Function.prod (α := fun (a : M) ↦ N) (β := fun (a : M) ↦ P) (⇑f : (a : M) → N) (⇑g : (a : M) → P))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : M →* N
g : M →* P
x : M
⊢ Eq (α := N × P) ((f.prod g : (a : M) → N × P) x : N × P) (((f : (a : M) → N) x, (g : (a : M) → P) x) : N × P)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : M →* N
g : M →* P
⊢ comp (fst N P) (f.prod g) = f

Tactic:
ext fun _ => rfl

Premises used: MonoidHom.ext, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : M →* N
g : M →* P
⊢ comp (snd N P) (f.prod g) = g

Tactic:
ext fun _ => rfl

Premises used: MonoidHom.ext, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : M →* N × P
x : M
⊢ Eq (α := N × P) (((comp (fst N P) f).prod (comp (snd N P) f) : (a : M) → N × P) x : N × P)
    ((f : (a : M) → N × P) x : N × P)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
M' : Type u_6
N' : Type u_7
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* M'
g : N →* N'
⊢ f.prodMap g = MonoidHom.prod (f.comp (fst M N)) (g.comp (snd M N))

Tactic:
rfl

Premises used: MonoidHom.prodMap, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
M' : Type u_6
N' : Type u_7
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* M'
g : N →* N'
⊢ Eq (α := (a : M × N) → M' × N') (⇑(f.prodMap g) : (a : M × N) → M' × N')
    (Prod.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))

Tactic:
rfl

Premises used: Prod.map, Function.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
M' : Type u_6
N' : Type u_7
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
f : P →* M
g : P →* N
f' : M →* M'
g' : N →* N'
⊢ (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

Tactic:
rfl

Premises used: MonoidHom.prod, Function.prod, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommMonoid P
f : M →* P
g : N →* P
p : M × N
⊢ (f.coprod g : (a : M × N) → P) p = HMul.hMul (α := P) (β := P) ((f : (a : M) → P) p.1 : P) ((g : (a : N) → P) p.2 : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommMonoid P
f : M →* P
g : N →* P
x : M
⊢ Eq.{u_5 + 1} (α := P) (((f.coprod g).comp (inl M N) : (a : M) → P) x : P) ((f : (a : M) → P) x : P)

Tactic:
simp [coprod_apply]

Premises used: MonoidHom.coprod_apply
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommMonoid P
f : M →* P
g : N →* P
x : N
⊢ Eq.{u_5 + 1} (α := P) (((f.coprod g).comp (inr M N) : (a : N) → P) x : P) ((g : (a : N) → P) x : P)

Tactic:
simp [coprod_apply]

Premises used: MonoidHom.coprod_apply
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommMonoid P
f : M × N →* P
x : M × N
⊢ Eq.{u_5 + 1} (α := P) (((f.comp (inl M N)).coprod (f.comp (inr M N)) : (a : M × N) → P) x : P)
    ((f : (a : M × N) → P) x : P)

Tactic:
simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

Premises used: MonoidHom.coprod_apply, MonoidHom.inr_apply, MonoidHom.inl_apply, map_mul
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_6
N : Type u_7
inst : CommMonoid M
inst_1 : CommMonoid N
⊢ Eq (α := M × N →* M × N) (coprod (inl M N) (inr M N)) (id (M × N))

Tactic:
coprod_unique (id <| M × N)

Premises used: MonoidHom.inr, MonoidHom.inl, MonoidHom.id, MonoidHom.coprod_unique, Prod
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommMonoid P
Q : Type u_6
inst_3 : CommMonoid Q
h : P →* Q
f : M →* P
g : N →* P
x : M × N
⊢ Eq.{u_6 + 1} (α := Q) ((h.comp (f.coprod g) : (a : M × N) → Q) x : Q)
    (((h.comp f).coprod (h.comp g) : (a : M × N) → Q) x : Q)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := (a : M × N) → N × M) (⇑prodComm : (a : M × N) → N × M) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := (a : N × M) → M × N) (⇑(symm prodComm) : (a : N × M) → M × N) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
⊢ Eq (α := (a : (M × N) × P) → M × N × P) (⇑prodAssoc : (a : (M × N) × P) → M × N × P)
    (⇑(Equiv.prodAssoc M N P) : (a : (M × N) × P) → M × N × P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
⊢ Eq (α := (a : M × N × P) → (M × N) × P) (⇑(symm prodAssoc) : (a : M × N × P) → (M × N) × P)
    (⇑(Equiv.prodAssoc M N P).symm : (a : M × N × P) → (M × N) × P)

Tactic:
rfl

Premises used: Equiv.prodAssoc, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
M' : Type u_6
N' : Type u_7
inst_2 : MulOneClass N'
inst_3 : MulOneClass M'
⊢ (↑(prodProdProdComm M N M' N') : (M × N) × M' × N' ≃ (M × M') × N × N') = Equiv.prodProdProdComm M N M' N'

Tactic:
rfl

Premises used: Equiv.prodProdProdComm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
M' : Type u_6
N' : Type u_7
inst_2 : MulOneClass N'
inst_3 : MulOneClass M'
⊢ Eq (α := (M × M') × N × N' ≃* (M × N) × M' × N') (symm (prodProdProdComm M N M' N')) (prodProdProdComm M M' N N')

Tactic:
rfl

Premises used: MulEquiv.prodProdProdComm, Equiv.symm, MulEquiv.symm, rfl