/-
Copyright (c) 2019 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro

! This file was ported from Lean 3 source module data.rat.big_operators
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Rat.Cast
import Mathlib.Algebra.BigOperators.Basic

/-! # Casting lemmas for rational numbers involving sums and products
-/

open BigOperators

variable {ι: Type ?u.2119
ι α: Type ?u.89
α : Type _: Type (?u.5+1)
Type _}

namespace Rat

section WithDivRing

variable [DivisionRing: Type ?u.2125 → Type ?u.2125
DivisionRing α: Type ?u.89
α] [CharZero: (R : Type ?u.1124) → [inst : AddMonoidWithOne R] → Prop
CharZero α: Type ?u.11
α]

@[simp, norm_cast]
theorem cast_list_sum: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ),
  ↑(List.sum s) = List.sum (List.map Rat.cast s)
cast_list_sum (s: List ℚ
s : List: Type ?u.164 → Type ?u.164
List ℚ: Type
ℚ) : (↑s: List ℚ
s.sum: {α : Type ?u.169} → [inst : Add α] → [inst : Zero α] → List α → α
sum : α: Type ?u.89
α) = (s: List ℚ
s.map: {α : Type ?u.275} → {β : Type ?u.274} → (α → β) → List α → List β
map (↑): ℚ → α
(↑)).sum: {α : Type ?u.283} → [inst : Add α] → [inst : Zero α] → List α → α
sum :=
  map_list_sum: ∀ {M : Type ?u.741} {N : Type ?u.742} [inst : AddMonoid M] [inst_1 : AddMonoid N] {F : Type ?u.740}
  [inst_2 : AddMonoidHomClass F M N] (f : F) (l : List M), ↑f (List.sum l) = List.sum (List.map (↑f) l)
map_list_sum (Rat.castHom: (α : Type ?u.749) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom α: Type ?u.89
α) _: List ?m.743
_
#align rat.cast_list_sum Rat.cast_list_sum: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ),
  ↑(List.sum s) = List.sum (List.map Rat.cast s)
Rat.cast_list_sum

@[simp, norm_cast]
theorem cast_multiset_sum: ∀ (s : Multiset ℚ), ↑(Multiset.sum s) = Multiset.sum (Multiset.map Rat.cast s)
cast_multiset_sum (s: Multiset ℚ
s : Multiset: Type ?u.1193 → Type ?u.1193
Multiset ℚ: Type
ℚ) : (↑s: Multiset ℚ
s.sum: {α : Type ?u.1198} → [inst : AddCommMonoid α] → Multiset α → α
sum : α: Type ?u.1118
α) = (s: Multiset ℚ
s.map: {α : Type ?u.1269} → {β : Type ?u.1268} → (α → β) → Multiset α → Multiset β
map (↑): ℚ → α
(↑)).sum: {α : Type ?u.1277} → [inst : AddCommMonoid α] → Multiset α → α
sum :=
  map_multiset_sum: ∀ {α : Type ?u.1597} {β : Type ?u.1598} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {F : Type ?u.1599}
  [inst_2 : AddMonoidHomClass F α β] (f : F) (s : Multiset α), ↑f (Multiset.sum s) = Multiset.sum (Multiset.map (↑f) s)
map_multiset_sum (Rat.castHom: (α : Type ?u.1606) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom α: Type ?u.1118
α) _: Multiset ?m.1600
_
#align rat.cast_multiset_sum Rat.cast_multiset_sum: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : Multiset ℚ),
  ↑(Multiset.sum s) = Multiset.sum (Multiset.map Rat.cast s)
Rat.cast_multiset_sum

@[simp, norm_cast]
theorem cast_sum: ∀ (s : Finset ι) (f : ι → ℚ), ↑(∑ i in s, f i) = ∑ i in s, ↑(f i)
cast_sum (s: Finset ι
s : Finset: Type ?u.2197 → Type ?u.2197
Finset ι: Type ?u.2119
ι) (f: ι → ℚ
f : ι: Type ?u.2119
ι → ℚ: Type
ℚ) : (∑ i: ?m.2213
i in s: Finset ι
s, f: ι → ℚ
f i: ?m.2213
i) = ∑ i: ?m.2234
i in s: Finset ι
s, (f: ι → ℚ
f i: ?m.2234
i : α: Type ?u.2122
α) :=
  (map_sum: ∀ {β : Type ?u.10556} {α : Type ?u.10555} {γ : Type ?u.10554} [inst : AddCommMonoid β] [inst_1 : AddCommMonoid γ]
  {G : Type ?u.10557} [inst_2 : AddMonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α),
  ↑g (∑ x in s, f x) = ∑ x in s, ↑g (f x)
map_sum (Rat.castHom: (α : Type ?u.10565) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom α: Type ?u.2122
α) _: ?m.10559 → ?m.10558
_ s: Finset ι
s)
#align rat.cast_sum Rat.cast_sum: ∀ {ι : Type u_1} {α : Type u_2} [inst : DivisionRing α] [inst_1 : CharZero α] (s : Finset ι) (f : ι → ℚ),
  ↑(∑ i in s, f i) = ∑ i in s, ↑(f i)
