-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
lemma sum_collapse (h𝒜 : 𝒜 ⊆ (insert a u).powerset) (hu : a ∉ u) :
    ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ 𝒜, f s

Proof state:
case calc_2.e_a.e_s.e_a.h.refine_1.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
hs : s ⊆ u
⊢ (insert a s).erase a ⊆ u ∧ ¬insert a s ⊆ u

Tactic:
exact ⟨subset_insert_iff.1 <| insert_subset_insert _ hs, fun h ↦
  hu <| h <| mem_insert_self _ _⟩

Result:
no goals

Proof state:
case calc_2.e_a.e_s.e_a.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ s ∈ image (insert a) u.powerset ↔ s ∈ (insert a u).powerset \ u.powerset

Tactic:
simp only [mem_image, mem_powerset, mem_sdiff, subset_insert_iff]

Result:
case calc_2.e_a.e_s.e_a.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) ↔ s.erase a ⊆ u ∧ ¬s ⊆ u

Proof state:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∀ x ∈ u.powerset, ∀ y ∈ u.powerset, insert a x = insert a y → x = y

Tactic:
exact (insert_erase_invOn.2.injOn).mono fun s hs ↦ not_mem_mono (mem_powerset.1 hs) hu

Result:
no goals

Proof state:
case calc_2.e_a.e_s.e_a.h.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
⊢ insert a (s.erase a) = s

Tactic:
rw [insert_erase (erase_ne_self.1 fun hs ↦ ?_)]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False

Tactic:
exact h.2 h.1

Result:
no goals

Proof state:
case calc_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s = ∑ s ∈ 𝒜, f s

Tactic:
rw [← sum_union (disjoint_sdiff_self_right.mono inf_le_left inf_le_left),
  ← union_inter_distrib_right, union_sdiff_of_subset (powerset_mono.2 <| subset_insert _ _),
  inter_eq_right.2 h𝒜]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ 𝒜, f s

Tactic:
calc
  _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ u.powerset.image (insert a) ∩ 𝒜, f s := ?_
  _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ ((insert a u).powerset \ u.powerset) ∩ 𝒜, f s := ?_
  _ = ∑ s ∈ 𝒜, f s := ?_

Result:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s

case calc_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s =
    ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s

case calc_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s = ∑ s ∈ 𝒜, f s

Proof state:
case calc_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s =
    ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s

Tactic:
congr with s

Result:
case calc_2.e_a.e_s.e_a.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ s ∈ image (insert a) u.powerset ↔ s ∈ (insert a u).powerset \ u.powerset

Proof state:
case calc_2.e_a.e_s.e_a.h.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) → s.erase a ⊆ u ∧ ¬s ⊆ u

Tactic:
rintro ⟨s, hs, rfl⟩

Result:
case calc_2.e_a.e_s.e_a.h.refine_1.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
hs : s ⊆ u
⊢ (insert a s).erase a ⊆ u ∧ ¬insert a s ⊆ u

Proof state:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s

Tactic:
rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]

Result:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    ∑ x ∈ u.powerset, ((if x ∈ 𝒜 then f x else 0) + if insert a x ∈ 𝒜 then f (insert a x) else 0)

case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∀ x ∈ u.powerset, ∀ y ∈ u.powerset, insert a x = insert a y → x = y

Proof state:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    ∑ x ∈ u.powerset, ((if x ∈ 𝒜 then f x else 0) + if insert a x ∈ 𝒜 then f (insert a x) else 0)

Tactic:
exact sum_congr rfl fun s hs ↦ collapse_eq (not_mem_mono (mem_powerset.1 hs) hu) _ _

Result:
no goals