[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
x y z : α
⊢ (fun x x_1 => x * x_1) x ((fun x x_1 => x * x_1) y z) = (fun x x_1 => x * x_1) y ((fun x x_1 => x * x_1) x z)
[PROOFSTEP]
simp [mul_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
x y z : α
⊢ (fun x x_1 => x * x_1) x ((fun x x_1 => x * x_1) y z) = (fun x x_1 => x * x_1) y ((fun x x_1 => x * x_1) x z)
[PROOFSTEP]
simp [mul_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
x y z : α
⊢ (fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) x y) z = (fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) x z) y
[PROOFSTEP]
simp [mul_right_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
⊢ foldl (fun x y => y * x) (_ : ∀ (_x _y _z : α), _z * (_y * _x) = _y * (_z * _x)) 1 s =
    foldl (fun x x_1 => x * x_1) (_ : ∀ (x y z : α), x * y * z = x * z * y) 1 s
[PROOFSTEP]
simp [mul_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
⊢ List.prod (toList s) = prod s
[PROOFSTEP]
conv_rhs => rw [← coe_toList s]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
| prod s
[PROOFSTEP]
rw [← coe_toList s]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
| prod s
[PROOFSTEP]
rw [← coe_toList s]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
| prod s
[PROOFSTEP]
rw [← coe_toList s]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
⊢ List.prod (toList s) = prod ↑(toList s)
[PROOFSTEP]
rw [coe_prod]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
h : a ∈ s
⊢ a * prod (erase s a) = prod s
[PROOFSTEP]
rw [← s.coe_toList, coe_erase, coe_prod, coe_prod, List.prod_erase (mem_toList.2 h)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * prod (map f (erase m a)) = prod (map f m)
[PROOFSTEP]
rw [← m.coe_toList, coe_erase, coe_map, coe_map, coe_prod, coe_prod, List.prod_map_erase f (mem_toList.2 h)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
a : α
⊢ prod {a} = a
[PROOFSTEP]
simp only [mul_one, prod_cons, ← cons_zero, eq_self_iff_true, prod_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
a b : α
⊢ prod {a, b} = a * b
[PROOFSTEP]
rw [insert_eq_cons, prod_cons, prod_singleton]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t✝ : Multiset α
a : α
m : Multiset ι
f g : ι → α
s t : Multiset α
l₁ l₂ : List α
⊢ prod (Quotient.mk (List.isSetoid α) l₁ + Quotient.mk (List.isSetoid α) l₂) =
    prod (Quotient.mk (List.isSetoid α) l₁) * prod (Quotient.mk (List.isSetoid α) l₂)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f g : ι → α
m : Multiset α
⊢ prod (0 • m) = prod m ^ 0
[PROOFSTEP]
rw [zero_nsmul, pow_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f g : ι → α
m : Multiset α
⊢ prod 0 = 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f g : ι → α
m : Multiset α
n : ℕ
⊢ prod ((n + 1) • m) = prod m ^ (n + 1)
[PROOFSTEP]
rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
n : ℕ
a : α
⊢ prod (replicate n a) = a ^ n
[PROOFSTEP]
simp [replicate, List.prod_replicate]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq ι
i : ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
⊢ prod (map f m) = f i ^ count i m
[PROOFSTEP]
induction' m using Quotient.inductionOn with l
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq ι
i : ι
hf✝ : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
l : List ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ Quotient.mk (List.isSetoid ι) l → f i' = 1
⊢ prod (map f (Quotient.mk (List.isSetoid ι) l)) = f i ^ count i (Quotient.mk (List.isSetoid ι) l)
[PROOFSTEP]
simp [List.prod_map_eq_pow_single i f hf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
a : α
h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1
⊢ prod s = a ^ count a s
[PROOFSTEP]
induction' s using Quotient.inductionOn with l
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
a : α
h✝ : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1
l : List α
h : ∀ (a' : α), a' ≠ a → a' ∈ Quotient.mk (List.isSetoid α) l → a' = 1
⊢ prod (Quotient.mk (List.isSetoid α) l) = a ^ count a (Quotient.mk (List.isSetoid α) l)
[PROOFSTEP]
simp [List.prod_eq_pow_single a h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
a : α
⊢ a ^ count a s = prod (filter (Eq a) s)
[PROOFSTEP]
rw [filter_eq, prod_replicate]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g : ι → α
inst✝¹ : CommMonoid β
s : Multiset α
F : Type u_5
inst✝ : MonoidHomClass F α β
f : F
l : List α
⊢ prod (map (↑f) (Quotient.mk (List.isSetoid α) l)) = ↑f (prod (Quotient.mk (List.isSetoid α) l))
[PROOFSTEP]
simp only [l.prod_hom f, quot_mk_to_coe, coe_map, coe_prod]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g✝ : ι → α
inst✝¹ : CommMonoid β
s : Multiset ι
F : Type u_5
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ prod (map (fun i => ↑f (g i)) s) = ↑f (prod (map g s))
[PROOFSTEP]
convert (s.map g).prod_hom f
[GOAL]
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g✝ : ι → α
inst✝¹ : CommMonoid β
s : Multiset ι
F : Type u_5
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ map (fun i => ↑f (g i)) s = map (↑f) (map g s)
[PROOFSTEP]
exact (map_map _ _ _).symm
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g : ι → α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
s : Multiset ι
f : α → β → γ
hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → α
f₂ : ι → β
l : List ι
⊢ prod (map (fun i => f (f₁ i) (f₂ i)) (Quotient.mk (List.isSetoid ι) l)) =
    f (prod (map f₁ (Quotient.mk (List.isSetoid ι) l))) (prod (map f₂ (Quotient.mk (List.isSetoid ι) l)))
[PROOFSTEP]
simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, coe_map, coe_prod]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g✝ : ι → α
inst✝ : CommMonoid β
s : Multiset ι
r : α → β → Prop
f : ι → α
g : ι → β
h₁ : r 1 1
h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)
l : List ι
⊢ r (prod (map f (Quotient.mk (List.isSetoid ι) l))) (prod (map g (Quotient.mk (List.isSetoid ι) l)))
[PROOFSTEP]
simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, coe_map, coe_prod]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
⊢ prod (map (fun x => 1) m) = 1
[PROOFSTEP]
rw [map_const', prod_replicate, one_pow]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
inst✝ : HasDistribNeg α
s : Multiset α
⊢ ∀ (a : List α),
    prod (map Neg.neg (Quotient.mk (List.isSetoid α) a)) =
      (-1) ^ ↑card (Quotient.mk (List.isSetoid α) a) * prod (Quotient.mk (List.isSetoid α) a)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f✝ g : ι → α
m : Multiset β
n : Multiset γ
f : β → γ → α
⊢ prod (map (fun a => prod (map (fun b => f a b) n)) 0) = prod (map (fun b => prod (map (fun a => f a b) 0)) n)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a✝ : α
m✝¹ : Multiset ι
f✝ g : ι → α
m✝ : Multiset β
n : Multiset γ
f : β → γ → α
a : β
m : Multiset β
ih : prod (map (fun a => prod (map (fun b => f a b) n)) m) = prod (map (fun b => prod (map (fun a => f a b) m)) n)
⊢ prod (map (fun a => prod (map (fun b => f a b) n)) (a ::ₘ m)) =
    prod (map (fun b => prod (map (fun a => f a b) (a ::ₘ m))) n)
[PROOFSTEP]
simp [ih]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
p : α → Prop
s : Multiset α
p_mul : ∀ (a b : α), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : α), a ∈ s → p a
⊢ p (prod s)
[PROOFSTEP]
rw [prod_eq_foldr]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
p : α → Prop
s : Multiset α
p_mul : ∀ (a b : α), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : α), a ∈ s → p a
⊢ p (foldr (fun x x_1 => x * x_1) (_ : ∀ (x y z : α), x * (y * z) = y * (x * z)) 1 s)
[PROOFSTEP]
exact foldr_induction (· * ·) (fun x y z => by simp [mul_left_comm]) 1 p s p_mul p_one p_s
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
p : α → Prop
s : Multiset α
p_mul : ∀ (a b : α), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : α), a ∈ s → p a
x y z : α
⊢ (fun x x_1 => x * x_1) x ((fun x x_1 => x * x_1) y z) = (fun x x_1 => x * x_1) y ((fun x x_1 => x * x_1) x z)
[PROOFSTEP]
simp [mul_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs : s ≠ ∅
p_s : ∀ (a : α), a ∈ s → p a
⊢ p (prod s)
[PROOFSTEP]
induction' s using Multiset.induction_on with a s hsa
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs✝ : s ≠ ∅
p_s✝ : ∀ (a : α), a ∈ s → p a
hs : 0 ≠ ∅
p_s : ∀ (a : α), a ∈ 0 → p a
⊢ p (prod 0)
[PROOFSTEP]
simp at hs
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs✝ : s✝ ≠ ∅
p_s✝ : ∀ (a : α), a ∈ s✝ → p a
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → p (prod s)
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ p (prod (a ::ₘ s))
[PROOFSTEP]
rw [prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs✝ : s✝ ≠ ∅
p_s✝ : ∀ (a : α), a ∈ s✝ → p a
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → p (prod s)
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a * prod s)
[PROOFSTEP]
by_cases hs_empty : s = ∅
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs✝ : s✝ ≠ ∅
p_s✝ : ∀ (a : α), a ∈ s✝ → p a
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → p (prod s)
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ p (a * prod s)
[PROOFSTEP]
simp [hs_empty, p_s a]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs✝ : s✝ ≠ ∅
p_s✝ : ∀ (a : α), a ∈ s✝ → p a
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → p (prod s)
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ p (a * prod s)
[PROOFSTEP]
have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s✝ t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs✝ : s✝ ≠ ∅
p_s✝ : ∀ (a : α), a ∈ s✝ → p a
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → p (prod s)
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
⊢ p (a * prod s)
[PROOFSTEP]
exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
h : s ≤ t
⊢ prod s ∣ prod t
[PROOFSTEP]
obtain ⟨z, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
s : Multiset α
a : α
m : Multiset ι
f g : ι → α
z : Multiset α
h : s ≤ s + z
⊢ prod s ∣ prod (s + z)
[PROOFSTEP]
simp only [prod_add, dvd_mul_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ prod (map g1 S) ∣ prod (map g2 S)
[PROOFSTEP]
apply Multiset.induction_on' S
[GOAL]
case h₁
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ prod (map g1 0) ∣ prod (map g2 0)
[PROOFSTEP]
simp
[GOAL]
case h₂
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
⊢ ∀ {a : α} {s : Multiset α},
    a ∈ S → s ⊆ S → prod (map g1 s) ∣ prod (map g2 s) → prod (map g1 (insert a s)) ∣ prod (map g2 (insert a s))
[PROOFSTEP]
intro a T haS _ IH
[GOAL]
case h₂
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a
a : α
T : Multiset α
haS : a ∈ S
a✝ : T ⊆ S
IH : prod (map g1 T) ∣ prod (map g2 T)
⊢ prod (map g1 (insert a T)) ∣ prod (map g2 (insert a T))
[PROOFSTEP]
simp [mul_dvd_mul (h a haS) IH]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
⊢ prod s = 0
[PROOFSTEP]
rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
s' : Multiset α
hs' : s = 0 ::ₘ s'
⊢ prod s = 0
[PROOFSTEP]
simp [hs', Multiset.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ prod (Quotient.mk (List.isSetoid α) l) = 0 ↔ 0 ∈ Quotient.mk (List.isSetoid α) l
[PROOFSTEP]
rw [quot_mk_to_coe, coe_prod]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ List.prod l = 0 ↔ 0 ∈ ↑l
[PROOFSTEP]
exact List.prod_eq_zero_iff
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionCommMonoid α
m : Multiset ι
f g : ι → α
⊢ prod (map (fun i => (f i)⁻¹) m) = (prod (map f m))⁻¹
[PROOFSTEP]
simp_rw [← (m.map f).prod_map_inv', map_map, Function.comp_apply]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionCommMonoid α
m : Multiset ι
f g : ι → α
n : ℤ
⊢ prod (map (fun i => f i ^ n) m) = prod (map f m) ^ n
[PROOFSTEP]
convert (m.map f).prod_hom (zpowGroupHom n : α →* α)
[GOAL]
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionCommMonoid α
m : Multiset ι
f g : ι → α
n : ℤ
⊢ map (fun i => f i ^ n) m = map (↑(zpowGroupHom n)) (map f m)
[PROOFSTEP]
simp only [map_map, Function.comp_apply, zpowGroupHom_apply]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : NonUnitalNonAssocSemiring α
a : α
s : Multiset ι
f : ι → α
⊢ sum (map (fun i => a * f i) 0) = a * sum (map f 0)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : NonUnitalNonAssocSemiring α
a : α
s✝ : Multiset ι
f : ι → α
i : ι
s : Multiset ι
ih : sum (map (fun i => a * f i) s) = a * sum (map f s)
⊢ sum (map (fun i => a * f i) (i ::ₘ s)) = a * sum (map f (i ::ₘ s))
[PROOFSTEP]
simp [ih, mul_add]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : NonUnitalNonAssocSemiring α
a : α
s : Multiset ι
f : ι → α
⊢ sum (map (fun i => f i * a) 0) = sum (map f 0) * a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : NonUnitalNonAssocSemiring α
a✝ : α
s✝ : Multiset ι
f : ι → α
a : ι
s : Multiset ι
ih : sum (map (fun i => f i * a✝) s) = sum (map f s) * a✝
⊢ sum (map (fun i => f i * a✝) (a ::ₘ s)) = sum (map f (a ::ₘ s)) * a✝
[PROOFSTEP]
simp [ih, add_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Semiring α
a : α
s✝ : Multiset α
x : α
s : Multiset α
ih : (∀ (x : α), x ∈ s → a ∣ x) → a ∣ sum s
h : ∀ (x_1 : α), x_1 ∈ x ::ₘ s → a ∣ x_1
⊢ a ∣ sum (x ::ₘ s)
[PROOFSTEP]
rw [sum_cons]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Semiring α
a : α
s✝ : Multiset α
x : α
s : Multiset α
ih : (∀ (x : α), x ∈ s → a ∣ x) → a ∣ sum s
h : ∀ (x_1 : α), x_1 ∈ x ::ₘ s → a ∣ x_1
⊢ a ∣ x + sum s
[PROOFSTEP]
exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy => h _ <| mem_cons.2 <| Or.inr hy)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
l : List α
hl : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → 1 ≤ x
⊢ 1 ≤ prod (Quotient.mk (List.isSetoid α) l)
[PROOFSTEP]
simpa using List.one_le_prod_of_one_le hl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
l : List α
hl : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → 1 ≤ x
x : α
hx : x ∈ Quotient.mk (List.isSetoid α) l
⊢ x ≤ prod (Quotient.mk (List.isSetoid α) l)
[PROOFSTEP]
simpa using List.single_le_prod hl x hx
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s✝ t : Multiset α
a : α
s : Multiset α
n : α
h : ∀ (x : α), x ∈ s → x ≤ n
⊢ prod s ≤ n ^ ↑card s
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a n : α
a✝ : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ n
⊢ prod (Quotient.mk (List.isSetoid α) a✝) ≤ n ^ ↑card (Quotient.mk (List.isSetoid α) a✝)
[PROOFSTEP]
simpa using List.prod_le_pow_card _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ ∀ (a : List α),
    (∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a → 1 ≤ x) →
      prod (Quotient.mk (List.isSetoid α) a) = 1 → ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a → x = 1
[PROOFSTEP]
simp only [quot_mk_to_coe, coe_prod, mem_coe]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ ∀ (a : List α), (∀ (x : α), x ∈ a → 1 ≤ x) → List.prod a = 1 → ∀ (x : α), x ∈ a → x = 1
[PROOFSTEP]
exact fun l => List.all_one_of_le_one_le_of_prod_eq_one
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
h : Rel (fun x x_1 => x ≤ x_1) s t
⊢ prod s ≤ prod t
[PROOFSTEP]
induction' h with _ _ _ _ rh _ rt
[GOAL]
case zero
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ prod 0 ≤ prod 0
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x x_1 => x ≤ x_1) as✝ bs✝
rt : prod as✝ ≤ prod bs✝
⊢ prod (a✝¹ ::ₘ as✝) ≤ prod (b✝ ::ₘ bs✝)
[PROOFSTEP]
rw [prod_cons, prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x x_1 => x ≤ x_1) as✝ bs✝
rt : prod as✝ ≤ prod bs✝
⊢ a✝¹ * prod as✝ ≤ b✝ * prod bs✝
[PROOFSTEP]
exact mul_le_mul' rh rt
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ ↑card s ≤ prod s
[PROOFSTEP]
rw [← Multiset.prod_replicate, ← Multiset.map_const]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ prod (map (Function.const α a) s) ≤ prod s
[PROOFSTEP]
exact prod_map_le_prod _ h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
h : ∀ (a : α), a ∈ m → 0 ≤ a
⊢ 0 ≤ prod m
[PROOFSTEP]
revert h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ (∀ (a : α), a ∈ m → 0 ≤ a) → 0 ≤ prod m
[PROOFSTEP]
refine' m.induction_on _ _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ (∀ (a : α), a ∈ 0 → 0 ≤ a) → 0 ≤ prod 0
[PROOFSTEP]
rintro -
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ 0 ≤ prod 0
[PROOFSTEP]
rw [prod_zero]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s) → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → 0 ≤ a_2) → 0 ≤ prod (a ::ₘ s)
[PROOFSTEP]
intro a s hs ih
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s
ih : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → 0 ≤ a_1
⊢ 0 ≤ prod (a ::ₘ s)
[PROOFSTEP]
rw [prod_cons]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : OrderedCommSemiring α
m : Multiset α
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → 0 ≤ a) → 0 ≤ prod s
ih : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → 0 ≤ a_1
⊢ 0 ≤ a * prod s
[PROOFSTEP]
exact mul_nonneg (ih _ <| mem_cons_self _ _) (hs fun a ha => ih _ <| mem_cons_of_mem ha)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
m : Multiset α
h : ∀ (x : α), x ∈ m → x = 1
⊢ prod m = 1
[PROOFSTEP]
induction' m using Quotient.inductionOn with l
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CommMonoid α
m : Multiset α
h✝ : ∀ (x : α), x ∈ m → x = 1
l : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → x = 1
⊢ prod (Quotient.mk (List.isSetoid α) l) = 1
[PROOFSTEP]
simp [List.prod_eq_one h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CanonicallyOrderedMonoid α
m : Multiset α
a : α
h : a ∈ m
⊢ a ≤ prod m
[PROOFSTEP]
obtain ⟨m', rfl⟩ := exists_cons_of_mem h
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CanonicallyOrderedMonoid α
a : α
m' : Multiset α
h : a ∈ a ::ₘ m'
⊢ a ≤ prod (a ::ₘ m')
[PROOFSTEP]
rw [prod_cons]
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : CanonicallyOrderedMonoid α
a : α
m' : Multiset α
h : a ∈ a ::ₘ m'
⊢ a ≤ a * prod m'
[PROOFSTEP]
exact _root_.le_mul_right (le_refl a)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
s : Multiset α
hps : ∀ (a : α), a ∈ s → p a
⊢ f (prod s) ≤ prod (map f s)
[PROOFSTEP]
revert s
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (s : Multiset α), (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
[PROOFSTEP]
refine' Multiset.induction _ _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ prod (map f 0)
[PROOFSTEP]
simp [le_of_eq h_one]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)) →
      (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
[PROOFSTEP]
intro a s hs hpsa
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
[PROOFSTEP]
have hps : ∀ x, x ∈ s → p x := fun x hx => hpsa x (mem_cons_of_mem hx)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hps : ∀ (x : α), x ∈ s → p x
⊢ f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
[PROOFSTEP]
have hp_prod : p s.prod := prod_induction p s hp_mul hp_one hps
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p (prod s)
⊢ f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
[PROOFSTEP]
rw [prod_cons, map_cons, prod_cons]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_one : f 1 = 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p (prod s)
⊢ f (a * prod s) ≤ f a * prod (map f s)
[PROOFSTEP]
exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans (mul_le_mul_left' (hs hps) _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_one : f 1 = 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ ∀ (a b : α), (fun x => True) a → (fun x => True) b → (fun x => True) (a * b)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_one : f 1 = 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ ∀ (a : α), a ∈ s → (fun x => True) a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
s : Multiset α
hs_nonempty : s ≠ ∅
hs : ∀ (a : α), a ∈ s → p a
⊢ f (prod s) ≤ prod (map f s)
[PROOFSTEP]
revert s
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (s : Multiset α), s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
[PROOFSTEP]
refine' Multiset.induction _ _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ 0 ≠ ∅ → (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ prod (map f 0)
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
h : 0 ≠ ∅
⊢ (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ prod (map f 0)
[PROOFSTEP]
exfalso
[GOAL]
case refine'_1.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
h : 0 ≠ ∅
⊢ False
[PROOFSTEP]
exact h rfl
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)) →
      a ::ₘ s ≠ ∅ → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
[PROOFSTEP]
rintro a s hs - hsa_prop
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
[PROOFSTEP]
rw [prod_cons, map_cons, prod_cons]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (a * prod s) ≤ f a * prod (map f s)
[PROOFSTEP]
by_cases hs_empty : s = ∅
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ f (a * prod s) ≤ f a * prod (map f s)
[PROOFSTEP]
simp [hs_empty]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ f (a * prod s) ≤ f a * prod (map f s)
[PROOFSTEP]
have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
⊢ f (a * prod s) ≤ f a * prod (map f s)
[PROOFSTEP]
have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
hp_sup : p (prod s)
⊢ f (a * prod s) ≤ f a * prod (map f s)
[PROOFSTEP]
have hp_a : p a := hsa_prop a (mem_cons_self a s)
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
hp_sup : p (prod s)
hp_a : p a
⊢ f (a * prod s) ≤ f a * prod (map f s)
[PROOFSTEP]
exact (h_mul a _ hp_a hp_sup).trans (mul_le_mul_left' (hs hs_empty hsa_restrict) _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ ∀ (a b : α), (fun x => True) a → (fun x => True) b → f (a * b) ≤ f a * f b
[PROOFSTEP]
simp [h_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ ∀ (a b : α), (fun x => True) a → (fun x => True) b → (fun x => True) (a * b)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ ∀ (a : α), a ∈ s → (fun x => True) a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Multiset α
⊢ sum (map (fun a => {a}) 0) = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, sum (map (fun a => {a}) s) = s → sum (map (fun a => {a}) (a ::ₘ s)) = a ::ₘ s
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Multiset ℕ
n : ℕ
⊢ sum s % n = sum (map (fun x => x % n) s) % n
[PROOFSTEP]
induction s using Multiset.induction
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n : ℕ
⊢ sum 0 % n = sum (map (fun x => x % n) 0) % n
[PROOFSTEP]
simp [Nat.add_mod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : sum s✝ % n = sum (map (fun x => x % n) s✝) % n
⊢ sum (a✝¹ ::ₘ s✝) % n = sum (map (fun x => x % n) (a✝¹ ::ₘ s✝)) % n
[PROOFSTEP]
simp [Nat.add_mod, *]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Multiset ℕ
n : ℕ
⊢ prod s % n = prod (map (fun x => x % n) s) % n
[PROOFSTEP]
induction s using Multiset.induction
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n : ℕ
⊢ prod 0 % n = prod (map (fun x => x % n) 0) % n
[PROOFSTEP]
simp [Nat.mul_mod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : prod s✝ % n = prod (map (fun x => x % n) s✝) % n
⊢ prod (a✝¹ ::ₘ s✝) % n = prod (map (fun x => x % n) (a✝¹ ::ₘ s✝)) % n
[PROOFSTEP]
simp [Nat.mul_mod, *]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Multiset ℤ
n : ℤ
⊢ sum s % n = sum (map (fun x => x % n) s) % n
[PROOFSTEP]
induction s using Multiset.induction
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n : ℤ
⊢ sum 0 % n = sum (map (fun x => x % n) 0) % n
[PROOFSTEP]
simp [Int.add_emod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : sum s✝ % n = sum (map (fun x => x % n) s✝) % n
⊢ sum (a✝¹ ::ₘ s✝) % n = sum (map (fun x => x % n) (a✝¹ ::ₘ s✝)) % n
[PROOFSTEP]
simp [Int.add_emod, *]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Multiset ℤ
n : ℤ
⊢ prod s % n = prod (map (fun x => x % n) s) % n
[PROOFSTEP]
induction s using Multiset.induction
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n : ℤ
⊢ prod 0 % n = prod (map (fun x => x % n) 0) % n
[PROOFSTEP]
simp [Int.mul_emod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : prod s✝ % n = prod (map (fun x => x % n) s✝) % n
⊢ prod (a✝¹ ::ₘ s✝) % n = prod (map (fun x => x % n) (a✝¹ ::ₘ s✝)) % n
[PROOFSTEP]
simp [Int.mul_emod, *]


[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∀ {s : Finset α}, ∏ i in s, x ^ f i = x ^ ∑ x in s, f x
[PROOFSTEP]
apply Finset.induction
[GOAL]
case empty
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∏ i in ∅, x ^ f i = x ^ ∑ x in ∅, f x
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s → ∏ i in s, x ^ f i = x ^ ∑ x in s, f x → ∏ i in insert a s, x ^ f i = x ^ ∑ x in insert a s, f x
[PROOFSTEP]
intro a s has H
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
a : α
s : Finset α
has : ¬a ∈ s
H : ∏ i in s, x ^ f i = x ^ ∑ x in s, f x
⊢ ∏ i in insert a s, x ^ f i = x ^ ∑ x in insert a s, f x
[PROOFSTEP]
rw [Finset.prod_insert has, Finset.sum_insert has, pow_add, H]
[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
⊢ (∑ x₁ in s₁, f₁ x₁) * ∑ x₂ in s₂, f₂ x₂ = ∑ p in s₁ ×ˢ s₂, f₁ p.fst * f₂ p.snd
[PROOFSTEP]
rw [sum_product, sum_mul, sum_congr rfl]
[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
⊢ ∀ (x : ι₁), x ∈ s₁ → f₁ x * ∑ x₂ in s₂, f₂ x₂ = ∑ y in s₂, f₁ (x, y).fst * f₂ (x, y).snd
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
x✝ : ι₁
a✝ : x✝ ∈ s₁
⊢ f₁ x✝ * ∑ x₂ in s₂, f₂ x₂ = ∑ y in s₂, f₁ (x✝, y).fst * f₂ (x✝, y).snd
[PROOFSTEP]
rw [mul_sum]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝¹ : NonAssocSemiring β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
⊢ (∑ x in s, f x * if a = x then 1 else 0) = if a ∈ s then f a else 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝¹ : NonAssocSemiring β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
⊢ ∑ x in s, (if a = x then 1 else 0) * f x = if a ∈ s then f a else 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b✝ : β
f✝ g : α → β
inst✝ : DivisionSemiring β
s : Finset α
f : α → β
b : β
⊢ (∑ x in s, f x) / b = ∑ x in s, f x / b
[PROOFSTEP]
simp only [div_eq_mul_inv, sum_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
s : Finset α
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
⊢ ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
induction' s using Finset.induction with a s ha ih
[GOAL]
case empty
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
⊢ ∏ a in ∅, ∑ b in t a, f a b = ∑ p in pi ∅ t, ∏ x in attach ∅, f (↑x) (p ↑x (_ : ↑x ∈ ∅))
[PROOFSTEP]
rw [pi_empty, sum_singleton]
[GOAL]
case empty
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
⊢ ∏ a in ∅, ∑ b in t a, f a b = ∏ x in attach ∅, f (↑x) (Pi.empty (fun a => δ a) ↑x (_ : ↑x ∈ ∅))
[PROOFSTEP]
rfl
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
⊢ ∏ a in insert a s, ∑ b in t a, f a b =
    ∑ p in pi (insert a s) t, ∏ x in attach (insert a s), f (↑x) (p ↑x (_ : ↑x ∈ insert a s))
[PROOFSTEP]
have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) :=
  by
  intro x _ y _ h
  simp only [disjoint_iff_ne, mem_image]
  rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
  have : Pi.cons s a x p₂ a (mem_insert_self _ _) = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
  rw [Pi.cons_same, Pi.cons_same] at this
  exact h this
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
⊢ ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
[PROOFSTEP]
intro x _ y _ h
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝² : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
x : δ a
a✝¹ : x ∈ t a
y : δ a
a✝ : y ∈ t a
h : x ≠ y
⊢ Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
[PROOFSTEP]
simp only [disjoint_iff_ne, mem_image]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝² : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
x : δ a
a✝¹ : x ∈ t a
y : δ a
a✝ : y ∈ t a
h : x ≠ y
⊢ ∀ (a_1 : (a' : α) → a' ∈ insert a s → δ a'),
    (∃ a_2, a_2 ∈ pi s t ∧ Pi.cons s a x a_2 = a_1) →
      ∀ (b : (a' : α) → a' ∈ insert a s → δ a'), (∃ a_3, a_3 ∈ pi s t ∧ Pi.cons s a y a_3 = b) → a_1 ≠ b
[PROOFSTEP]
rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝³ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
x : δ a
a✝² : x ∈ t a
y : δ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : α) → a' ∈ insert a s → δ a'
p₂ : (a : α) → a ∈ s → δ a
left✝¹ : p₂ ∈ pi s t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : α) → a' ∈ insert a s → δ a'
p₃ : (a : α) → a ∈ s → δ a
left✝ : p₃ ∈ pi s t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ False
[PROOFSTEP]
have : Pi.cons s a x p₂ a (mem_insert_self _ _) = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝³ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
x : δ a
a✝² : x ∈ t a
y : δ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : α) → a' ∈ insert a s → δ a'
p₂ : (a : α) → a ∈ s → δ a
left✝¹ : p₂ ∈ pi s t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : α) → a' ∈ insert a s → δ a'
p₃ : (a : α) → a ∈ s → δ a
left✝ : p₃ ∈ pi s t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ Pi.cons s a x p₂ a (_ : a ∈ insert a s) = Pi.cons s a y p₃ a (_ : a ∈ insert a s)
[PROOFSTEP]
rw [eq₂, eq₃, eq]
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝³ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
x : δ a
a✝² : x ∈ t a
y : δ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : α) → a' ∈ insert a s → δ a'
p₂ : (a : α) → a ∈ s → δ a
left✝¹ : p₂ ∈ pi s t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : α) → a' ∈ insert a s → δ a'
p₃ : (a : α) → a ∈ s → δ a
left✝ : p₃ ∈ pi s t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
this : Pi.cons s a x p₂ a (_ : a ∈ insert a s) = Pi.cons s a y p₃ a (_ : a ∈ insert a s)
⊢ False
[PROOFSTEP]
rw [Pi.cons_same, Pi.cons_same] at this
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝³ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
x : δ a
a✝² : x ∈ t a
y : δ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : α) → a' ∈ insert a s → δ a'
p₂ : (a : α) → a ∈ s → δ a
left✝¹ : p₂ ∈ pi s t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : α) → a' ∈ insert a s → δ a'
p₃ : (a : α) → a ∈ s → δ a
left✝ : p₃ ∈ pi s t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
this : x = y
⊢ False
[PROOFSTEP]
exact h this
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
⊢ ∏ a in insert a s, ∑ b in t a, f a b =
    ∑ p in pi (insert a s) t, ∏ x in attach (insert a s), f (↑x) (p ↑x (_ : ↑x ∈ insert a s))
[PROOFSTEP]
rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
⊢ ∑ x in t a, f a x * ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s)) =
    ∑ x in t a, ∑ i in image (Pi.cons s a x) (pi s t), ∏ x in attach (insert a s), f (↑x) (i ↑x (_ : ↑x ∈ insert a s))
[PROOFSTEP]
refine' sum_congr rfl fun b _ => _
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝ : b ∈ t a
⊢ f a b * ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s)) =
    ∑ i in image (Pi.cons s a b) (pi s t), ∏ x in attach (insert a s), f (↑x) (i ↑x (_ : ↑x ∈ insert a s))
[PROOFSTEP]
have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ := fun p₁ _ p₂ _ eq =>
  Pi.cons_injective ha eq
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
⊢ f a b * ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s)) =
    ∑ i in image (Pi.cons s a b) (pi s t), ∏ x in attach (insert a s), f (↑x) (i ↑x (_ : ↑x ∈ insert a s))
[PROOFSTEP]
rw [sum_image h₂, mul_sum]
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
⊢ ∑ x in pi s t, f a b * ∏ x_1 in attach s, f (↑x_1) (x ↑x_1 (_ : ↑x_1 ∈ s)) =
    ∑ x in pi s t, ∏ x_1 in attach (insert a s), f (↑x_1) (Pi.cons s a b x ↑x_1 (_ : ↑x_1 ∈ insert a s))
[PROOFSTEP]
refine' sum_congr rfl fun g _ => _
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
⊢ f a b * ∏ x in attach s, f (↑x) (g ↑x (_ : ↑x ∈ s)) =
    ∏ x in attach (insert a s), f (↑x) (Pi.cons s a b g ↑x (_ : ↑x ∈ insert a s))
[PROOFSTEP]
rw [attach_insert, prod_insert, prod_image]
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
⊢ f a b * ∏ x in attach s, f (↑x) (g ↑x (_ : ↑x ∈ s)) =
    f (↑{ val := a, property := (_ : a ∈ insert a s) })
        (Pi.cons s a b g ↑{ val := a, property := (_ : a ∈ insert a s) }
          (_ : ↑{ val := a, property := (_ : a ∈ insert a s) } ∈ insert a s)) *
      ∏ x in attach s,
        f (↑{ val := ↑x, property := (_ : ↑x ∈ insert a s) })
          (Pi.cons s a b g ↑{ val := ↑x, property := (_ : ↑x ∈ insert a s) }
            (_ : ↑{ val := ↑x, property := (_ : ↑x ∈ insert a s) } ∈ insert a s))
[PROOFSTEP]
simp only [Pi.cons_same]
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
⊢ f a b * ∏ x in attach s, f (↑x) (g ↑x (_ : ↑x ∈ s)) =
    f a b *
      ∏ x in attach s,
        f (↑x)
          (Pi.cons s a b g ↑{ val := ↑x, property := (_ : ↑x ∈ insert a s) }
            (_ : ↑{ val := ↑x, property := (_ : ↑x ∈ insert a s) } ∈ insert a s))
[PROOFSTEP]
congr with ⟨v, hv⟩
[GOAL]
case insert.e_a.e_f.h.mk
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
v : α
hv : v ∈ s
⊢ f (↑{ val := v, property := hv }) (g ↑{ val := v, property := hv } (_ : ↑{ val := v, property := hv } ∈ s)) =
    f (↑{ val := v, property := hv })
      (Pi.cons s a b g
        ↑{ val := ↑{ val := v, property := hv }, property := (_ : ↑{ val := v, property := hv } ∈ insert a s) }
        (_ :
          ↑{ val := ↑{ val := v, property := hv }, property := (_ : ↑{ val := v, property := hv } ∈ insert a s) } ∈
            insert a s))
[PROOFSTEP]
congr
[GOAL]
case insert.e_a.e_f.h.mk.e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
v : α
hv : v ∈ s
⊢ g ↑{ val := v, property := hv } (_ : ↑{ val := v, property := hv } ∈ s) =
    Pi.cons s a b g
      ↑{ val := ↑{ val := v, property := hv }, property := (_ : ↑{ val := v, property := hv } ∈ insert a s) }
      (_ :
        ↑{ val := ↑{ val := v, property := hv }, property := (_ : ↑{ val := v, property := hv } ∈ insert a s) } ∈
          insert a s)
[PROOFSTEP]
exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
v : α
hv : v ∈ s
⊢ a ≠ ↑{ val := v, property := hv }
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
hv : a ∈ s
⊢ False
[PROOFSTEP]
exact ha hv
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
⊢ ∀ (x : { x // x ∈ s }),
    x ∈ attach s →
      ∀ (y : { x // x ∈ s }),
        y ∈ attach s →
          { val := ↑x, property := (_ : ↑x ∈ insert a s) } = { val := ↑y, property := (_ : ↑y ∈ insert a s) } → x = y
[PROOFSTEP]
exact fun _ _ _ _ => Subtype.eq ∘ Subtype.mk.inj
[GOAL]
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b✝ : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
δ : α → Type u_1
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ a in s, ∑ b in t a, f a b = ∑ p in pi s t, ∏ x in attach s, f (↑x) (p ↑x (_ : ↑x ∈ s))
h₁ :
  ∀ (x : δ a),
    x ∈ t a → ∀ (y : δ a), y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t))
b : δ a
x✝¹ : b ∈ t a
h₂ :
  ∀ (p₁ : (a : α) → a ∈ s → δ a),
    p₁ ∈ pi s t → ∀ (p₂ : (a : α) → a ∈ s → δ a), p₂ ∈ pi s t → Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : α) → a ∈ s → δ a
x✝ : g ∈ pi s t
⊢ ¬{ val := a, property := (_ : a ∈ insert a s) } ∈
      image (fun x => { val := ↑x, property := (_ : ↑x ∈ insert a s) }) (attach s)
[PROOFSTEP]
simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and, Subtype.exists, exists_prop, exists_eq_right] using ha
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∏ a in s, (f a + g a) = ∑ t in powerset s, (∏ a in t, f a) * ∏ a in s \ t, g a
[PROOFSTEP]
classical calc
  ∏ a in s, (f a + g a) = ∏ a in s, ∑ p in ({ True, False } : Finset Prop), if p then f a else g a := by simp
  _ =
      ∑ p in (s.pi fun _ => { True, False } : Finset (∀ a ∈ s, Prop)),
        ∏ a in s.attach, if p a.1 a.2 then f a.1 else g a.1 :=
    prod_sum
  _ = ∑ t in s.powerset, (∏ a in t, f a) * ∏ a in s \ t, g a :=
    sum_bij' (fun f _ => s.filter (fun a => ∀ h : a ∈ s, f a h)) (by simp)
      (fun a _ => by
        rw [prod_ite]
        congr 1
        exact
          prod_bij' (fun a _ => a.1) (by simp; tauto) (by simp) (fun a ha => ⟨a, (mem_filter.1 ha).1⟩)
            (fun a ha => by simp at ha ; simp; tauto) (by simp) (by simp)
        exact
          prod_bij' (fun a _ => a.1) (by simp) (by simp) (fun a ha => ⟨a, (mem_sdiff.1 ha).1⟩)
            (fun a ha => by simp at ha ; simp; tauto) (by simp) (by simp))
      (fun t _ a _ => a ∈ t) (by simp [Classical.em])
      (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
      (by simp_rw [ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∏ a in s, (f a + g a) = ∑ t in powerset s, (∏ a in t, f a) * ∏ a in s \ t, g a
[PROOFSTEP]
calc
  ∏ a in s, (f a + g a) = ∏ a in s, ∑ p in ({ True, False } : Finset Prop), if p then f a else g a := by simp
  _ =
      ∑ p in (s.pi fun _ => { True, False } : Finset (∀ a ∈ s, Prop)),
        ∏ a in s.attach, if p a.1 a.2 then f a.1 else g a.1 :=
    prod_sum
  _ = ∑ t in s.powerset, (∏ a in t, f a) * ∏ a in s \ t, g a :=
    sum_bij' (fun f _ => s.filter (fun a => ∀ h : a ∈ s, f a h)) (by simp)
      (fun a _ => by
        rw [prod_ite]
        congr 1
        exact
          prod_bij' (fun a _ => a.1) (by simp; tauto) (by simp) (fun a ha => ⟨a, (mem_filter.1 ha).1⟩)
            (fun a ha => by simp at ha ; simp; tauto) (by simp) (by simp)
        exact
          prod_bij' (fun a _ => a.1) (by simp) (by simp) (fun a ha => ⟨a, (mem_sdiff.1 ha).1⟩)
            (fun a ha => by simp at ha ; simp; tauto) (by simp) (by simp))
      (fun t _ a _ => a ∈ t) (by simp [Classical.em])
      (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
      (by simp_rw [ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∏ a in s, (f a + g a) = ∏ a in s, ∑ p in {True, False}, if p then f a else g a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∀ (a : (a : α) → a ∈ s → Prop) (ha : a ∈ pi s fun x => {True, False}),
    (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a ha ∈ powerset s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ (∏ a_1 in attach s, if a ↑a_1 (_ : ↑a_1 ∈ s) then f ↑a_1 else g ↑a_1) =
    (∏ a in (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝, f a) *
      ∏ a in s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝, g a
[PROOFSTEP]
rw [prod_ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ (∏ x in filter (fun a_1 => a ↑a_1 (_ : ↑a_1 ∈ s)) (attach s), f ↑x) *
      ∏ x in filter (fun x => ¬a ↑x (_ : ↑x ∈ s)) (attach s), g ↑x =
    (∏ a in (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝, f a) *
      ∏ a in s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝, g a
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∏ x in filter (fun a_1 => a ↑a_1 (_ : ↑a_1 ∈ s)) (attach s), f ↑x =
    ∏ a in (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝, f a
case e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∏ x in filter (fun x => ¬a ↑x (_ : ↑x ∈ s)) (attach s), g ↑x =
    ∏ a in s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝, g a
[PROOFSTEP]
exact
  prod_bij' (fun a _ => a.1) (by simp; tauto) (by simp) (fun a ha => ⟨a, (mem_filter.1 ha).1⟩)
    (fun a ha => by simp at ha ; simp; tauto) (by simp) (by simp)
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : { x // x ∈ s }) (ha : a_1 ∈ filter (fun a_2 => a ↑a_2 (_ : ↑a_2 ∈ s)) (attach s)),
    (fun a_2 x => ↑a_2) a_1 ha ∈ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : α) (b : a_1 ∈ s),
    a a_1 (_ : ↑{ val := a_1, property := b } ∈ s) → ∀ (h : ↑{ val := a_1, property := b } ∈ s), a a_1 h
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : { x // x ∈ s }) (ha : a_1 ∈ filter (fun a_2 => a ↑a_2 (_ : ↑a_2 ∈ s)) (attach s)),
    f ↑a_1 = f ((fun a_2 x => ↑a_2) a_1 ha)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a✝ : (a : α) → a ∈ s → Prop
x✝ : a✝ ∈ pi s fun x => {True, False}
a : α
ha : a ∈ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a✝ x✝
⊢ (fun a ha => { val := a, property := (_ : a ∈ s) }) a ha ∈ filter (fun a => a✝ ↑a (_ : ↑a ∈ s)) (attach s)
[PROOFSTEP]
simp at ha
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a✝ : (a : α) → a ∈ s → Prop
x✝ : a✝ ∈ pi s fun x => {True, False}
a : α
ha✝ : a ∈ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a✝ x✝
ha : a ∈ s ∧ ∀ (h : a ∈ s), a✝ a h
⊢ (fun a ha => { val := a, property := (_ : a ∈ s) }) a ha✝ ∈ filter (fun a => a✝ ↑a (_ : ↑a ∈ s)) (attach s)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a✝ : (a : α) → a ∈ s → Prop
x✝ : a✝ ∈ pi s fun x => {True, False}
a : α
ha✝ : a ∈ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a✝ x✝
ha : a ∈ s ∧ ∀ (h : a ∈ s), a✝ a h
⊢ a✝ a (_ : ↑{ val := a, property := (_ : a ∈ s) } ∈ s)
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : { x // x ∈ s }) (ha : a_1 ∈ filter (fun a_2 => a ↑a_2 (_ : ↑a_2 ∈ s)) (attach s)),
    (fun a_2 ha => { val := a_2, property := (_ : a_2 ∈ s) }) ((fun a_2 x => ↑a_2) a_1 ha)
        (_ : (fun a_2 x => ↑a_2) a_1 ha ∈ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝) =
      a_1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : α) (ha : a_1 ∈ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝),
    (fun a_2 x => ↑a_2) ((fun a_2 ha => { val := a_2, property := (_ : a_2 ∈ s) }) a_1 ha)
        (_ :
          (fun a_2 ha => { val := a_2, property := (_ : a_2 ∈ s) }) a_1 ha ∈
            filter (fun a_2 => a ↑a_2 (_ : ↑a_2 ∈ s)) (attach s)) =
      a_1
[PROOFSTEP]
simp
[GOAL]
case e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∏ x in filter (fun x => ¬a ↑x (_ : ↑x ∈ s)) (attach s), g ↑x =
    ∏ a in s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝, g a
[PROOFSTEP]
exact
  prod_bij' (fun a _ => a.1) (by simp) (by simp) (fun a ha => ⟨a, (mem_sdiff.1 ha).1⟩)
    (fun a ha => by simp at ha ; simp; tauto) (by simp) (by simp)
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : { x // x ∈ s }) (ha : a_1 ∈ filter (fun x => ¬a ↑x (_ : ↑x ∈ s)) (attach s)),
    (fun a_2 x => ↑a_2) a_1 ha ∈ s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : { x // x ∈ s }) (ha : a_1 ∈ filter (fun x => ¬a ↑x (_ : ↑x ∈ s)) (attach s)),
    g ↑a_1 = g ((fun a_2 x => ↑a_2) a_1 ha)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a✝ : (a : α) → a ∈ s → Prop
x✝ : a✝ ∈ pi s fun x => {True, False}
a : α
ha : a ∈ s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a✝ x✝
⊢ (fun a ha => { val := a, property := (_ : a ∈ s) }) a ha ∈ filter (fun x => ¬a✝ ↑x (_ : ↑x ∈ s)) (attach s)
[PROOFSTEP]
simp at ha
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a✝ : (a : α) → a ∈ s → Prop
x✝ : a✝ ∈ pi s fun x => {True, False}
a : α
ha✝ : a ∈ s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a✝ x✝
ha : a ∈ s ∧ (a ∈ s → ∃ x, ¬a✝ a x)
⊢ (fun a ha => { val := a, property := (_ : a ∈ s) }) a ha✝ ∈ filter (fun x => ¬a✝ ↑x (_ : ↑x ∈ s)) (attach s)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a✝ : (a : α) → a ∈ s → Prop
x✝ : a✝ ∈ pi s fun x => {True, False}
a : α
ha✝ : a ∈ s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a✝ x✝
ha : a ∈ s ∧ (a ∈ s → ∃ x, ¬a✝ a x)
⊢ ¬a✝ a (_ : ↑{ val := a, property := (_ : a ∈ s) } ∈ s)
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : { x // x ∈ s }) (ha : a_1 ∈ filter (fun x => ¬a ↑x (_ : ↑x ∈ s)) (attach s)),
    (fun a_2 ha => { val := a_2, property := (_ : a_2 ∈ s) }) ((fun a_2 x => ↑a_2) a_1 ha)
        (_ : ↑a_1 ∈ s \ filter (fun a_2 => ∀ (h : a_2 ∈ s), a a_2 h) s) =
      a_1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
a : (a : α) → a ∈ s → Prop
x✝ : a ∈ pi s fun x => {True, False}
⊢ ∀ (a_1 : α) (ha : a_1 ∈ s \ (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a x✝),
    (fun a_2 x => ↑a_2) ((fun a_2 ha => { val := a_2, property := (_ : a_2 ∈ s) }) a_1 ha)
        (_ :
          (fun a_2 ha => { val := a_2, property := (_ : a_2 ∈ s) }) a_1 ha ∈
            filter (fun x => ¬a ↑x (_ : ↑x ∈ s)) (attach s)) =
      a_1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∀ (a : Finset α) (ha : a ∈ powerset s), (fun t x a x => a ∈ t) a ha ∈ pi s fun x => {True, False}
[PROOFSTEP]
simp [Classical.em]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∀ (a : (a : α) → a ∈ s → Prop) (ha : a ∈ pi s fun x => {True, False}),
    (fun t x a x => a ∈ t) ((fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) a ha)
        (_ : filter (fun a_1 => ∀ (h : a_1 ∈ s), a a_1 h) s ∈ powerset s) =
      a
[PROOFSTEP]
simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∀ (a : (a : α) → a ∈ s → Prop),
    (∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h = True ∨ a a_1 h ∈ {False}) →
      ∀ (a_1 : α) (a_2 : a_1 ∈ s), (a_1 ∈ s ∧ ∀ (h : a_1 ∈ s), a a_1 h) ↔ a a_1 a_2
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∀ (a : Finset α) (ha : a ∈ powerset s),
    (fun f x => filter (fun a => ∀ (h : a ∈ s), f a h) s) ((fun t x a x => a ∈ t) a ha)
        (_ : (fun a_1 x => a_1 ∈ a) ∈ pi s fun x => {True, False}) =
      a
[PROOFSTEP]
simp_rw [ext_iff, @mem_filter _ _ (id _), mem_powerset]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝¹ : CommSemiring β
inst✝ : DecidableEq α
f g : α → β
s : Finset α
⊢ ∀ (a : Finset α), a ⊆ s → ∀ (a_1 : α), a_1 ∈ s ∧ (a_1 ∈ s → a_1 ∈ a) ↔ a_1 ∈ a
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
[PROOFSTEP]
refine' Finset.induction_on_max s (by simp) _
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i in ∅, (f i + g i) =
    ∏ i in ∅, f i +
      ∑ i in ∅, (g i * ∏ j in filter (fun x => x < i) ∅, (f j + g j)) * ∏ j in filter (fun j => i < j) ∅, f j
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ (x : ι), x ∈ s → x < a) →
      ∏ i in s, (f i + g i) =
          ∏ i in s, f i +
            ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j →
        ∏ i in insert a s, (f i + g i) =
          ∏ i in insert a s, f i +
            ∑ i in insert a s,
              (g i * ∏ j in filter (fun x => x < i) (insert a s), (f j + g j)) *
                ∏ j in filter (fun j => i < j) (insert a s), f j
[PROOFSTEP]
clear s
[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ (x : ι), x ∈ s → x < a) →
      ∏ i in s, (f i + g i) =
          ∏ i in s, f i +
            ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j →
        ∏ i in insert a s, (f i + g i) =
          ∏ i in insert a s, f i +
            ∑ i in insert a s,
              (g i * ∏ j in filter (fun x => x < i) (insert a s), (f j + g j)) *
                ∏ j in filter (fun j => i < j) (insert a s), f j
[PROOFSTEP]
intro a s ha ihs
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
⊢ ∏ i in insert a s, (f i + g i) =
    ∏ i in insert a s, f i +
      ∑ i in insert a s,
        (g i * ∏ j in filter (fun x => x < i) (insert a s), (f j + g j)) *
          ∏ j in filter (fun j => i < j) (insert a s), f j
[PROOFSTEP]
have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ ∏ i in insert a s, (f i + g i) =
    ∏ i in insert a s, f i +
      ∑ i in insert a s,
        (g i * ∏ j in filter (fun x => x < i) (insert a s), (f j + g j)) *
          ∏ j in filter (fun j => i < j) (insert a s), f j
[PROOFSTEP]
rw [prod_insert ha', prod_insert ha', sum_insert ha', filter_insert, if_neg (lt_irrefl a), filter_true_of_mem ha, ihs,
  add_mul, mul_add, mul_add, add_assoc]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ f a * ∏ i in s, f i +
      (f a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j +
        (g a * ∏ i in s, f i +
          g a *
            ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j)) =
    f a * ∏ x in s, f x +
      ((g a * ∏ i in s, f i +
            g a *
              ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j) *
          ∏ j in filter (fun j => a < j) (insert a s), f j +
        ∑ x in s,
          (g x * ∏ j in filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) *
            ∏ j in filter (fun j => x < j) (insert a s), f j)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ f a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j +
      (g a * ∏ i in s, f i +
        g a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j) =
    (g a * ∏ i in s, f i +
          g a *
            ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j) *
        ∏ j in filter (fun j => a < j) (insert a s), f j +
      ∑ x in s,
        (g x * ∏ j in filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) *
          ∏ j in filter (fun j => x < j) (insert a s), f j
[PROOFSTEP]
rw [add_comm]
[GOAL]
case e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ g a * ∏ i in s, f i +
        g a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j +
      f a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j =
    (g a * ∏ i in s, f i +
          g a *
            ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j) *
        ∏ j in filter (fun j => a < j) (insert a s), f j +
      ∑ x in s,
        (g x * ∏ j in filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) *
          ∏ j in filter (fun j => x < j) (insert a s), f j
[PROOFSTEP]
congr 1
[GOAL]
case e_a.e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ g a * ∏ i in s, f i +
      g a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j =
    (g a * ∏ i in s, f i +
        g a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j) *
      ∏ j in filter (fun j => a < j) (insert a s), f j
[PROOFSTEP]
rw [filter_false_of_mem, prod_empty, mul_one]
[GOAL]
case e_a.e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ ∀ (x : ι), x ∈ insert a s → ¬a < x
[PROOFSTEP]
exact (forall_mem_insert _ _ _).2 ⟨lt_irrefl a, fun i hi => (ha i hi).not_lt⟩
[GOAL]
case e_a.e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ f a * ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j =
    ∑ x in s,
      (g x * ∏ j in filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) *
        ∏ j in filter (fun j => x < j) (insert a s), f j
[PROOFSTEP]
rw [mul_sum]
[GOAL]
case e_a.e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
⊢ ∑ x in s, f a * ((g x * ∏ j in filter (fun x_1 => x_1 < x) s, (f j + g j)) * ∏ j in filter (fun j => x < j) s, f j) =
    ∑ x in s,
      (g x * ∏ j in filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) *
        ∏ j in filter (fun j => x < j) (insert a s), f j
[PROOFSTEP]
refine' sum_congr rfl fun i hi => _
[GOAL]
case e_a.e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
i : ι
hi : i ∈ s
⊢ f a * ((g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j) =
    (g i * ∏ j in filter (fun x => x < i) (insert a s), (f j + g j)) * ∏ j in filter (fun j => i < j) (insert a s), f j
[PROOFSTEP]
rw [filter_insert, if_neg (ha i hi).not_lt, filter_insert, if_pos (ha i hi), prod_insert, mul_left_comm]
[GOAL]
case e_a.e_a
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ (x : ι), x ∈ s → x < a
ihs :
  ∏ i in s, (f i + g i) =
    ∏ i in s, f i +
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j + g j)) * ∏ j in filter (fun j => i < j) s, f j
ha' : ¬a ∈ s
i : ι
hi : i ∈ s
⊢ ¬a ∈ filter (fun j => i < j) s
[PROOFSTEP]
exact mt (fun ha => (mem_filter.1 ha).1) ha'
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i in s, (f i - g i) =
    ∏ i in s, f i -
      ∑ i in s, (g i * ∏ j in filter (fun x => x < i) s, (f j - g j)) * ∏ j in filter (fun j => i < j) s, f j
[PROOFSTEP]
simp only [sub_eq_add_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ x in s, (f x + -g x) =
    ∏ i in s, f i +
      -∑ x in s, (g x * ∏ x in filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i in filter (fun j => x < j) s, f i
[PROOFSTEP]
convert prod_add_ordered s f fun i => -g i
[GOAL]
case h.e'_3.h.e'_6
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ -∑ x in s, (g x * ∏ x in filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i in filter (fun j => x < j) s, f i =
    ∑ i in s, (-g i * ∏ j in filter (fun x => x < i) s, (f j + -g j)) * ∏ j in filter (fun j => i < j) s, f j
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i in s, (1 - f i) = 1 - ∑ i in s, f i * ∏ j in filter (fun x => x < i) s, (1 - f j)
[PROOFSTEP]
rw [prod_sub_ordered]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i in s, 1 - ∑ i in s, (f i * ∏ j in filter (fun x => x < i) s, (1 - f j)) * ∏ j in filter (fun j => i < j) s, 1 =
    1 - ∑ i in s, f i * ∏ j in filter (fun x => x < i) s, (1 - f j)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s : Finset α
⊢ ∑ t in powerset s, a ^ card t * b ^ (card s - card t) = (a + b) ^ card s
[PROOFSTEP]
classical
rw [← prod_const, prod_add]
refine' Finset.sum_congr rfl fun t ht => _
rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s : Finset α
⊢ ∑ t in powerset s, a ^ card t * b ^ (card s - card t) = (a + b) ^ card s
[PROOFSTEP]
rw [← prod_const, prod_add]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s : Finset α
⊢ ∑ t in powerset s, a ^ card t * b ^ (card s - card t) = ∑ t in powerset s, (∏ a_1 in t, a) * ∏ a in s \ t, b
[PROOFSTEP]
refine' Finset.sum_congr rfl fun t ht => _
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a✝ : α✝
b✝ : β
f g : α✝ → β
inst✝¹ : CommSemiring β
α : Type u_1
R : Type u_2
inst✝ : CommSemiring R
a b : R
s t : Finset α
ht : t ∈ powerset s
⊢ a ^ card t * b ^ (card s - card t) = (∏ a_1 in t, a) * ∏ a in s \ t, b
[PROOFSTEP]
rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b✝ : β
f✝ g : α → β
inst✝ : CommSemiring β
b : β
s : Finset α
f : α → β
h : ∀ (x : α), x ∈ s → b ∣ f x
y : β
hy : y ∈ Multiset.map (fun x => f x) s.val
⊢ b ∣ y
[PROOFSTEP]
rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b✝ : β
f✝ g : α → β
inst✝ : CommSemiring β
b : β
s : Finset α
f : α → β
h : ∀ (x : α), x ∈ s → b ∣ f x
x : α
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun x => f x) s.val
⊢ b ∣ f x
[PROOFSTEP]
exact h x hx
[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f g : α → β
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i in range k, (↑n - ↑i) = ↑(∏ i in range k, (n - i))
[PROOFSTEP]
rw [prod_natCast]
[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f g : α → β
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i in range k, (↑n - ↑i) = ∏ x in range k, ↑(n - x)
[PROOFSTEP]
cases' le_or_lt k n with hkn hnk
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f g : α → β
R : Type u_1
inst✝ : CommRing R
n k : ℕ
hkn : k ≤ n
⊢ ∏ i in range k, (↑n - ↑i) = ∏ x in range k, ↑(n - x)
[PROOFSTEP]
exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f g : α → β
R : Type u_1
inst✝ : CommRing R
n k : ℕ
hnk : n < k
⊢ ∏ i in range k, (↑n - ↑i) = ∏ x in range k, ↑(n - x)
[PROOFSTEP]
rw [← mem_range] at hnk
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f g : α → β
R : Type u_1
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ∏ i in range k, (↑n - ↑i) = ∏ x in range k, ↑(n - x)
[PROOFSTEP]
rw [prod_eq_zero hnk, prod_eq_zero hnk]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f g : α → β
R : Type u_1
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑(n - n) = 0
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f g : α → β
R : Type u_1
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑n - ↑n = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∏ a in powerset (insert x s), f a = (∏ a in powerset s, f a) * ∏ t in powerset s, f (insert x t)
[PROOFSTEP]
rw [powerset_insert, Finset.prod_union, Finset.prod_image]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∀ (x_1 : Finset α), x_1 ∈ powerset s → ∀ (y : Finset α), y ∈ powerset s → insert x x_1 = insert x y → x_1 = y
[PROOFSTEP]
intro t₁ h₁ t₂ h₂ heq
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ powerset s
heq : insert x t₁ = insert x t₂
⊢ t₁ = t₂
[PROOFSTEP]
rw [← Finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₁ h), ←
  Finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₂ h), heq]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ Disjoint (powerset s) (image (insert x) (powerset s))
[PROOFSTEP]
rw [Finset.disjoint_iff_ne]
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∀ (a : Finset α), a ∈ powerset s → ∀ (b : Finset α), b ∈ image (insert x) (powerset s) → a ≠ b
[PROOFSTEP]
intro t₁ h₁ t₂ h₂
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
⊢ t₁ ≠ t₂
[PROOFSTEP]
rcases Finset.mem_image.1 h₂ with ⟨t₃, _h₃, H₃₂⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
t₃ : Finset α
_h₃ : t₃ ∈ powerset s
H₃₂ : insert x t₃ = t₂
⊢ t₁ ≠ t₂
[PROOFSTEP]
rw [← H₃₂]
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
t₃ : Finset α
_h₃ : t₃ ∈ powerset s
H₃₂ : insert x t₃ = t₂
⊢ t₁ ≠ insert x t₃
[PROOFSTEP]
exact ne_insert_of_not_mem _ _ (not_mem_of_mem_powerset_of_not_mem h₁ h)
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : Finset α → β
⊢ ∏ t in powerset s, f t = ∏ j in range (card s + 1), ∏ t in powersetLen j s, f t
[PROOFSTEP]
rw [powerset_card_disjiUnion, prod_disjiUnion]
[GOAL]
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝ : NonUnitalNonAssocSemiring β
n k : ℕ
f g : ℕ → β
⊢ (∑ i in range (n + 1), f i) * ∑ i in range (k + 1), g i =
    (∑ i in range n, f i) * ∑ i in range k, g i + f n * ∑ i in range k, g i + (∑ i in range n, f i) * g k + f n * g k
[PROOFSTEP]
simp only [add_mul, mul_add, add_assoc, sum_range_succ]