/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.int.cast.prod
! leanprover-community/mathlib commit ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Cast.Lemmas
import Mathlib.Data.Nat.Cast.Prod

/-!
# The product of two `AddGroupWithOne`s.
-/


namespace Prod

variable {
α: Type ?u.2
α 
β: Type ?u.5
β : 
Type _: Type (?u.4076+1)
Type _} [
AddGroupWithOne: Type ?u.20 → Type ?u.20
AddGroupWithOne 
α: Type ?u.14
α] [
AddGroupWithOne: Type ?u.4085 → Type ?u.4085
AddGroupWithOne 
β: Type ?u.5
β]

instance: {α : Type u_1} → {β : Type u_2} → [inst : AddGroupWithOne α] → [inst : AddGroupWithOne β] → AddGroupWithOne (α × β)
instance : 
AddGroupWithOne: Type ?u.26 → Type ?u.26
AddGroupWithOne (
α: Type ?u.14
α × 
β: Type ?u.17
β) :=
  { 
Prod.instAddMonoidWithOneProd: {α : Type ?u.33} →
  {β : Type ?u.32} → [inst : AddMonoidWithOne α] → [inst : AddMonoidWithOne β] → AddMonoidWithOne (α × β)
Prod.instAddMonoidWithOneProd, 
Prod.instAddGroupSum: {G : Type ?u.96} → {H : Type ?u.95} → [inst : AddGroup G] → [inst : AddGroup H] → AddGroup (G × H)
Prod.instAddGroupSum with
    intCast := fun 
n: ?m.163
n => (
n: ?m.163
n, 
n: ?m.163
n)
    intCast_ofNat := fun 
_: ?m.554
_ => by
Goals accomplished! 🐙 
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

IntCast.intCast ↑x✝ = ↑x✝simp
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

(↑x✝, ↑x✝) = ↑x✝;
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

(↑x✝, ↑x✝) = ↑x✝ 
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

IntCast.intCast ↑x✝ = ↑x✝rfl
Goals accomplished! 🐙
    intCast_negSucc := fun 
_: ?m.561
_ => by
Goals accomplished! 🐙 
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)simp
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

(-1 + -↑x✝, -1 + -↑x✝) = -1 + -↑x✝;
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

(-1 + -↑x✝, -1 + -↑x✝) = -1 + -↑x✝ 
α: Type ?u.14

β: Type ?u.17

inst✝¹: AddGroupWithOne α

inst✝: AddGroupWithOne β

src✝¹:= instAddMonoidWithOneProd: AddMonoidWithOne (α × β)

src✝:= instAddGroupSum: AddGroup (α × β)

x✝: ℕ

IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)rfl
Goals accomplished! 🐙 }

@[simp]
theorem 
fst_intCast: ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroupWithOne α] [inst_1 : AddGroupWithOne β] (n : ℤ), (↑n).fst = ↑n
fst_intCast (
n: ℤ
n : 
ℤ: Type
ℤ) : (
n: ℤ
n : 
α: Type ?u.4076
α × 
β: Type ?u.4079
β).
fst: {α : Type ?u.4231} → {β : Type ?u.4230} → α × β → α
fst = 
n: ℤ
n :=
  
rfl: ∀ {α : Sort ?u.4433} {a : α}, a = a
rfl
#align prod.fst_int_cast 
Prod.fst_intCast: ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroupWithOne α] [inst_1 : AddGroupWithOne β] (n : ℤ), (↑n).fst = ↑n
Prod.fst_intCast

@[simp]
theorem 
snd_intCast: ∀ {α : Type u_2} {β : Type u_1} [inst : AddGroupWithOne α] [inst_1 : AddGroupWithOne β] (n : ℤ), (↑n).snd = ↑n
snd_intCast (
n: ℤ
n : 
ℤ: Type
ℤ) : (
n: ℤ
n : 
α: Type ?u.4460
α × 
β: Type ?u.4463
β).
snd: {α : Type ?u.4615} → {β : Type ?u.4614} → α × β → β
snd = 
n: ℤ
n :=
  
rfl: ∀ {α : Sort ?u.4817} {a : α}, a = a
rfl
#align prod.snd_int_cast 
Prod.snd_intCast: ∀ {α : Type u_2} {β : Type u_1} [inst : AddGroupWithOne α] [inst_1 : AddGroupWithOne β] (n : ℤ), (↑n).snd = ↑n
Prod.snd_intCast

end Prod