[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)
[PROOFSTEP]
rw [mk_mul_mk, mul_one]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Mul M
inst✝ : Monoid N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
[PROOFSTEP]
rw [mk_mul_mk, mul_one]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : SemigroupWithZero M
inst✝ : SemigroupWithZero N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : SemigroupWithZero M
inst✝ : SemigroupWithZero N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ ∀ (a : M × N), 1 * a = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ ∀ (a : M × N), a * 1 = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : DivisionMonoid G
inst✝ : DivisionMonoid H
⊢ ∀ (x : G × H), x⁻¹⁻¹ = x
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
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₁)
[PROOFSTEP]
rw [mk_mul_mk, mul_comm g₁, mul_comm h₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
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₁)
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : LeftCancelMonoid M
inst✝ : LeftCancelMonoid N
⊢ ∀ (a : M × N), 1 * a = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : LeftCancelMonoid M
inst✝ : LeftCancelMonoid N
⊢ ∀ (a : M × N), a * 1 = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : RightCancelMonoid M
inst✝ : RightCancelMonoid N
⊢ ∀ (a : M × N), 1 * a = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : RightCancelMonoid M
inst✝ : RightCancelMonoid N
⊢ ∀ (a : M × N), a * 1 = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CancelMonoid M
inst✝ : CancelMonoid N
⊢ ∀ (a b c : M × N), a * b = c * b → a = c
[PROOFSTEP]
simp only [mul_left_inj, imp_self, forall_const]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
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₁)
[PROOFSTEP]
rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
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₁)
[PROOFSTEP]
rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MonoidWithZero M
inst✝ : MonoidWithZero N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MonoidWithZero M
inst✝ : MonoidWithZero N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
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₁)
[PROOFSTEP]
rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
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 x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : CommSemigroup P
f✝ : M →ₙ* P
g✝ : N →ₙ* P
Q : Type u_8
inst✝ : CommSemigroup Q
h : P →ₙ* Q
f : M →ₙ* P
g : N →ₙ* P
x : M × N
⊢ ↑(comp h (coprod f g)) x = ↑(coprod (comp h f) (comp h g)) x
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M →* N × P
x : M
⊢ ↑(MonoidHom.prod (comp (fst N P) f) (comp (snd N P) f)) x = ↑f x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : M
⊢ ↑(comp (coprod f g) (inl M N)) x = ↑f x
[PROOFSTEP]
simp [coprod_apply]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : N
⊢ ↑(comp (coprod f g) (inr M N)) x = ↑g x
[PROOFSTEP]
simp [coprod_apply]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f✝ : M →* P
g : N →* P
f : M × N →* P
x : M × N
⊢ ↑(coprod (comp f (inl M N)) (comp f (inr M N))) x = ↑f x
[PROOFSTEP]
simp [coprod_apply, inl_apply, inr_apply, ← map_mul]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
f✝ : M →* P
g✝ : N →* P
Q : Type u_8
inst✝ : CommMonoid Q
h : P →* Q
f : M →* P
g : N →* P
x : M × N
⊢ ↑(comp h (coprod f g)) x = ↑(coprod (comp h f) (comp h g)) x
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.fst, ↑u.snd) * (↑u.fst⁻¹, ↑u.snd⁻¹) = 1
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.fst⁻¹, ↑u.snd⁻¹) * (↑u.fst, ↑u.snd) = 1
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
u : (M × N)ˣ
⊢ (fun u =>
        { val := (↑u.fst, ↑u.snd), inv := (↑u.fst⁻¹, ↑u.snd⁻¹),
          val_inv := (_ : (↑u.fst * ↑u.fst⁻¹, ↑u.snd * ↑u.snd⁻¹) = 1),
          inv_val := (_ : (↑u.fst⁻¹ * ↑u.fst, ↑u.snd⁻¹ * ↑u.snd) = 1) })
      (↑(MonoidHom.prod (Units.map (MonoidHom.fst M N)) (Units.map (MonoidHom.snd M N))) u) =
    u
[PROOFSTEP]
simp only [MonoidHom.prod_apply, Units.coe_map, MonoidHom.coe_fst, MonoidHom.coe_snd, Prod.mk.eta, Units.coe_map_inv,
  Units.mk_val]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ ↑(MonoidHom.prod (Units.map (MonoidHom.fst M N)) (Units.map (MonoidHom.snd M N)))
      ((fun u =>
          { val := (↑u.fst, ↑u.snd), inv := (↑u.fst⁻¹, ↑u.snd⁻¹),
            val_inv := (_ : (↑u.fst * ↑u.fst⁻¹, ↑u.snd * ↑u.snd⁻¹) = 1),
            inv_val := (_ : (↑u.fst⁻¹ * ↑u.fst, ↑u.snd⁻¹ * ↑u.snd) = 1) })
        (u₁, u₂)) =
    (u₁, u₂)
[PROOFSTEP]
simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv, MonoidHom.coe_snd, MonoidHom.prod_apply, Prod.mk.injEq]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ ↑(MonoidHom.mk'
            (fun u =>
              { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
            (_ :
              ∀ (a b : (M × N)ˣ),
                (fun u =>
                      { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                        inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
                    (a * b) =
                  (fun u =>
                        { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                          inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
                      a *
                    (fun u =>
                        { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                          inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
                      b))
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹),
          val_inv := (_ : (↑(u₁, u₂).fst * ↑(u₁, u₂).fst⁻¹, ↑(u₁, u₂).snd * ↑(u₁, u₂).snd⁻¹) = 1),
          inv_val := (_ : (↑(u₁, u₂).fst⁻¹ * ↑(u₁, u₂).fst, ↑(u₁, u₂).snd⁻¹ * ↑(u₁, u₂).snd) = 1) } =
      u₁ ∧
    ↑(MonoidHom.mk'
            (fun u =>
              { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
            (_ :
              ∀ (a b : (M × N)ˣ),
                (fun u =>
                      { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                        inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
                    (a * b) =
                  (fun u =>
                        { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                          inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
                      a *
                    (fun u =>
                        { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                          inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
                      b))
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹),
          val_inv := (_ : (↑(u₁, u₂).fst * ↑(u₁, u₂).fst⁻¹, ↑(u₁, u₂).snd * ↑(u₁, u₂).snd⁻¹) = 1),
          inv_val := (_ : (↑(u₁, u₂).fst⁻¹ * ↑(u₁, u₂).fst, ↑(u₁, u₂).snd⁻¹ * ↑(u₁, u₂).snd) = 1) } =
      u₂
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
α : Type u_8
inst✝ : Monoid α
⊢ (fun x => (↑x, op ↑x⁻¹)) 1 = 1
[PROOFSTEP]
simp only [inv_one, eq_self_iff_true, Units.val_one, op_one, Prod.mk_eq_one, and_self_iff]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
α : Type u_8
inst✝ : Monoid α
x y : αˣ
⊢ OneHom.toFun { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := (_ : (1, op ↑1⁻¹) = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := (_ : (1, op ↑1⁻¹) = 1) } x *
      OneHom.toFun { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := (_ : (1, op ↑1⁻¹) = 1) } y
[PROOFSTEP]
simp only [mul_inv_rev, op_mul, Units.val_mul, Prod.mk_mul_mk]
