[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : Bool → α
⊢ ∏ b : Bool, f b = f true * f false
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ (∏ i : ι, if i ∈ s then f i else 1) = ∏ i in s, f i
[PROOFSTEP]
rw [← prod_filter, filter_mem_eq_inter, univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x : α, f x = f a * f b
[PROOFSTEP]
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx
[GOAL]
case ha
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ¬a ∈ Finset.univ → f a = 1
[PROOFSTEP]
exact fun hc => (hc (Finset.mem_univ _)).elim
[GOAL]
case hb
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ¬b ∈ Finset.univ → f b = 1
[PROOFSTEP]
exact fun hc => (hc (Finset.mem_univ _)).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
⊢ Finset.card (piFinset t) = ∏ a : α, Finset.card (t a)
[PROOFSTEP]
simp [Fintype.piFinset, card_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card (α → β) = card β ^ card α
[PROOFSTEP]
rw [Fintype.card_pi, Finset.prod_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card β ^ Finset.card univ = card β ^ card α
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Vector α n) = Fintype.card α ^ n
[PROOFSTEP]
rw [Fintype.ofEquiv_card]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : CommMonoid β
f : { a // a ∈ univ } → β
x : { x // x ∈ univ }
⊢ f x =
    f
      { val := ↑(Equiv.subtypeUnivEquiv (_ : ∀ (x : α), x ∈ univ)) x,
        property := (_ : ↑(Equiv.subtypeUnivEquiv (_ : ∀ (x : α), x ∈ univ)) x ∈ univ) }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∏ x in pi univ t, f x = ∏ x in Fintype.piFinset t, f fun a x_1 => x a
[PROOFSTEP]
refine
  prod_bij (fun x _ a => x a (mem_univ _)) ?_ (by simp)
    (by simp (config := { contextual := true }) [Function.funext_iff]) fun x hx =>
    ⟨fun a _ => x a, by simp_all⟩
      -- Porting note: old proof was `by simp`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a : (a : α) → a ∈ univ → δ a) (ha : a ∈ pi univ t),
    f a = f fun a_1 x => (fun x x_1 a => x a (_ : a ∈ univ)) a ha a_1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a₁ a₂ : (a : α) → a ∈ univ → δ a) (ha₁ : a₁ ∈ pi univ t) (ha₂ : a₂ ∈ pi univ t),
    (fun x x_1 a => x a (_ : a ∈ univ)) a₁ ha₁ = (fun x x_1 a => x a (_ : a ∈ univ)) a₂ ha₂ → a₁ = a₂
[PROOFSTEP]
simp (config := { contextual := true }) [Function.funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
x : (a : α) → δ a
hx : x ∈ Fintype.piFinset t
⊢ ∃ ha, x = (fun x x_1 a => x a (_ : a ∈ univ)) (fun a x_1 => x a) ha
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a : (a : α) → a ∈ univ → δ a) (ha : a ∈ pi univ t), (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
[PROOFSTEP]
simp only [Fintype.piFinset, mem_map, mem_pi, Function.Embedding.coeFn_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ ∃ a_1, (∀ (a : α) (h : a ∈ univ), a_1 a h ∈ t a) ∧ (fun a => a_1 a (_ : a ∈ univ)) = fun a_2 => a a_2 (_ : a_2 ∈ univ)
[PROOFSTEP]
exact ⟨a, by simpa using ha, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ ∀ (a_1 : α) (h : a_1 ∈ univ), a a_1 h ∈ t a_1
[PROOFSTEP]
simpa using ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ (fun a_1 => a a_1 (_ : a_1 ∈ univ)) = fun a_1 => a a_1 (_ : a_1 ∈ univ)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : CommSemiring β
δ : α → Type u_1
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
⊢ ∏ a : α, ∑ b in t a, f a b = ∑ p in Fintype.piFinset t, ∏ x : α, f x (p x)
[PROOFSTEP]
simp only [Finset.prod_attach_univ, prod_sum, Finset.sum_univ_pi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (i : Fin n), f ↑i = f ↑(↑(equivSubtype.trans (Equiv.subtypeEquivRight (_ : ∀ (a : ℕ), a < n ↔ a ∈ range n))) i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i : { x // x ∈ range n }, f ↑i = ∏ i in range n, f i
[PROOFSTEP]
rw [← attach_eq_univ, prod_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i : Fin n, c i = ∏ i in range n, if h : i < n then c { val := i, isLt := h } else 1
[PROOFSTEP]
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ (x : Fin n), x ∈ univ → c x = if h : ↑x < n then c { val := ↑x, isLt := h } else 1
[PROOFSTEP]
rintro ⟨i, hi⟩ _
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
a✝ : { val := i, isLt := hi } ∈ univ
⊢ c { val := i, isLt := hi } =
    if h : ↑{ val := i, isLt := hi } < n then c { val := ↑{ val := i, isLt := hi }, isLt := h } else 1
[PROOFSTEP]
simp only [hi, dif_pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a in Set.toFinset {x | p x}, f a = ∏ a : Subtype p, f ↑a
[PROOFSTEP]
rw [← Finset.prod_subtype]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ Set.toFinset {x | p x} ↔ p x
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x
[PROOFSTEP]
intro
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
inst✝ : CommMonoid γ
f : α → β
g : α → γ
⊢ ∏ b : β, ∏ a : { a // f a = b }, g ↑a = ∏ a : α, g a
[PROOFSTEP]
rw [← (Equiv.sigmaFiberEquiv f).prod_comp, ← univ_sigma_univ, prod_sigma]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
inst✝ : CommMonoid γ
f : α → β
g : α → γ
⊢ ∏ b : β, ∏ a : { a // f a = b }, g ↑a =
    ∏ a : β, ∏ s : { x // f x = a }, g (↑(Equiv.sigmaFiberEquiv f) { fst := a, snd := s })
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ a : α, dite (p a) (f a) (g a) = (∏ a : { a // p a }, f ↑a (_ : p ↑a)) * ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
[PROOFSTEP]
simp only [prod_dite, attach_eq_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ (∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x)) *
      ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) =
    (∏ a : { a // p a }, f ↑a (_ : p ↑a)) * ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x) = ∏ a : { a // p a }, f ↑a (_ : p ↑a)
[PROOFSTEP]
exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // p x } => f x x.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => p x) univ ↔ p x
[PROOFSTEP]
simp
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) = ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
[PROOFSTEP]
exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // ¬p x } => g x x.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => ¬p x) univ ↔ ¬p x
[PROOFSTEP]
simp