Rat.cast_sum

@[simp, norm_cast]
theorem cast_list_prod: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ),
  ↑(List.prod s) = List.prod (List.map Rat.cast s)
cast_list_prod (s: List ℚ
s : List: Type ?u.11175 → Type ?u.11175
List ℚ: Type
ℚ) : (↑s: List ℚ
s.prod: {α : Type ?u.11180} → [inst : Mul α] → [inst : One α] → List α → α
prod : α: Type ?u.11100
α) = (s: List ℚ
s.map: {α : Type ?u.11279} → {β : Type ?u.11278} → (α → β) → List α → List β
map (↑): ℚ → α
(↑)).prod: {α : Type ?u.11287} → [inst : Mul α] → [inst : One α] → List α → α
prod :=
  map_list_prod: ∀ {M : Type ?u.11659} {N : Type ?u.11660} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.11658}
  [inst_2 : MonoidHomClass F M N] (f : F) (l : List M), ↑f (List.prod l) = List.prod (List.map (↑f) l)
map_list_prod (Rat.castHom: (α : Type ?u.11667) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom α: Type ?u.11100
α) _: List ?m.11661
_
#align rat.cast_list_prod Rat.cast_list_prod: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ),
  ↑(List.prod s) = List.prod (List.map Rat.cast s)
Rat.cast_list_prod

end WithDivRing

section Field

variable [Field: Type ?u.12998 → Type ?u.12998
Field α: Type ?u.12141
α] [CharZero: (R : Type ?u.12147) → [inst : AddMonoidWithOne R] → Prop
CharZero α: Type ?u.12141
α]

@[simp, norm_cast]
theorem cast_multiset_prod: ∀ (s : Multiset ℚ), ↑(Multiset.prod s) = Multiset.prod (Multiset.map Rat.cast s)
cast_multiset_prod (s: Multiset ℚ
s : Multiset: Type ?u.12304 → Type ?u.12304
Multiset ℚ: Type
ℚ) : (↑s: Multiset ℚ
s.prod: {α : Type ?u.12309} → [inst : CommMonoid α] → Multiset α → α
prod : α: Type ?u.12224
α) = (s: Multiset ℚ
s.map: {α : Type ?u.12375} → {β : Type ?u.12374} → (α → β) → Multiset α → Multiset β
map (↑): ℚ → α
(↑)).prod: {α : Type ?u.12383} → [inst : CommMonoid α] → Multiset α → α
prod :=
  map_multiset_prod: ∀ {α : Type ?u.12575} {β : Type ?u.12576} [inst : CommMonoid α] [inst_1 : CommMonoid β] {F : Type ?u.12577}
  [inst_2 : MonoidHomClass F α β] (f : F) (s : Multiset α), ↑f (Multiset.prod s) = Multiset.prod (Multiset.map (↑f) s)
map_multiset_prod (Rat.castHom: (α : Type ?u.12584) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom α: Type ?u.12224
α) _: Multiset ?m.12578
_
#align rat.cast_multiset_prod Rat.cast_multiset_prod: ∀ {α : Type u_1} [inst : Field α] [inst_1 : CharZero α] (s : Multiset ℚ),
  ↑(Multiset.prod s) = Multiset.prod (Multiset.map Rat.cast s)
Rat.cast_multiset_prod

@[simp, norm_cast]
theorem cast_prod: ∀ (s : Finset ι) (f : ι → ℚ), ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
cast_prod (s: Finset ι
s : Finset: Type ?u.13075 → Type ?u.13075
Finset ι: Type ?u.12992
ι) (f: ι → ℚ
f : ι: Type ?u.12992
ι → ℚ: Type
ℚ) : (∏ i: ?m.13091
i in s: Finset ι
s, f: ι → ℚ
f i: ?m.13091
i) = ∏ i: ?m.13114
i in s: Finset ι
s, (f: ι → ℚ
f i: ?m.13114
i : α: Type ?u.12995
α) :=
  map_prod: ∀ {β : Type ?u.21298} {α : Type ?u.21297} {γ : Type ?u.21296} [inst : CommMonoid β] [inst_1 : CommMonoid γ]
  {G : Type ?u.21299} [inst_2 : MonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α),
  ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
map_prod (Rat.castHom: (α : Type ?u.21307) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom α: Type ?u.12995
α) _: ?m.21301 → ?m.21300
_ _: Finset ?m.21301
_
#align rat.cast_prod Rat.cast_prod: ∀ {ι : Type u_1} {α : Type u_2} [inst : Field α] [inst_1 : CharZero α] (s : Finset ι) (f : ι → ℚ),
  ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
Rat.cast_prod

end Field

end Rat