/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot, Yury Kudryashov

! This file was ported from Lean 3 source module algebra.group.prod
! leanprover-community/mathlib commit cf9386b56953fb40904843af98b7a80757bbe7f9
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Opposite
import Mathlib.Algebra.GroupWithZero.Units.Basic
import Mathlib.Algebra.Hom.Units

/-!
# Monoid, group etc structures on `M × N`

In this file we define one-binop (`Monoid`, `Group` etc) structures on `M × N`. We also prove
trivial `simp` lemmas, and define the following operations on `MonoidHom`s:

* `fst M N : M × N →* M`, `snd M N : M × N →* N`: projections `Prod.fst` and `Prod.snd`
  as `MonoidHom`s;
* `inl M N : M →* M × N`, `inr M N : N →* M × N`: inclusions of first/second monoid
  into the product;
* `f.prod g : `M →* N × P`: sends `x` to `(f x, g x)`;
* `f.coprod g : M × N →* P`: sends `(x, y)` to `f x * g y`;
* `f.prodMap g : M × N → M' × N'`: `prod.map f g` as a `MonoidHom`,
  sends `(x, y)` to `(f x, g y)`.

## Main declarations

* `mulMulHom`/`mulMonoidHom`/`mulMonoidWithZeroHom`: Multiplication bundled as a
  multiplicative/monoid/monoid with zero homomorphism.
* `divMonoidHom`/`divMonoidWithZeroHom`: Division bundled as a monoid/monoid with zero
  homomorphism.
-/


variable {A: Type ?u.23
A : Type _: Type (?u.59943+1)
Type _} {B: Type ?u.26
B : Type _: Type (?u.21364+1)
Type _} {G: Type ?u.39690
G : Type _: Type (?u.15455+1)
Type _} {H: Type ?u.32
H : Type _: Type (?u.1002+1)
Type _} {M: Type ?u.14
M : Type _: Type (?u.1005+1)
Type _} {N: Type ?u.39699
N : Type _: Type (?u.7978+1)
Type _} {P: Type ?u.39702
P : Type _: Type (?u.42267+1)
Type _}

namespace Prod

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst : Add N] → Add (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst : Mul N] → Mul (M × N)
instance [Mul: Type ?u.44 → Type ?u.44
Mul M: Type ?u.35
M] [Mul: Type ?u.47 → Type ?u.47
Mul N: Type ?u.38
N] : Mul: Type ?u.50 → Type ?u.50
Mul (M: Type ?u.35
M × N: Type ?u.38
N) :=
  ⟨fun p: ?m.62
p q: ?m.65
q => ⟨p: ?m.62
p.1: {α : Type ?u.81} → {β : Type ?u.80} → α × β → α
1 * q: ?m.65
q.1: {α : Type ?u.85} → {β : Type ?u.84} → α × β → α
1, p: ?m.62
p.2: {α : Type ?u.129} → {β : Type ?u.128} → α × β → β
2 * q: ?m.65
q.2: {α : Type ?u.133} → {β : Type ?u.132} → α × β → β
2⟩⟩

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).fst = p.fst + q.fst
to_additive (attr := simp)]
theorem fst_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).fst = p.fst * q.fst
fst_mul [Mul: Type ?u.526 → Type ?u.526
Mul M: Type ?u.517
M] [Mul: Type ?u.529 → Type ?u.529
Mul N: Type ?u.520
N] (p: M × N
p q: M × N
q : M: Type ?u.517
M × N: Type ?u.520
N) : (p: M × N
p * q: M × N
q).1: {α : Type ?u.615} → {β : Type ?u.614} → α × β → α
1 = p: M × N
p.1: {α : Type ?u.624} → {β : Type ?u.623} → α × β → α
1 * q: M × N
q.1: {α : Type ?u.628} → {β : Type ?u.627} → α × β → α
1 :=
  rfl: ∀ {α : Sort ?u.672} {a : α}, a = a
rfl
#align prod.fst_mul Prod.fst_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).fst = p.fst * q.fst
Prod.fst_mul
#align prod.fst_add Prod.fst_add: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).fst = p.fst + q.fst
Prod.fst_add

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).snd = p.snd + q.snd
to_additive (attr := simp)]
theorem snd_mul: ∀ [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).snd = p.snd * q.snd
snd_mul [Mul: Type ?u.770 → Type ?u.770
Mul M: Type ?u.761
M] [Mul: Type ?u.773 → Type ?u.773
Mul N: Type ?u.764
N] (p: M × N
p q: M × N
q : M: Type ?u.761
M × N: Type ?u.764
N) : (p: M × N
p * q: M × N
q).2: {α : Type ?u.859} → {β : Type ?u.858} → α × β → β
2 = p: M × N
p.2: {α : Type ?u.868} → {β : Type ?u.867} → α × β → β
2 * q: M × N
q.2: {α : Type ?u.872} → {β : Type ?u.871} → α × β → β
2 :=
  rfl: ∀ {α : Sort ?u.916} {a : α}, a = a
rfl
#align prod.snd_mul Prod.snd_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).snd = p.snd * q.snd
Prod.snd_mul
#align prod.snd_add Prod.snd_add: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).snd = p.snd + q.snd
Prod.snd_add

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
to_additive (attr := simp)]
theorem mk_mul_mk: ∀ [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N), (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk [Mul: Type ?u.1014 → Type ?u.1014
Mul M: Type ?u.1005
M] [Mul: Type ?u.1017 → Type ?u.1017
Mul N: Type ?u.1008
N] (a₁: M
a₁ a₂: M
a₂ : M: Type ?u.1005
M) (b₁: N
b₁ b₂: N
b₂ : N: Type ?u.1008
N) :
    (a₁: M
a₁, b₁: N
b₁) * (a₂: M
a₂, b₂: N
b₂) = (a₁: M
a₁ * a₂: M
a₂, b₁: N
b₁ * b₂: N
b₂) :=
  rfl: ∀ {α : Sort ?u.1200} {a : α}, a = a
rfl
#align prod.mk_mul_mk Prod.mk_mul_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
Prod.mk_mul_mk
#align prod.mk_add_mk Prod.mk_add_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
Prod.mk_add_mk

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), swap (p + q) = swap p + swap q
to_additive (attr := simp)]
theorem swap_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), swap (p * q) = swap p * swap q
swap_mul [Mul: Type ?u.1332 → Type ?u.1332
Mul M: Type ?u.1323
M] [Mul: Type ?u.1335 → Type ?u.1335
Mul N: Type ?u.1326
N] (p: M × N
p q: M × N
q : M: Type ?u.1323
M × N: Type ?u.1326
N) : (p: M × N
p * q: M × N
q).swap: {α : Type ?u.1421} → {β : Type ?u.1420} → α × β → β × α
swap = p: M × N
p.swap: {α : Type ?u.1433} → {β : Type ?u.1432} → α × β → β × α
swap * q: M × N
q.swap: {α : Type ?u.1440} → {β : Type ?u.1439} → α × β → β × α
swap :=
  rfl: ∀ {α : Sort ?u.1507} {a : α}, a = a
rfl
#align prod.swap_mul Prod.swap_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), swap (p * q) = swap p * swap q
Prod.swap_mul
#align prod.swap_add Prod.swap_add: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), swap (p + q) = swap p + swap q
Prod.swap_add

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), p + q = (p.fst + q.fst, p.snd + q.snd)
to_additive]
theorem mul_def: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), p * q = (p.fst * q.fst, p.snd * q.snd)
mul_def [Mul: Type ?u.1619 → Type ?u.1619
Mul M: Type ?u.1610
M] [Mul: Type ?u.1622 → Type ?u.1622
Mul N: Type ?u.1613
N] (p: M × N
p q: M × N
q : M: Type ?u.1610
M × N: Type ?u.1613
N) : p: M × N
p * q: M × N
q = (p: M × N
p.1: {α : Type ?u.1645} → {β : Type ?u.1644} → α × β → α
1 * q: M × N
q.1: {α : Type ?u.1651} → {β : Type ?u.1650} → α × β → α
1, p: M × N
p.2: {α : Type ?u.1696} → {β : Type ?u.1695} → α × β → β
2 * q: M × N
q.2: {α : Type ?u.1700} → {β : Type ?u.1699} → α × β → β
2) :=
  rfl: ∀ {α : Sort ?u.1811} {a : α}, a = a
rfl
#align prod.mul_def Prod.mul_def: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), p * q = (p.fst * q.fst, p.snd * q.snd)
Prod.mul_def
#align prod.add_def Prod.add_def: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), p + q = (p.fst + q.fst, p.snd + q.snd)
Prod.add_def

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : Add N] (b₁ b₂ : N), (0, b₁) + (0, b₂) = (0, b₁ + b₂)
to_additive]
theorem one_mk_mul_one_mk: ∀ [inst : Monoid M] [inst_1 : Mul N] (b₁ b₂ : N), (1, b₁) * (1, b₂) = (1, b₁ * b₂)
one_mk_mul_one_mk [Monoid: Type ?u.1869 → Type ?u.1869
Monoid M: Type ?u.1860
M] [Mul: Type ?u.1872 → Type ?u.1872
Mul N: Type ?u.1863
N] (b₁: N
b₁ b₂: N
b₂ : N: Type ?u.1863
N) :
    ((1: ?m.1889
1 : M: Type ?u.1860
M), b₁: N
b₁) * (1: ?m.2018
1, b₂: N
b₂) = (1: ?m.2037
1, b₁: N
b₁ * b₂: N
b₂) :=
  by
Goals accomplished! 🐙 A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N

(1, b₁) * (1, b₂) = (1, b₁ * b₂)rw [A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N

(1, b₁) * (1, b₂) = (1, b₁ * b₂)mk_mul_mk: ∀ {M : Type ?u.2305} {N : Type ?u.2306} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N

(1 * 1, b₁ * b₂) = (1, b₁ * b₂) A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N

(1, b₁) * (1, b₂) = (1, b₁ * b₂)mul_one: ∀ {M : Type ?u.2511} [inst : MulOneClass M] (a : M), a * 1 = a
mul_oneA: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N

(1, b₁ * b₂) = (1, b₁ * b₂)]
Goals accomplished! 🐙
#align prod.one_mk_mul_one_mk Prod.one_mk_mul_one_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Mul N] (b₁ b₂ : N), (1, b₁) * (1, b₂) = (1, b₁ * b₂)
Prod.one_mk_mul_one_mk
#align prod.zero_mk_add_zero_mk Prod.zero_mk_add_zero_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : Add N] (b₁ b₂ : N), (0, b₁) + (0, b₂) = (0, b₁ + b₂)
Prod.zero_mk_add_zero_mk

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : AddMonoid N] (a₁ a₂ : M), (a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
to_additive]
theorem mk_one_mul_mk_one: ∀ [inst : Mul M] [inst_1 : Monoid N] (a₁ a₂ : M), (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
mk_one_mul_mk_one [Mul: Type ?u.2655 → Type ?u.2655
Mul M: Type ?u.2646
M] [Monoid: Type ?u.2658 → Type ?u.2658
Monoid N: Type ?u.2649
N] (a₁: M
a₁ a₂: M
a₂ : M: Type ?u.2646
M) :
    (a₁: M
a₁, (1: ?m.2675
1 : N: Type ?u.2649
N)) * (a₂: M
a₂, 1: ?m.2804
1) = (a₁: M
a₁ * a₂: M
a₂, 1: ?m.2869
1) :=
  by
Goals accomplished! 🐙 A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M

(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)rw [A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M

(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)mk_mul_mk: ∀ {M : Type ?u.3086} {N : Type ?u.3087} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M

(a₁ * a₂, 1 * 1) = (a₁ * a₂, 1) A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M

(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)mul_one: ∀ {M : Type ?u.3289} [inst : MulOneClass M] (a : M), a * 1 = a
mul_oneA: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M

(a₁ * a₂, 1) = (a₁ * a₂, 1)]
Goals accomplished! 🐙
#align prod.mk_one_mul_mk_one Prod.mk_one_mul_mk_one: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Monoid N] (a₁ a₂ : M), (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
Prod.mk_one_mul_mk_one
#align prod.mk_zero_add_mk_zero Prod.mk_zero_add_mk_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : AddMonoid N] (a₁ a₂ : M), (a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
Prod.mk_zero_add_mk_zero

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Zero M] → [inst : Zero N] → Zero (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : One M] → [inst : One N] → One (M × N)
instance [One: Type ?u.3442 → Type ?u.3442
One M: Type ?u.3433
M] [One: Type ?u.3445 → Type ?u.3445
One N: Type ?u.3436
N] : One: Type ?u.3448 → Type ?u.3448
One (M: Type ?u.3433
M × N: Type ?u.3436
N) :=
  ⟨(1: ?m.3466
1, 1: ?m.3488
1)⟩

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.fst = 0
to_additive (attr := simp)]
theorem fst_one: ∀ [inst : One M] [inst_1 : One N], 1.fst = 1
fst_one [One: Type ?u.3681 → Type ?u.3681
One M: Type ?u.3672
M] [One: Type ?u.3684 → Type ?u.3684
One N: Type ?u.3675
N] : (1: ?m.3692
1 : M: Type ?u.3672
M × N: Type ?u.3675
N).1: {α : Type ?u.3747} → {β : Type ?u.3746} → α × β → α
1 = 1: ?m.3751
1 :=
  rfl: ∀ {α : Sort ?u.3787} {a : α}, a = a
rfl
#align prod.fst_one Prod.fst_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1.fst = 1
Prod.fst_one
#align prod.fst_zero Prod.fst_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.fst = 0
Prod.fst_zero

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.snd = 0
to_additive (attr := simp)]
theorem snd_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1.snd = 1
snd_one [One: Type ?u.3861 → Type ?u.3861
One M: Type ?u.3852
M] [One: Type ?u.3864 → Type ?u.3864
One N: Type ?u.3855
N] : (1: ?m.3872
1 : M: Type ?u.3852
M × N: Type ?u.3855
N).2: {α : Type ?u.3927} → {β : Type ?u.3926} → α × β → β
2 = 1: ?m.3931
1 :=
  rfl: ∀ {α : Sort ?u.3967} {a : α}, a = a
rfl
#align prod.snd_one Prod.snd_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1.snd = 1
Prod.snd_one
#align prod.snd_zero Prod.snd_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.snd = 0
Prod.snd_zero

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0 = (0, 0)
to_additive]
theorem one_eq_mk: ∀ [inst : One M] [inst_1 : One N], 1 = (1, 1)
one_eq_mk [One: Type ?u.4041 → Type ?u.4041
One M: Type ?u.4032
M] [One: Type ?u.4044 → Type ?u.4044
One N: Type ?u.4035
N] : (1: ?m.4052
1 : M: Type ?u.4032
M × N: Type ?u.4035
N) = (1: ?m.4111
1, 1: ?m.4121
1) :=
  rfl: ∀ {α : Sort ?u.4206} {a : α}, a = a
rfl
#align prod.one_eq_mk Prod.one_eq_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1 = (1, 1)
Prod.one_eq_mk
#align prod.zero_eq_mk Prod.zero_eq_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0 = (0, 0)
Prod.zero_eq_mk

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] {x : M} {y : N}, (x, y) = 0 ↔ x = 0 ∧ y = 0
to_additive (attr := simp)]
theorem mk_eq_one: ∀ [inst : One M] [inst_1 : One N] {x : M} {y : N}, (x, y) = 1 ↔ x = 1 ∧ y = 1
mk_eq_one [One: Type ?u.4254 → Type ?u.4254
One M: Type ?u.4245
M] [One: Type ?u.4257 → Type ?u.4257
One N: Type ?u.4248
N] {x: M
x : M: Type ?u.4245
M} {y: N
y : N: Type ?u.4248
N} : (x: M
x, y: N
y) = 1: ?m.4270
1 ↔ x: M
x = 1: ?m.4338
1 ∧ y: N
y = 1: ?m.4373
1 :=
  mk.inj_iff: ∀ {α : Type ?u.4411} {β : Type ?u.4412} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
#align prod.mk_eq_one Prod.mk_eq_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N] {x : M} {y : N}, (x, y) = 1 ↔ x = 1 ∧ y = 1
Prod.mk_eq_one
#align prod.mk_eq_zero Prod.mk_eq_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] {x : M} {y : N}, (x, y) = 0 ↔ x = 0 ∧ y = 0
Prod.mk_eq_zero

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], swap 0 = 0
to_additive (attr := simp)]
theorem swap_one: ∀ [inst : One M] [inst_1 : One N], swap 1 = 1
swap_one [One: Type ?u.4552 → Type ?u.4552
One M: Type ?u.4543
M] [One: Type ?u.4555 → Type ?u.4555
One N: Type ?u.4546
N] : (1: ?m.4563
1 : M: Type ?u.4543
M × N: Type ?u.4546
N).swap: {α : Type ?u.4618} → {β : Type ?u.4617} → α × β → β × α
swap = 1: ?m.4625
1 :=
  rfl: ∀ {α : Sort ?u.4681} {a : α}, a = a
rfl
#align prod.swap_one Prod.swap_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], swap 1 = 1
Prod.swap_one
#align prod.swap_zero Prod.swap_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], swap 0 = 0
Prod.swap_zero

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (p : M × N),
  (p.fst, 0) + (0, p.snd) = p
to_additive]
theorem fst_mul_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (p : M × N), (p.fst, 1) * (1, p.snd) = p
fst_mul_snd [MulOneClass: Type ?u.4765 → Type ?u.4765
MulOneClass M: Type ?u.4756
M] [MulOneClass: Type ?u.4768 → Type ?u.4768
MulOneClass N: Type ?u.4759
N] (p: M × N
p : M: Type ?u.4756
M × N: Type ?u.4759
N) : (p: M × N
p.fst: {α : Type ?u.4784} → {β : Type ?u.4783} → α × β → α
fst, 1: ?m.4790
1) * (1: ?m.4804
1, p: M × N
p.snd: {α : Type ?u.4814} → {β : Type ?u.4813} → α × β → β
snd) = p: M × N
p :=
  ext: ∀ {α : Type ?u.5462} {β : Type ?u.5463} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (mul_one: ∀ {M : Type ?u.5473} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one p: M × N
p.1: {α : Type ?u.5477} → {β : Type ?u.5476} → α × β → α
1) (one_mul: ∀ {M : Type ?u.5492} [inst : MulOneClass M] (a : M), 1 * a = a
one_mul p: M × N
p.2: {α : Type ?u.5496} → {β : Type ?u.5495} → α × β → β
2)
#align prod.fst_mul_snd Prod.fst_mul_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (p : M × N), (p.fst, 1) * (1, p.snd) = p
Prod.fst_mul_snd
#align prod.fst_add_snd Prod.fst_add_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (p : M × N),
  (p.fst, 0) + (0, p.snd) = p
Prod.fst_add_snd

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Neg M] → [inst : Neg N] → Neg (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Inv M] → [inst : Inv N] → Inv (M × N)
instance [Inv: Type ?u.5558 → Type ?u.5558
Inv M: Type ?u.5549
M] [Inv: Type ?u.5561 → Type ?u.5561
Inv N: Type ?u.5552
N] : Inv: Type ?u.5564 → Type ?u.5564
Inv (M: Type ?u.5549
M × N: Type ?u.5552
N) :=
  ⟨fun p: ?m.5576
p => (p: ?m.5576
p.1: {α : Type ?u.5604} → {β : Type ?u.5603} → α × β → α
1⁻¹, p: ?m.5576
p.2: {α : Type ?u.5635} → {β : Type ?u.5634} → α × β → β
2⁻¹)⟩

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).fst = -p.fst
to_additive (attr := simp)]
theorem fst_inv: ∀ [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.fst = p.fst⁻¹
fst_inv [Inv: Type ?u.5889 → Type ?u.5889
Inv G: Type ?u.5874
G] [Inv: Type ?u.5892 → Type ?u.5892
Inv H: Type ?u.5877
H] (p: G × H
p : G: Type ?u.5874
G × H: Type ?u.5877
H) : p: G × H
p⁻¹.1: {α : Type ?u.5938} → {β : Type ?u.5937} → α × β → α
1 = p: G × H
p.1: {α : Type ?u.5945} → {β : Type ?u.5944} → α × β → α
1⁻¹ :=
  rfl: ∀ {α : Sort ?u.5959} {a : α}, a = a
rfl
#align prod.fst_inv Prod.fst_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.fst = p.fst⁻¹
Prod.fst_inv
#align prod.fst_neg Prod.fst_neg: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).fst = -p.fst
Prod.fst_neg

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).snd = -p.snd
to_additive (attr := simp)]
theorem snd_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.snd = p.snd⁻¹
snd_inv [Inv: Type ?u.6042 → Type ?u.6042
Inv G: Type ?u.6027
G] [Inv: Type ?u.6045 → Type ?u.6045
Inv H: Type ?u.6030
H] (p: G × H
p : G: Type ?u.6027
G × H: Type ?u.6030
H) : p: G × H
p⁻¹.2: {α : Type ?u.6091} → {β : Type ?u.6090} → α × β → β
2 = p: G × H
p.2: {α : Type ?u.6098} → {β : Type ?u.6097} → α × β → β
2⁻¹ :=
  rfl: ∀ {α : Sort ?u.6112} {a : α}, a = a
rfl
#align prod.snd_inv Prod.snd_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.snd = p.snd⁻¹
Prod.snd_inv
#align prod.snd_neg Prod.snd_neg: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).snd = -p.snd
Prod.snd_neg

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (a : G) (b : H), -(a, b) = (-a, -b)
to_additive (attr := simp)]
theorem inv_mk: ∀ [inst : Inv G] [inst_1 : Inv H] (a : G) (b : H), (a, b)⁻¹ = (a⁻¹, b⁻¹)
inv_mk [Inv: Type ?u.6195 → Type ?u.6195
Inv G: Type ?u.6180
G] [Inv: Type ?u.6198 → Type ?u.6198
Inv H: Type ?u.6183
H] (a: G
a : G: Type ?u.6180
G) (b: H
b : H: Type ?u.6183
H) : (a: G
a, b: H
b)⁻¹ = (a: G
a⁻¹, b: H
b⁻¹) :=
  rfl: ∀ {α : Sort ?u.6311} {a : α}, a = a
rfl
#align prod.inv_mk Prod.inv_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (a : G) (b : H), (a, b)⁻¹ = (a⁻¹, b⁻¹)
Prod.inv_mk
#align prod.neg_mk Prod.neg_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (a : G) (b : H), -(a, b) = (-a, -b)
Prod.neg_mk

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), swap (-p) = -swap p
to_additive (attr := simp)]
theorem swap_inv: ∀ [inst : Inv G] [inst_1 : Inv H] (p : G × H), swap p⁻¹ = (swap p)⁻¹
swap_inv [Inv: Type ?u.6417 → Type ?u.6417
Inv G: Type ?u.6402
G] [Inv: Type ?u.6420 → Type ?u.6420
Inv H: Type ?u.6405
H] (p: G × H
p : G: Type ?u.6402
G × H: Type ?u.6405
H) : p: G × H
p⁻¹.swap: {α : Type ?u.6466} → {β : Type ?u.6465} → α × β → β × α
swap = p: G × H
p.swap: {α : Type ?u.6476} → {β : Type ?u.6475} → α × β → β × α
swap⁻¹ :=
  rfl: ∀ {α : Sort ?u.6513} {a : α}, a = a
rfl
#align prod.swap_inv Prod.swap_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), swap p⁻¹ = (swap p)⁻¹
Prod.swap_inv
#align prod.swap_neg Prod.swap_neg: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), swap (-p) = -swap p
Prod.swap_neg

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : InvolutiveNeg M] → [inst : InvolutiveNeg N] → InvolutiveNeg (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : InvolutiveInv M] → [inst : InvolutiveInv N] → InvolutiveInv (M × N)
instance [InvolutiveInv: Type ?u.6608 → Type ?u.6608
InvolutiveInv M: Type ?u.6599
M] [InvolutiveInv: Type ?u.6611 → Type ?u.6611
InvolutiveInv N: Type ?u.6602
N] : InvolutiveInv: Type ?u.6614 → Type ?u.6614
InvolutiveInv (M: Type ?u.6599
M × N: Type ?u.6602
N) :=
  { inv_inv := fun _: ?m.6786
_ => ext: ∀ {α : Type ?u.6788} {β : Type ?u.6789} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (inv_inv: ∀ {G : Type ?u.6799} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
inv_inv _: ?m.6800
_) (inv_inv: ∀ {G : Type ?u.6821} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
inv_inv _: ?m.6822
_) }

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Sub M] → [inst : Sub N] → Sub (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Div M] → [inst : Div N] → Div (M × N)
instance [Div: Type ?u.7024 → Type ?u.7024
Div M: Type ?u.7015
M] [Div: Type ?u.7027 → Type ?u.7027
Div N: Type ?u.7018
N] : Div: Type ?u.7030 → Type ?u.7030
Div (M: Type ?u.7015
M × N: Type ?u.7018
N) :=
  ⟨fun p: ?m.7042
p q: ?m.7045
q => ⟨p: ?m.7042
p.1: {α : Type ?u.7061} → {β : Type ?u.7060} → α × β → α
1 / q: ?m.7045
q.1: {α : Type ?u.7065} → {β : Type ?u.7064} → α × β → α
1, p: ?m.7042
p.2: {α : Type ?u.7109} → {β : Type ?u.7108} → α × β → β
2 / q: ?m.7045
q.2: {α : Type ?u.7113} → {β : Type ?u.7112} → α × β → β
2⟩⟩

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).fst = a.fst - b.fst
to_additive (attr := simp)]
theorem fst_div: ∀ [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).fst = a.fst / b.fst
fst_div [Div: Type ?u.7496 → Type ?u.7496
Div G: Type ?u.7481
G] [Div: Type ?u.7499 → Type ?u.7499
Div H: Type ?u.7484
H] (a: G × H
a b: G × H
b : G: Type ?u.7481
G × H: Type ?u.7484
H) : (a: G × H
a / b: G × H
b).1: {α : Type ?u.7585} → {β : Type ?u.7584} → α × β → α
1 = a: G × H
a.1: {α : Type ?u.7594} → {β : Type ?u.7593} → α × β → α
1 / b: G × H
b.1: {α : Type ?u.7598} → {β : Type ?u.7597} → α × β → α
1 :=
  rfl: ∀ {α : Sort ?u.7642} {a : α}, a = a
rfl
#align prod.fst_div Prod.fst_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).fst = a.fst / b.fst
Prod.fst_div
#align prod.fst_sub Prod.fst_sub: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).fst = a.fst - b.fst
Prod.fst_sub

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).snd = a.snd - b.snd
to_additive (attr := simp)]
theorem snd_div: ∀ [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).snd = a.snd / b.snd
snd_div [Div: Type ?u.7740 → Type ?u.7740
Div G: Type ?u.7725
G] [Div: Type ?u.7743 → Type ?u.7743
Div H: Type ?u.7728
H] (a: G × H
a b: G × H
b : G: Type ?u.7725
G × H: Type ?u.7728
H) : (a: G × H
a / b: G × H
b).2: {α : Type ?u.7829} → {β : Type ?u.7828} → α × β → β
2 = a: G × H
a.2: {α : Type ?u.7838} → {β : Type ?u.7837} → α × β → β
2 / b: G × H
b.2: {α : Type ?u.7842} → {β : Type ?u.7841} → α × β → β
2 :=
  rfl: ∀ {α : Sort ?u.7886} {a : α}, a = a
rfl
#align prod.snd_div Prod.snd_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).snd = a.snd / b.snd
Prod.snd_div
#align prod.snd_sub Prod.snd_sub: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).snd = a.snd - b.snd
Prod.snd_sub

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (x₁ x₂ : G) (y₁ y₂ : H),
  (x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
to_additive (attr := simp)]
theorem mk_div_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (x₁ x₂ : G) (y₁ y₂ : H),
  (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
mk_div_mk [Div: Type ?u.7984 → Type ?u.7984
Div G: Type ?u.7969
G] [Div: Type ?u.7987 → Type ?u.7987
Div H: Type ?u.7972
H] (x₁: G
x₁ x₂: G
x₂ : G: Type ?u.7969
G) (y₁: H
y₁ y₂: H
y₂ : H: Type ?u.7972
H) :
    (x₁: G
x₁, y₁: H
y₁) / (x₂: G
x₂, y₂: H
y₂) = (x₁: G
x₁ / x₂: G
x₂, y₁: H
y₁ / y₂: H
y₂) :=
  rfl: ∀ {α : Sort ?u.8170} {a : α}, a = a
rfl
#align prod.mk_div_mk Prod.mk_div_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (x₁ x₂ : G) (y₁ y₂ : H),
  (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
Prod.mk_div_mk
#align prod.mk_sub_mk Prod.mk_sub_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (x₁ x₂ : G) (y₁ y₂ : H),
  (x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
Prod.mk_sub_mk

@[to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), swap (a - b) = swap a - swap b
to_additive (attr := simp)]
theorem swap_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), swap (a / b) = swap a / swap b
swap_div [Div: Type ?u.8302 → Type ?u.8302
Div G: Type ?u.8287
G] [Div: Type ?u.8305 → Type ?u.8305
Div H: Type ?u.8290
H] (a: G × H
a b: G × H
b : G: Type ?u.8287
G × H: Type ?u.8290
H) : (a: G × H
a / b: G × H
b).swap: {α : Type ?u.8391} → {β : Type ?u.8390} → α × β → β × α
swap = a: G × H
a.swap: {α : Type ?u.8403} → {β : Type ?u.8402} → α × β → β × α
swap / b: G × H
b.swap: {α : Type ?u.8410} → {β : Type ?u.8409} → α × β → β × α
swap :=
  rfl: ∀ {α : Sort ?u.8477} {a : α}, a = a
rfl
#align prod.swap_div Prod.swap_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), swap (a / b) = swap a / swap b
Prod.swap_div
#align prod.swap_sub Prod.swap_sub: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), swap (a - b) = swap a - swap b
Prod.swap_sub

instance: {M : Type u_1} → {N : Type u_2} → [inst : MulZeroClass M] → [inst : MulZeroClass N] → MulZeroClass (M × N)
instance [MulZeroClass: Type ?u.8589 → Type ?u.8589
MulZeroClass M: Type ?u.8580
M] [MulZeroClass: Type ?u.8592 → Type ?u.8592
MulZeroClass N: Type ?u.8583
N] : MulZeroClass: Type ?u.8595 → Type ?u.8595
MulZeroClass (M: Type ?u.8580
M × N: Type ?u.8583
N) :=
  { zero_mul := fun a: ?m.8805
a => Prod.recOn: ∀ {α : Type ?u.8808} {β : Type ?u.8807} {motive : α × β → Sort ?u.8809} (t : α × β),
  (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn a: ?m.8805
a fun _: ?m.8880
_ _: ?m.8883
_ => mk.inj_iff: ∀ {α : Type ?u.8885} {β : Type ?u.8886} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨zero_mul: ∀ {M₀ : Type ?u.8909} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul _: ?m.8910
_, zero_mul: ∀ {M₀ : Type ?u.8940} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul _: ?m.8941
_⟩,
    mul_zero := fun a: ?m.8845
a => Prod.recOn: ∀ {α : Type ?u.8848} {β : Type ?u.8847} {motive : α × β → Sort ?u.8849} (t : α × β),
  (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn a: ?m.8845
a fun _: ?m.8979
_ _: ?m.8982
_ => mk.inj_iff: ∀ {α : Type ?u.8984} {β : Type ?u.8985} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨mul_zero: ∀ {M₀ : Type ?u.9000} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero _: ?m.9001
_, mul_zero: ∀ {M₀ : Type ?u.9010} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero _: ?m.9011
_⟩ }

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddSemigroup M] → [inst : AddSemigroup N] → AddSemigroup (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Semigroup M] → [inst : Semigroup N] → Semigroup (M × N)
instance [Semigroup: Type ?u.9130 → Type ?u.9130
Semigroup M: Type ?u.9121
M] [Semigroup: Type ?u.9133 → Type ?u.9133
Semigroup N: Type ?u.9124
N] : Semigroup: Type ?u.9136 → Type ?u.9136
Semigroup (M: Type ?u.9121
M × N: Type ?u.9124
N) :=
  { mul_assoc := fun _: ?m.9522
_ _: ?m.9525
_ _: ?m.9528
_ => mk.inj_iff: ∀ {α : Type ?u.9530} {β : Type ?u.9531} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨mul_assoc: ∀ {G : Type ?u.9559} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc _: ?m.9560
_ _: ?m.9560
_ _: ?m.9560
_, mul_assoc: ∀ {G : Type ?u.9595} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc _: ?m.9596
_ _: ?m.9596
_ _: ?m.9596
_⟩ }

@[to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddCommSemigroup G] → [inst : AddCommSemigroup H] → AddCommSemigroup (G × H)
to_additive]
instance: {G : Type u_1} → {H : Type u_2} → [inst : CommSemigroup G] → [inst : CommSemigroup H] → CommSemigroup (G × H)
instance [CommSemigroup: Type ?u.9826 → Type ?u.9826
CommSemigroup G: Type ?u.9811
G] [CommSemigroup: Type ?u.9829 → Type ?u.9829
CommSemigroup H: Type ?u.9814
H] : CommSemigroup: Type ?u.9832 → Type ?u.9832
CommSemigroup (G: Type ?u.9811
G × H: Type ?u.9814
H) :=
  { mul_comm := fun _: ?m.10202
_ _: ?m.10205
_ => mk.inj_iff: ∀ {α : Type ?u.10207} {β : Type ?u.10208} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨mul_comm: ∀ {G : Type ?u.10236} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm _: ?m.10237
_ _: ?m.10237
_, mul_comm: ∀ {G : Type ?u.10261} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm _: ?m.10262
_ _: ?m.10262
_⟩ }

instance: {M : Type u_1} →
  {N : Type u_2} → [inst : SemigroupWithZero M] → [inst : SemigroupWithZero N] → SemigroupWithZero (M × N)
instance [SemigroupWithZero: Type ?u.10474 → Type ?u.10474
SemigroupWithZero M: Type ?u.10465
M] [SemigroupWithZero: Type ?u.10477 → Type ?u.10477
SemigroupWithZero N: Type ?u.10468
N] : SemigroupWithZero: Type ?u.10480 → Type ?u.10480
SemigroupWithZero (M: Type ?u.10465
M × N: Type ?u.10468
N) :=
  { zero_mul := : SemigroupWithZero ?m.10487
{ zero_mul{ zero_mul := : SemigroupWithZero ?m.10487
 := by
Goals accomplished! 🐙 A: Type ?u.10453

B: Type ?u.10456

G: Type ?u.10459

H: Type ?u.10462

M: Type ?u.10465

N: Type ?u.10468

P: Type ?u.10471

inst✝¹: SemigroupWithZero M

inst✝: SemigroupWithZero N

∀ (a : M × N), 0 * a = 0simp
Goals accomplished! 🐙,
    mul_zero := : SemigroupWithZero ?m.10487,
    mul_zero,
    mul_zero := : SemigroupWithZero ?m.10487
 := by
Goals accomplished! 🐙 A: Type ?u.10453

B: Type ?u.10456

G: Type ?u.10459

H: Type ?u.10462

M: Type ?u.10465

N: Type ?u.10468

P: Type ?u.10471

inst✝¹: SemigroupWithZero M

inst✝: SemigroupWithZero N

∀ (a : M × N), a * 0 = 0simp
Goals accomplished! 🐙 }: SemigroupWithZero ?m.10487
 }

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst : AddZeroClass N] → AddZeroClass (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst : MulOneClass N] → MulOneClass (M × N)
instance [MulOneClass: Type ?u.12227 → Type ?u.12227
MulOneClass M: Type ?u.12218
M] [MulOneClass: Type ?u.12230 → Type ?u.12230
MulOneClass N: Type ?u.12221
N] : MulOneClass: Type ?u.12233 → Type ?u.12233
MulOneClass (M: Type ?u.12218
M × N: Type ?u.12221
N) :=
  { one_mul := fun a: ?m.12762
a => Prod.recOn: ∀ {α : Type ?u.12765} {β : Type ?u.12764} {motive : α × β → Sort ?u.12766} (t : α × β),
  (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn a: ?m.12762
a fun _: ?m.12837
_ _: ?m.12840
_ => mk.inj_iff: ∀ {α : Type ?u.12842} {β : Type ?u.12843} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨one_mul: ∀ {M : Type ?u.12866} [inst : MulOneClass M] (a : M), 1 * a = a
one_mul _: ?m.12867
_, one_mul: ∀ {M : Type ?u.12900} [inst : MulOneClass M] (a : M), 1 * a = a
one_mul _: ?m.12901
_⟩,
    mul_one := fun a: ?m.12802
a => Prod.recOn: ∀ {α : Type ?u.12805} {β : Type ?u.12804} {motive : α × β → Sort ?u.12806} (t : α × β),
  (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn a: ?m.12802
a fun _: ?m.12942
_ _: ?m.12945
_ => mk.inj_iff: ∀ {α : Type ?u.12947} {β : Type ?u.12948} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨mul_one: ∀ {M : Type ?u.12963} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one _: ?m.12964
_, mul_one: ∀ {M : Type ?u.12976} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one _: ?m.12977
_⟩ }

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddMonoid M] → [inst : AddMonoid N] → AddMonoid (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Monoid M] → [inst : Monoid N] → Monoid (M × N)
instance [Monoid: Type ?u.13214 → Type ?u.13214
Monoid M: Type ?u.13205
M] [Monoid: Type ?u.13217 → Type ?u.13217
Monoid N: Type ?u.13208
N] : Monoid: Type ?u.13220 → Type ?u.13220
Monoid (M: Type ?u.13205
M × N: Type ?u.13208
N) :=
  { npow := fun z: ?m.13601
z a: ?m.13604
a => ⟨Monoid.npow: {M : Type ?u.13616} → [self : Monoid M] → ℕ → M → M
Monoid.npow z: ?m.13601
z a: ?m.13604
a.1: {α : Type ?u.13633} → {β : Type ?u.13632} → α × β → α
1, Monoid.npow: {M : Type ?u.13642} → [self : Monoid M] → ℕ → M → M
Monoid.npow z: ?m.13601
z a: ?m.13604
a.2: {α : Type ?u.13659} → {β : Type ?u.13658} → α × β → β
2⟩,
    npow_zero := fun z: ?m.13673
z => ext: ∀ {α : Type ?u.13675} {β : Type ?u.13676} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (Monoid.npow_zero: ∀ {M : Type ?u.13688} [self : Monoid M] (x : M), Monoid.npow 0 x = 1
Monoid.npow_zero _: ?m.13689
_) (Monoid.npow_zero: ∀ {M : Type ?u.13714} [self : Monoid M] (x : M), Monoid.npow 0 x = 1
Monoid.npow_zero _: ?m.13715
_),
    npow_succ := fun z: ?m.13746
z a: ?m.13749
a => ext: ∀ {α : Type ?u.13751} {β : Type ?u.13752} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (Monoid.npow_succ: ∀ {M : Type ?u.13761} [self : Monoid M] (n : ℕ) (x : M), Monoid.npow (n + 1) x = x * Monoid.npow n x
Monoid.npow_succ _: ℕ
_ _: ?m.13762
_) (Monoid.npow_succ: ∀ {M : Type ?u.13785} [self : Monoid M] (n : ℕ) (x : M), Monoid.npow (n + 1) x = x * Monoid.npow n x
Monoid.npow_succ _: ℕ
_ _: ?m.13786
_),
    one_mul := by
Goals accomplished! 🐙 A: Type ?u.13193

B: Type ?u.13196

G: Type ?u.13199

H: Type ?u.13202

M: Type ?u.13205

N: Type ?u.13208

P: Type ?u.13211

inst✝¹: Monoid M

inst✝: Monoid N

∀ (a : M × N), 1 * a = asimp
Goals accomplished! 🐙,
    mul_one := by
Goals accomplished! 🐙 A: Type ?u.13193

B: Type ?u.13196

G: Type ?u.13199

H: Type ?u.13202

M: Type ?u.13205

N: Type ?u.13208

P: Type ?u.13211

inst✝¹: Monoid M

inst✝: Monoid N

∀ (a : M × N), a * 1 = asimp
Goals accomplished! 🐙 }

@[to_additive Prod.subNegMonoid: {G : Type u_1} → {H : Type u_2} → [inst : SubNegMonoid G] → [inst : SubNegMonoid H] → SubNegMonoid (G × H)
Prod.subNegMonoid]
instance: {G : Type u_1} → {H : Type u_2} → [inst : DivInvMonoid G] → [inst : DivInvMonoid H] → DivInvMonoid (G × H)
instance [DivInvMonoid: Type ?u.15470 → Type ?u.15470
DivInvMonoid G: Type ?u.15455
G] [DivInvMonoid: Type ?u.15473 → Type ?u.15473
DivInvMonoid H: Type ?u.15458
H] : DivInvMonoid: Type ?u.15476 → Type ?u.15476
DivInvMonoid (G: Type ?u.15455
G × H: Type ?u.15458
H) :=
  { div_eq_mul_inv := fun _: ?m.15784
_ _: ?m.15787
_ => mk.inj_iff: ∀ {α : Type ?u.15789} {β : Type ?u.15790} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨div_eq_mul_inv: ∀ {G : Type ?u.15818} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv _: ?m.15819
_ _: ?m.15819
_, div_eq_mul_inv: ∀ {G : Type ?u.15853} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv _: ?m.15854
_ _: ?m.15854
_⟩,
    zpow := fun z: ?m.15896
z a: ?m.15899
a => ⟨DivInvMonoid.zpow: {G : Type ?u.15909} → [self : DivInvMonoid G] → ℤ → G → G
DivInvMonoid.zpow z: ?m.15896
z a: ?m.15899
a.1: {α : Type ?u.15923} → {β : Type ?u.15922} → α × β → α
1, DivInvMonoid.zpow: {G : Type ?u.15926} → [self : DivInvMonoid G] → ℤ → G → G
DivInvMonoid.zpow z: ?m.15896
z a: ?m.15899
a.2: {α : Type ?u.15940} → {β : Type ?u.15939} → α × β → β
2⟩,
    zpow_zero' := fun _: ?m.15948
_ => ext: ∀ {α : Type ?u.15950} {β : Type ?u.15951} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (DivInvMonoid.zpow_zero': ∀ {G : Type ?u.15960} [self : DivInvMonoid G] (a : G), DivInvMonoid.zpow 0 a = 1
DivInvMonoid.zpow_zero' _: ?m.15961
_) (DivInvMonoid.zpow_zero': ∀ {G : Type ?u.15980} [self : DivInvMonoid G] (a : G), DivInvMonoid.zpow 0 a = 1
DivInvMonoid.zpow_zero' _: ?m.15981
_),
    zpow_succ' := fun _: ?m.16006
_ _: ?m.16009
_ => ext: ∀ {α : Type ?u.16011} {β : Type ?u.16012} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (DivInvMonoid.zpow_succ': ∀ {G : Type ?u.16021} [self : DivInvMonoid G] (n : ℕ) (a : G),
  DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
DivInvMonoid.zpow_succ' _: ℕ
_ _: ?m.16022
_) (DivInvMonoid.zpow_succ': ∀ {G : Type ?u.16041} [self : DivInvMonoid G] (n : ℕ) (a : G),
  DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
DivInvMonoid.zpow_succ' _: ℕ
_ _: ?m.16042
_),
    zpow_neg' := fun _: ?m.16065
_ _: ?m.16068
_ => ext: ∀ {α : Type ?u.16070} {β : Type ?u.16071} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (DivInvMonoid.zpow_neg': ∀ {G : Type ?u.16080} [self : DivInvMonoid G] (n : ℕ) (a : G),
  DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
DivInvMonoid.zpow_neg' _: ℕ
_ _: ?m.16081
_) (DivInvMonoid.zpow_neg': ∀ {G : Type ?u.16101} [self : DivInvMonoid G] (n : ℕ) (a : G),
  DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
DivInvMonoid.zpow_neg' _: ℕ
_ _: ?m.16102
_) }

@[to_additive: {G : Type u_1} →
  {H : Type u_2} → [inst : SubtractionMonoid G] → [inst : SubtractionMonoid H] → SubtractionMonoid (G × H)
to_additive]
instance: {G : Type u_1} → {H : Type u_2} → [inst : DivisionMonoid G] → [inst : DivisionMonoid H] → DivisionMonoid (G × H)
instance [DivisionMonoid: Type ?u.16670 → Type ?u.16670
DivisionMonoid G: Type ?u.16655
G] [DivisionMonoid: Type ?u.16673 → Type ?u.16673
DivisionMonoid H: Type ?u.16658
H] : DivisionMonoid: Type ?u.16676 → Type ?u.16676
DivisionMonoid (G: Type ?u.16655
G × H: Type ?u.16658
H) :=
  { mul_inv_rev := fun a: ?m.16756
a b: ?m.16759
b => ext: ∀ {α : Type ?u.16761} {β : Type ?u.16762} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (mul_inv_rev: ∀ {G : Type ?u.16772} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev _: ?m.16773
_ _: ?m.16773
_) (mul_inv_rev: ∀ {G : Type ?u.16816} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev _: ?m.16817
_ _: ?m.16817
_),
    inv_eq_of_mul := fun a: ?m.16868
a b: ?m.16871
b h: ?m.16874
h =>
      ext: ∀ {α : Type ?u.16876} {β : Type ?u.16877} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext (inv_eq_of_mul_eq_one_right: ∀ {G : Type ?u.16884} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a⁻¹ = b
inv_eq_of_mul_eq_one_right <| congr_arg: ∀ {α : Sort ?u.16898} {β : Sort ?u.16897} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg fst: {α : Type ?u.16904} → {β : Type ?u.16903} → α × β → α
fst h: ?m.16874
h)
        (inv_eq_of_mul_eq_one_right: ∀ {G : Type ?u.16915} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a⁻¹ = b
inv_eq_of_mul_eq_one_right <| congr_arg: ∀ {α : Sort ?u.16929} {β : Sort ?u.16928} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg snd: {α : Type ?u.16935} → {β : Type ?u.16934} → α × β → β
snd h: ?m.16874
h),
    inv_inv := by
Goals accomplished! 🐙 A: Type ?u.16649

B: Type ?u.16652

G: Type ?u.16655

H: Type ?u.16658

M: Type ?u.16661

N: Type ?u.16664

P: Type ?u.16667

inst✝¹: DivisionMonoid G

inst✝: DivisionMonoid H

∀ (x : G × H), x⁻¹⁻¹ = xsimp
Goals accomplished! 🐙 }

@[to_additive SubtractionCommMonoid: {G : Type u_1} →
  {H : Type u_2} →
    [inst : _root_.SubtractionCommMonoid G] →
      [inst : _root_.SubtractionCommMonoid H] → _root_.SubtractionCommMonoid (G × H)
SubtractionCommMonoid]
instance: {G : Type u_1} →
  {H : Type u_2} → [inst : DivisionCommMonoid G] → [inst : DivisionCommMonoid H] → DivisionCommMonoid (G × H)
instance [DivisionCommMonoid: Type ?u.17831 → Type ?u.17831
DivisionCommMonoid G: Type ?u.17816
G] [DivisionCommMonoid: Type ?u.17834 → Type ?u.17834
DivisionCommMonoid H: Type ?u.17819
H] : DivisionCommMonoid: Type ?u.17837 → Type ?u.17837
DivisionCommMonoid (G: Type ?u.17816
G × H: Type ?u.17819
H) :=
  { mul_comm := fun ⟨g₁: G
g₁ , h₁: H
h₁⟩ ⟨_, _⟩ => by
Goals accomplished! 🐙 A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)rw [A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)mk_mul_mk: ∀ {M : Type ?u.18059} {N : Type ?u.18060} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁ * fst✝, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁) A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)mul_comm: ∀ {G : Type ?u.18395} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm g₁: G
g₁,A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(fst✝ * g₁, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁) A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)mul_comm: ∀ {G : Type ?u.18446} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm h₁: H
h₁A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)]A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁);A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁) A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)rfl
Goals accomplished! 🐙 }

@[to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst : AddGroup H] → AddGroup (G × H)
to_additive]
instance: {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst : Group H] → Group (G × H)
instance [Group: Type ?u.18747 → Type ?u.18747
Group G: Type ?u.18732
G] [Group: Type ?u.18750 → Type ?u.18750
Group H: Type ?u.18735
H] : Group: Type ?u.18753 → Type ?u.18753
Group (G: Type ?u.18732
G × H: Type ?u.18735
H) :=
  { mul_left_inv := fun _: ?m.18814
_ => mk.inj_iff: ∀ {α : Type ?u.18816} {β : Type ?u.18817} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨mul_left_inv: ∀ {G : Type ?u.18845} [inst : Group G] (a : G), a⁻¹ * a = 1
mul_left_inv _: ?m.18846
_, mul_left_inv: ∀ {G : Type ?u.18875} [inst : Group G] (a : G), a⁻¹ * a = 1
mul_left_inv _: ?m.18876
_⟩ }

@[to_additive: {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddLeftCancelSemigroup G] → [inst : AddLeftCancelSemigroup H] → AddLeftCancelSemigroup (G × H)
to_additive]
instance: {G : Type u_1} →
  {H : Type u_2} → [inst : LeftCancelSemigroup G] → [inst : LeftCancelSemigroup H] → LeftCancelSemigroup (G × H)
instance [LeftCancelSemigroup: Type ?u.19086 → Type ?u.19086
LeftCancelSemigroup G: Type ?u.19071
G] [LeftCancelSemigroup: Type ?u.19089 → Type ?u.19089
LeftCancelSemigroup H: Type ?u.19074
H] : LeftCancelSemigroup: Type ?u.19092 → Type ?u.19092
LeftCancelSemigroup (G: Type ?u.19071
G × H: Type ?u.19074
H) :=
  { mul_left_cancel := fun _: ?m.19448
_ _: ?m.19451
_ _: ?m.19454
_ h: ?m.19457
h =>
      Prod.ext: ∀ {α : Type ?u.19459} {β : Type ?u.19460} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (mul_left_cancel: ∀ {G : Type ?u.19470} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
mul_left_cancel (Prod.ext_iff: ∀ {α : Type ?u.19533} {β : Type ?u.19534} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: ?m.19457
h).1: ∀ {a b : Prop}, a ∧ b → a
1) (mul_left_cancel: ∀ {G : Type ?u.19758} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
mul_left_cancel (Prod.ext_iff: ∀ {α : Type ?u.19821} {β : Type ?u.19822} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: ?m.19457
h).2: ∀ {a b : Prop}, a ∧ b → b
2) }

@[to_additive: {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddRightCancelSemigroup G] → [inst : AddRightCancelSemigroup H] → AddRightCancelSemigroup (G × H)
to_additive]
instance: {G : Type u_1} →
  {H : Type u_2} → [inst : RightCancelSemigroup G] → [inst : RightCancelSemigroup H] → RightCancelSemigroup (G × H)
instance [RightCancelSemigroup: Type ?u.20244 → Type ?u.20244
RightCancelSemigroup G: Type ?u.20229
G] [RightCancelSemigroup: Type ?u.20247 → Type ?u.20247
RightCancelSemigroup H: Type ?u.20232
H] : RightCancelSemigroup: Type ?u.20250 → Type ?u.20250
RightCancelSemigroup (G: Type ?u.20229
G × H: Type ?u.20232
H) :=
  { mul_right_cancel := fun _: ?m.20592
_ _: ?m.20595
_ _: ?m.20598
_ h: ?m.20601
h =>
      Prod.ext: ∀ {α : Type ?u.20603} {β : Type ?u.20604} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (mul_right_cancel: ∀ {G : Type ?u.20614} [inst : Mul G] [inst_1 : IsRightCancelMul G] {a b c : G}, a * b = c * b → a = c
mul_right_cancel (Prod.ext_iff: ∀ {α : Type ?u.20677} {β : Type ?u.20678} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: ?m.20601
h).1: ∀ {a b : Prop}, a ∧ b → a
1) (mul_right_cancel: ∀ {G : Type ?u.20899} [inst : Mul G] [inst_1 : IsRightCancelMul G] {a b c : G}, a * b = c * b → a = c
mul_right_cancel (Prod.ext_iff: ∀ {α : Type ?u.20962} {β : Type ?u.20963} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: ?m.20601
h).2: ∀ {a b : Prop}, a ∧ b → b
2) }

@[to_additive: {M : Type u_1} →
  {N : Type u_2} → [inst : AddLeftCancelMonoid M] → [inst : AddLeftCancelMonoid N] → AddLeftCancelMonoid (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : LeftCancelMonoid M] → [inst : LeftCancelMonoid N] → LeftCancelMonoid (M × N)
instance [LeftCancelMonoid: Type ?u.21382 → Type ?u.21382
LeftCancelMonoid M: Type ?u.21373
M] [LeftCancelMonoid: Type ?u.21385 → Type ?u.21385
LeftCancelMonoid N: Type ?u.21376
N] : LeftCancelMonoid: Type ?u.21388 → Type ?u.21388
LeftCancelMonoid (M: Type ?u.21373
M × N: Type ?u.21376
N) :=
  { mul_one := : LeftCancelMonoid ?m.21395
{ mul_one{ mul_one := : LeftCancelMonoid ?m.21395
 := by
Goals accomplished! 🐙 A: Type ?u.21361

B: Type ?u.21364

G: Type ?u.21367

H: Type ?u.21370

M: Type ?u.21373

N: Type ?u.21376

P: Type ?u.21379

inst✝¹: LeftCancelMonoid M

inst✝: LeftCancelMonoid N

∀ (a : M × N), a * 1 = asimp
Goals accomplished! 🐙,
    one_mul := : LeftCancelMonoid ?m.21395,
    one_mul,
    one_mul := : LeftCancelMonoid ?m.21395
 := by
Goals accomplished! 🐙 A: Type ?u.21361

B: Type ?u.21364

G: Type ?u.21367

H: Type ?u.21370

M: Type ?u.21373

N: Type ?u.21376

P: Type ?u.21379

inst✝¹: LeftCancelMonoid M

inst✝: LeftCancelMonoid N

∀ (a : M × N), 1 * a = asimp
Goals accomplished! 🐙 }: LeftCancelMonoid ?m.21395
 }

@[to_additive: {M : Type u_1} →
  {N : Type u_2} → [inst : AddRightCancelMonoid M] → [inst : AddRightCancelMonoid N] → AddRightCancelMonoid (M × N)
to_additive]
instance: {M : Type u_1} →
  {N : Type u_2} → [inst : RightCancelMonoid M] → [inst : RightCancelMonoid N] → RightCancelMonoid (M × N)
instance [RightCancelMonoid: Type ?u.23331 → Type ?u.23331
RightCancelMonoid M: Type ?u.23322
M] [RightCancelMonoid: Type ?u.23334 → Type ?u.23334
RightCancelMonoid N: Type ?u.23325
N] : RightCancelMonoid: Type ?u.23337 → Type ?u.23337
RightCancelMonoid (M: Type ?u.23322
M × N: Type ?u.23325
N) :=
  { mul_one := : RightCancelMonoid ?m.23344
{ mul_one{ mul_one := : RightCancelMonoid ?m.23344
 := by
Goals accomplished! 🐙 A: Type ?u.23310

B: Type ?u.23313

G: Type ?u.23316

H: Type ?u.23319

M: Type ?u.23322

N: Type ?u.23325

P: Type ?u.23328

inst✝¹: RightCancelMonoid M

inst✝: RightCancelMonoid N

∀ (a : M × N), a * 1 = asimp
Goals accomplished! 🐙,
    one_mul := : RightCancelMonoid ?m.23344,
    one_mul,
    one_mul := : RightCancelMonoid ?m.23344
 := by
Goals accomplished! 🐙 A: Type ?u.23310

B: Type ?u.23313

G: Type ?u.23316

H: Type ?u.23319

M: Type ?u.23322

N: Type ?u.23325

P: Type ?u.23328

inst✝¹: RightCancelMonoid M

inst✝: RightCancelMonoid N

∀ (a : M × N), 1 * a = asimp
Goals accomplished! 🐙 }: RightCancelMonoid ?m.23344
 }

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddCancelMonoid M] → [inst : AddCancelMonoid N] → AddCancelMonoid (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : CancelMonoid M] → [inst : CancelMonoid N] → CancelMonoid (M × N)
instance [CancelMonoid: Type ?u.25176 → Type ?u.25176
CancelMonoid M: Type ?u.25167
M] [CancelMonoid: Type ?u.25179 → Type ?u.25179
CancelMonoid N: Type ?u.25170
N] : CancelMonoid: Type ?u.25182 → Type ?u.25182
CancelMonoid (M: Type ?u.25167
M × N: Type ?u.25170
N) :=
  { mul_right_cancel := by
Goals accomplished! 🐙 A: Type ?u.25155

B: Type ?u.25158

G: Type ?u.25161

H: Type ?u.25164

M: Type ?u.25167

N: Type ?u.25170

P: Type ?u.25173

inst✝¹: CancelMonoid M

inst✝: CancelMonoid N

∀ (a b c : M × N), a * b = c * b → a = csimp only [mul_left_inj: ∀ {G : Type ?u.25252} [inst : Mul G] [inst_1 : IsRightCancelMul G] (a : G) {b c : G}, b * a = c * a ↔ b = c
mul_left_inj, imp_self: ∀ {a : Prop}, a → a ↔ True
imp_self, forall_const: ∀ {b : Prop} (α : Sort ?u.25292) [i : Nonempty α], α → b ↔ b
forall_const]
Goals accomplished! 🐙 }

@[to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddCommMonoid M] → [inst : AddCommMonoid N] → AddCommMonoid (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : CommMonoid M] → [inst : CommMonoid N] → CommMonoid (M × N)
instance [CommMonoid: Type ?u.26364 → Type ?u.26364
CommMonoid M: Type ?u.26355
M] [CommMonoid: Type ?u.26367 → Type ?u.26367
CommMonoid N: Type ?u.26358
N] : CommMonoid: Type ?u.26370 → Type ?u.26370
CommMonoid (M: Type ?u.26355
M × N: Type ?u.26358
N) :=
  { mul_comm := fun ⟨m₁: M
m₁, n₁: N
n₁⟩ ⟨_, _⟩ => by
Goals accomplished! 🐙 A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)rw [A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mk_mul_mk: ∀ {M : Type ?u.26822} {N : Type ?u.26823} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁ * fst✝, n₁ * snd✝) = (fst✝, snd✝) * (m₁, n₁) A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mk_mul_mk: ∀ {M : Type ?u.27197} {N : Type ?u.27198} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁ * fst✝, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁) A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mul_comm: ∀ {G : Type ?u.27306} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm m₁: M
m₁,A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(fst✝ * m₁, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁) A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mul_comm: ∀ {G : Type ?u.27326} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm n₁: N
n₁A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(fst✝ * m₁, snd✝ * n₁) = (fst✝ * m₁, snd✝ * n₁)]
Goals accomplished! 🐙 }

@[to_additive: {M : Type u_1} →
  {N : Type u_2} → [inst : AddCancelCommMonoid M] → [inst : AddCancelCommMonoid N] → AddCancelCommMonoid (M × N)
to_additive]
instance: {M : Type u_1} → {N : Type u_2} → [inst : CancelCommMonoid M] → [inst : CancelCommMonoid N] → CancelCommMonoid (M × N)
instance [CancelCommMonoid: Type ?u.27556 → Type ?u.27556
CancelCommMonoid M: Type ?u.27547
M] [CancelCommMonoid: Type ?u.27559 → Type ?u.27559
CancelCommMonoid N: Type ?u.27550
N] : CancelCommMonoid: Type ?u.27562 → Type ?u.27562
CancelCommMonoid (M: Type ?u.27547
M × N: Type ?u.27550
N) :=
  { mul_comm := fun ⟨m₁: M
m₁, n₁: N
n₁⟩ ⟨_, _⟩ => by
Goals accomplished! 🐙 A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)rw [A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mk_mul_mk: ∀ {M : Type ?u.27771} {N : Type ?u.27772} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁ * fst✝, n₁ * snd✝) = (fst✝, snd✝) * (m₁, n₁) A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mk_mul_mk: ∀ {M : Type ?u.28166} {N : Type ?u.28167} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁ * fst✝, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁) A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mul_comm: ∀ {G : Type ?u.28275} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm m₁: M
m₁,A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(fst✝ * m₁, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁) A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)mul_comm: ∀ {G : Type ?u.28321} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm n₁: N
n₁A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N

(fst✝ * m₁, snd✝ * n₁) = (fst✝ * m₁, snd✝ * n₁)]
Goals accomplished! 🐙 }

instance: {M : Type u_1} → {N : Type u_2} → [inst : MulZeroOneClass M] → [inst : MulZeroOneClass N] → MulZeroOneClass (M × N)
instance [MulZeroOneClass: Type ?u.28577 → Type ?u.28577
MulZeroOneClass M: Type ?u.28568
M] [MulZeroOneClass: Type ?u.28580 → Type ?u.28580
MulZeroOneClass N: Type ?u.28571
N] : MulZeroOneClass: Type ?u.28583 → Type ?u.28583
MulZeroOneClass (M: Type ?u.28568
M × N: Type ?u.28571
N) :=
  { zero_mul := : MulZeroOneClass ?m.28590
{ zero_mul{ zero_mul := : MulZeroOneClass ?m.28590
 := by
Goals accomplished! 🐙 A: Type ?u.28556

B: Type ?u.28559

G: Type ?u.28562

H: Type ?u.28565

M: Type ?u.28568

N: Type ?u.28571

P: Type ?u.28574

inst✝¹: MulZeroOneClass M

inst✝: MulZeroOneClass N

∀ (a : M × N), 0 * a = 0simp
Goals accomplished! 🐙,
    mul_zero := : MulZeroOneClass ?m.28590,
    mul_zero,
    mul_zero := : MulZeroOneClass ?m.28590
 := by
Goals accomplished! 🐙 A: Type ?u.28556

B: Type ?u.28559

G: Type ?u.28562

H: Type ?u.28565

M: Type ?u.28568

N: Type ?u.28571

P: Type ?u.28574

inst✝¹: MulZeroOneClass M

inst✝: MulZeroOneClass N

∀ (a : M × N), a * 0 = 0simp
Goals accomplished! 🐙 }: MulZeroOneClass ?m.28590
 }

instance: {M : Type u_1} → {N : Type u_2} → [inst : MonoidWithZero M] → [inst : MonoidWithZero N] → MonoidWithZero (M × N)
instance [MonoidWithZero: Type ?u.30143 → Type ?u.30143
MonoidWithZero M: Type ?u.30134
M] [MonoidWithZero: Type ?u.30146 → Type ?u.30146
MonoidWithZero N: Type ?u.30137
N] : MonoidWithZero: Type ?u.30149 → Type ?u.30149
MonoidWithZero (M: Type ?u.30134
M × N: Type ?u.30137
N) :=
  { zero_mul := : MonoidWithZero ?m.30156
{ zero_mul{ zero_mul := : MonoidWithZero ?m.30156
 := by
Goals accomplished! 🐙 A: Type ?u.30122

B: Type ?u.30125

G: Type ?u.30128

H: Type ?u.30131

M: Type ?u.30134

N: Type ?u.30137

P: Type ?u.30140

inst✝¹: MonoidWithZero M

inst✝: MonoidWithZero N

∀ (a : M × N), 0 * a = 0simp
Goals accomplished! 🐙,
    mul_zero := : MonoidWithZero ?m.30156,
    mul_zero,
    mul_zero := : MonoidWithZero ?m.30156
 := by
Goals accomplished! 🐙 A: Type ?u.30122

B: Type ?u.30125

G: Type ?u.30128

H: Type ?u.30131

M: Type ?u.30134

N: Type ?u.30137

P: Type ?u.30140

inst✝¹: MonoidWithZero M

inst✝: MonoidWithZero N

∀ (a : M × N), a * 0 = 0simp
Goals accomplished! 🐙 }: MonoidWithZero ?m.30156
 }

instance: {M : Type u_1} →
  {N : Type u_2} → [inst : CommMonoidWithZero M] → [inst : CommMonoidWithZero N] → CommMonoidWithZero (M × N)
instance [CommMonoidWithZero: Type ?u.31564 → Type ?u.31564
CommMonoidWithZero M: Type ?u.31555
M] [CommMonoidWithZero: Type ?u.31567 → Type ?u.31567
CommMonoidWithZero N: Type ?u.31558
N] : CommMonoidWithZero: Type ?u.31570 → Type ?u.31570
CommMonoidWithZero (M: Type ?u.31555
M × N: Type ?u.31558
N) :=
  { zero_mul := : CommMonoidWithZero ?m.31577
{ zero_mul{ zero_mul := : CommMonoidWithZero ?m.31577
 := by
Goals accomplished! 🐙 A: Type ?u.31543

B: Type ?u.31546

G: Type ?u.31549

H: Type ?u.31552

M: Type ?u.31555

N: Type ?u.31558

P: Type ?u.31561

inst✝¹: CommMonoidWithZero M

inst✝: CommMonoidWithZero N

∀ (a : M × N), 0 * a = 0simp
Goals accomplished! 🐙,
    mul_zero := : CommMonoidWithZero ?m.31577,
    mul_zero,
    mul_zero := : CommMonoidWithZero ?m.31577
 := by
Goals accomplished! 🐙 A: Type ?u.31543

B: Type ?u.31546

G: Type ?u.31549

H: Type ?u.31552

M: Type ?u.31555

N: Type ?u.31558

P: Type ?u.31561

inst✝¹: CommMonoidWithZero M

inst✝: CommMonoidWithZero N

∀ (a : M × N), a * 0 = 0simp
Goals accomplished! 🐙 }: CommMonoidWithZero ?m.31577
 }

@[to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddCommGroup G] → [inst : AddCommGroup H] → AddCommGroup (G × H)
to_additive]
instance: {G : Type u_1} → {H : Type u_2} → [inst : CommGroup G] → [inst : CommGroup H] → CommGroup (G × H)
instance [CommGroup: Type ?u.32990 → Type ?u.32990
CommGroup G: Type ?u.32975
G] [CommGroup: Type ?u.32993 → Type ?u.32993
CommGroup H: Type ?u.32978
H] : CommGroup: Type ?u.32996 → Type ?u.32996
CommGroup (G: Type ?u.32975
G × H: Type ?u.32978
H) :=
  { mul_comm := fun ⟨g₁: G
g₁, h₁: H
h₁⟩ ⟨_, _⟩ => by
Goals accomplished! 🐙 A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)rw [A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)mk_mul_mk: ∀ {M : Type ?u.33200} {N : Type ?u.33201} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁ * fst✝, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁) A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)mk_mul_mk: ∀ {M : Type ?u.33503} {N : Type ?u.33504} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk,A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁ * fst✝, h₁ * snd✝) = (fst✝ * g₁, snd✝ * h₁) A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)mul_comm: ∀ {G : Type ?u.33612} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm g₁: G
g₁,A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(fst✝ * g₁, h₁ * snd✝) = (fst✝ * g₁, snd✝ * h₁) A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)mul_comm: ∀ {G : Type ?u.33647} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm h₁: H
h₁A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H

(fst✝ * g₁, snd✝ * h₁) = (fst✝ * g₁, snd✝ * h₁)]
Goals accomplished! 🐙 }

end Prod

namespace MulHom

section Prod

variable (M: ?m.33892
M N: ?m.33895
N) [Mul: Type ?u.33898 → Type ?u.33898
Mul M: Type ?u.33919
M] [Mul: Type ?u.34527 → Type ?u.34527
Mul N: Type ?u.33922
N] [Mul: Type ?u.34530 → Type ?u.34530
Mul P: Type ?u.33889
P]

/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `M`.-/
@[to_additive: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) M
to_additive
      "Given additive magmas `A`, `B`, the natural projection homomorphism
      from `A × B` to `A`"]
def fst: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst : M: Type ?u.33919
M × N: Type ?u.33922
N →ₙ* M: Type ?u.33919
M :=
  ⟨Prod.fst: {α : Type ?u.34030} → {β : Type ?u.34029} → α × β → α
Prod.fst, fun _: ?m.34039
_ _: ?m.34042
_ => rfl: ∀ {α : Sort ?u.34044} {a : α}, a = a
rfl⟩
#align mul_hom.fst MulHom.fst: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
MulHom.fst
#align add_hom.fst AddHom.fst: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) M
AddHom.fst

/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `N`.-/
@[to_additive: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) N
to_additive
      "Given additive magmas `A`, `B`, the natural projection homomorphism
      from `A × B` to `B`"]
def snd: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd : M: Type ?u.34224
M × N: Type ?u.34227
N →ₙ* N: Type ?u.34227
N :=
  ⟨Prod.snd: {α : Type ?u.34335} → {β : Type ?u.34334} → α × β → β
Prod.snd, fun _: ?m.34344
_ _: ?m.34347
_ => rfl: ∀ {α : Sort ?u.34349} {a : α}, a = a
rfl⟩
#align mul_hom.snd MulHom.snd: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
MulHom.snd
#align add_hom.snd AddHom.snd: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) N
AddHom.snd

variable {M: ?m.34533
M N: ?m.34536
N}

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.fst M N) = Prod.fst
to_additive (attr := simp)]
theorem coe_fst: ↑(fst M N) = Prod.fst
coe_fst : ⇑(fst: (M : Type ?u.34571) → (N : Type ?u.34570) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst M: Type ?u.34551
M N: Type ?u.34554
N) = Prod.fst: {α : Type ?u.34764} → {β : Type ?u.34763} → α × β → α
Prod.fst :=
  rfl: ∀ {α : Sort ?u.34819} {a : α}, a = a
rfl
#align mul_hom.coe_fst MulHom.coe_fst: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N], ↑(fst M N) = Prod.fst
MulHom.coe_fst
#align add_hom.coe_fst AddHom.coe_fst: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.fst M N) = Prod.fst
AddHom.coe_fst

@[to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.snd M N) = Prod.snd
to_additive (attr := simp)]
theorem coe_snd: ↑(snd M N) = Prod.snd
coe_snd : ⇑(snd: (M : Type ?u.34942) → (N : Type ?u.34941) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd M: Type ?u.34922
M N: Type ?u.34925
N) = Prod.snd: {α : Type ?u.35135} → {β : Type ?u.35134} → α × β → β
Prod.snd :=
  rfl: ∀ {α : Sort ?u.35190} {a : α}, a = a
rfl
#align mul_hom.coe_snd MulHom.coe_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N], ↑(snd M N) = Prod.snd
MulHom.coe_snd
#align add_hom.coe_snd AddHom.coe_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.snd M N) = Prod.snd
AddHom.coe_snd

/-- Combine two `MonoidHom`s `f : M →ₙ* N`, `g : M →ₙ* P` into
`f.prod g : M →ₙ* (N × P)` given by `(f.prod g) x = (f x, g x)`. -/
@[to_additive prod: {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → AddHom M N → AddHom M P → AddHom M (N × P)
prod
      "Combine two `AddMonoidHom`s `f : AddHom M N`, `g : AddHom M P` into
      `f.prod g : AddHom M (N × P)` given by `(f.prod g) x = (f x, g x)`"]
protected def prod: {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod (f: M →ₙ* N
f : M: Type ?u.35293
M →ₙ* N: Type ?u.35296
N) (g: M →ₙ* P
g : M: Type ?u.35293
M →ₙ* P: Type ?u.35299
P) :
    M: Type ?u.35293
M →ₙ* N: Type ?u.35296
N × P: Type ?u.35299
P where
  toFun := Pi.prod: {I : Type ?u.35402} →
  {f : I → Type ?u.35401} → {g : I → Type ?u.35400} → ((i : I) → f i) → ((i : I) → g i) → (i : I) → f i × g i
Pi.prod f: M →ₙ* N
f g: M →ₙ* P
g
  map_mul' x: ?m.35753
x y: ?m.35756
y := Prod.ext: ∀ {α : Type ?u.35758} {β : Type ?u.35759} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (f: M →ₙ* N
f.map_mul: ∀ {M : Type ?u.35769} {N : Type ?u.35770} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a b : M),
  ↑f (a * b) = ↑f a * ↑f b
map_mul x: ?m.35753
x y: ?m.35756
y) (g: M →ₙ* P
g.map_mul: ∀ {M : Type ?u.35791} {N : Type ?u.35792} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a b : M),
  ↑f (a * b) = ↑f a * ↑f b
map_mul x: ?m.35753
x y: ?m.35756
y)
#align mul_hom.prod MulHom.prod: {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
MulHom.prod
#align add_hom.prod AddHom.prod: {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → AddHom M N → AddHom M P → AddHom M (N × P)
AddHom.prod

@[to_additive coe_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P), ↑(AddHom.prod f g) = Pi.prod ↑f ↑g
coe_prod]
theorem coe_prod: ∀ (f : M →ₙ* N) (g : M →ₙ* P), ↑(MulHom.prod f g) = Pi.prod ↑f ↑g
coe_prod (f: M →ₙ* N
f : M: Type ?u.36210
M →ₙ* N: Type ?u.36213
N) (g: M →ₙ* P
g : M: Type ?u.36210
M →ₙ* P: Type ?u.36216
P) : ⇑(f: M →ₙ* N
f.prod: {M : Type ?u.36261} →
  {N : Type ?u.36260} →
    {P : Type ?u.36259} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod g: M →ₙ* P
g) = Pi.prod: {I : Type ?u.36468} →
  {f : I → Type ?u.36467} → {g : I → Type ?u.36466} → ((i : I) → f i) → ((i : I) → g i) → (i : I) → f i × g i
Pi.prod f: M →ₙ* N
f g: M →ₙ* P
g :=
  rfl: ∀ {α : Sort ?u.36824} {a : α}, a = a
rfl
#align mul_hom.coe_prod MulHom.coe_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), ↑(MulHom.prod f g) = Pi.prod ↑f ↑g
MulHom.coe_prod
#align add_hom.coe_prod AddHom.coe_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P), ↑(AddHom.prod f g) = Pi.prod ↑f ↑g
AddHom.coe_prod

@[to_additive (attr := simp) prod_apply: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P) (x : M), ↑(AddHom.prod f g) x = (↑f x, ↑g x)
prod_apply]
theorem prod_apply: ∀ (f : M →ₙ* N) (g : M →ₙ* P) (x : M), ↑(MulHom.prod f g) x = (↑f x, ↑g x)
prod_apply (f: M →ₙ* N
f : M: Type ?u.36904
M →ₙ* N: Type ?u.36907
N) (g: M →ₙ* P
g : M: Type ?u.36904
M →ₙ* P: Type ?u.36910
P) (x: M
x) : f: M →ₙ* N
f.prod: {M : Type ?u.36958} →
  {N : Type ?u.36957} →
    {P : Type ?u.36956} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod g: M →ₙ* P
g x: ?m.36952
x = (f: M →ₙ* N
f x: ?m.36952
x, g: M →ₙ* P
g x: ?m.36952
x) :=
  rfl: ∀ {α : Sort ?u.37507} {a : α}, a = a
rfl
#align mul_hom.prod_apply MulHom.prod_apply: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P) (x : M), ↑(MulHom.prod f g) x = (↑f x, ↑g x)
MulHom.prod_apply
#align add_hom.prod_apply AddHom.prod_apply: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P) (x : M), ↑(AddHom.prod f g) x = (↑f x, ↑g x)
AddHom.prod_apply

@[to_additive (attr := simp) fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P), AddHom.comp (AddHom.fst N P) (AddHom.prod f g) = f
fst_comp_prod]
theorem fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), comp (fst N P) (MulHom.prod f g) = f
fst_comp_prod (f: M →ₙ* N
f : M: Type ?u.37662
M →ₙ* N: Type ?u.37665
N) (g: M →ₙ* P
g : M: Type ?u.37662
M →ₙ* P: Type ?u.37668
P) : (fst: (M : Type ?u.37712) → (N : Type ?u.37711) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst N: Type ?u.37665
N P: Type ?u.37668
P).comp: {M : Type ?u.37717} →
  {N : Type ?u.37716} →
    {P : Type ?u.37715} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp (f: M →ₙ* N
f.prod: {M : Type ?u.37739} →
  {N : Type ?u.37738} →
    {P : Type ?u.37737} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod g: M →ₙ* P
g) = f: M →ₙ* N
f :=
  ext: ∀ {M : Type ?u.37824} {N : Type ?u.37825} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄,
  (∀ (x : M), ↑f x = ↑g x) → f = g
ext fun _: ?m.37880
_ => rfl: ∀ {α : Sort ?u.37882} {a : α}, a = a
rfl
#align mul_hom.fst_comp_prod MulHom.fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), comp (fst N P) (MulHom.prod f g) = f
MulHom.fst_comp_prod
#align add_hom.fst_comp_prod AddHom.fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P), AddHom.comp (AddHom.fst N P) (AddHom.prod f g) = f
AddHom.fst_comp_prod

@[to_additive (attr := simp) snd_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P), AddHom.comp (AddHom.snd N P) (AddHom.prod f g) = g
snd_comp_prod]
theorem snd_comp_prod: ∀ (f : M →ₙ* N) (g : M →ₙ* P), comp (snd N P) (MulHom.prod f g) = g
snd_comp_prod (f: M →ₙ* N
f : M: Type ?u.38036
M →ₙ* N: Type ?u.38039
N) (g: M →ₙ* P
g : M: Type ?u.38036
M →ₙ* P: Type ?u.38042
P) : (snd: (M : Type ?u.38086) → (N : Type ?u.38085) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd N: Type ?u.38039
N P: Type ?u.38042
P).comp: {M : Type ?u.38091} →
  {N : Type ?u.38090} →
    {P : Type ?u.38089} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp (f: M →ₙ* N
f.prod: {M : Type ?u.38113} →
  {N : Type ?u.38112} →
    {P : Type ?u.38111} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod g: M →ₙ* P
g) = g: M →ₙ* P
g :=
  ext: ∀ {M : Type ?u.38198} {N : Type ?u.38199} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄,
  (∀ (x : M), ↑f x = ↑g x) → f = g
ext fun _: ?m.38254
_ => rfl: ∀ {α : Sort ?u.38256} {a : α}, a = a
rfl
#align mul_hom.snd_comp_prod MulHom.snd_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), comp (snd N P) (MulHom.prod f g) = g
MulHom.snd_comp_prod
#align add_hom.snd_comp_prod AddHom.snd_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N)
  (g : AddHom M P), AddHom.comp (AddHom.snd N P) (AddHom.prod f g) = g
AddHom.snd_comp_prod

@[to_additive (attr := simp) prod_unique: ∀ {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M (N × P)),
  AddHom.prod (AddHom.comp (AddHom.fst N P) f) (AddHom.comp (AddHom.snd N P) f) = f
prod_unique]
theorem prod_unique: ∀ (f : M →ₙ* N × P), MulHom.prod (comp (fst N P) f) (comp (snd N P) f) = f
prod_unique (f: M →ₙ* N × P
f : M: Type ?u.38410
M →ₙ* N: Type ?u.38413
N × P: Type ?u.38416
P) : ((fst: (M : Type ?u.38470) → (N : Type ?u.38469) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst N: Type ?u.38413
N P: Type ?u.38416
P).comp: {M : Type ?u.38483} →
  {N : Type ?u.38482} →
    {P : Type ?u.38481} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp f: M →ₙ* N × P
f).prod: {M : Type ?u.38530} →
  {N : Type ?u.38529} →
    {P : Type ?u.38528} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod ((snd: (M : Type ?u.38550) → (N : Type ?u.38549) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd N: Type ?u.38413
N P: Type ?u.38416
P).comp: {M : Type ?u.38555} →
  {N : Type ?u.38554} →
    {P : Type ?u.38553} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp f: M →ₙ* N × P
f) = f: M →ₙ* N × P
f :=
  ext: ∀ {M : Type ?u.38608} {N : Type ?u.38609} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄,
  (∀ (x : M), ↑f x = ↑g x) → f = g
ext fun x: ?m.38664
x => by
Goals accomplished! 🐙 A: Type ?u.38398

B: Type ?u.38401

G: Type ?u.38404

H: Type ?u.38407

M: Type u_1

N: Type u_3

P: Type u_2

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

f: M →ₙ* N × P

x: M

↑(MulHom.prod (comp (fst N P) f) (comp (snd N P) f)) x = ↑f xsimp only [prod_apply: ∀ {M : Type ?u.38718} {N : Type ?u.38719} {P : Type ?u.38720} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P]
  (f : M →ₙ* N) (g : M →ₙ* P) (x : M), ↑(MulHom.prod f g) x = (↑f x, ↑g x)
prod_apply, coe_fst: ∀ {M : Type ?u.38762} {N : Type ?u.38763} [inst : Mul M] [inst_1 : Mul N], ↑(fst M N) = Prod.fst
coe_fst, coe_snd: ∀ {M : Type ?u.38790} {N : Type ?u.38791} [inst : Mul M] [inst_1 : Mul N], ↑(snd M N) = Prod.snd
coe_snd, comp_apply: ∀ {M : Type ?u.38816} {N : Type ?u.38817} {P : Type ?u.38818} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P]
  (g : N →ₙ* P) (f : M →ₙ* N) (x : M), ↑(comp g f) x = ↑g (↑f x)
comp_apply, Prod.mk.eta: ∀ {α : Type ?u.38858} {β : Type ?u.38859} {p : α × β}, (p.fst, p.snd) = p
Prod.mk.eta]
Goals accomplished! 🐙
#align mul_hom.prod_unique MulHom.prod_unique: ∀ {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N × P),
  MulHom.prod (comp (fst N P) f) (comp (snd N P) f) = f
MulHom.prod_unique
#align add_hom.prod_unique AddHom.prod_unique: ∀ {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M (N × P)),
  AddHom.prod (AddHom.comp (AddHom.fst N P) f) (AddHom.comp (AddHom.snd N P) f) = f
AddHom.prod_unique

end Prod

section Prod_map

variable {M': Type ?u.40314
M' : Type _: Type (?u.39705+1)
Type _} {N': Type ?u.40317
N' : Type _: Type (?u.39708+1)
Type _} [Mul: Type ?u.39711 → Type ?u.39711
Mul M: Type ?u.39696
M] [Mul: Type ?u.40649 → Type ?u.40649
Mul N: Type ?u.39777
N] [Mul: Type ?u.41496 → Type ?u.41496
Mul M': Type ?u.40314
M'] [Mul: Type ?u.40329 → Type ?u.40329
Mul N': Type ?u.40317
N'] [Mul: Type ?u.40332 → Type ?u.40332
Mul P: Type ?u.40311
P] (