-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@[simp] lemma supSum_singleton (hs : s ≠ univ) :
    supSum ({s} : Finset (Finset α)) = card α * ∑ k ∈ range (card α), (k : ℚ)⁻¹

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ x : Finset α, (↑(card α) - ↑(#({s}.truncatedSup x))) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))

Tactic:
rw [sum_congr rfl fun t _ ↦ this t, sum_ite, sum_const_zero, add_zero, filter_subset_univ,
  sum_powerset, ← binomial_sum_eq ((card_lt_iff_ne_univ _).2 hs), eq_comm]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ ∑ j ∈ range (#s + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ∑ i ∈ range (#s + 1), ↑((#s).choose i) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑i) * ↑((card α).choose i))

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
n : ℕ
x✝ : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ↑((#s).choose n) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑n) * ↑((card α).choose n))

Tactic:
rw [mul_div_assoc, ← nsmul_eq_mul]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
n : ℕ
x✝ : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    (#s).choose n • ((↑(card α) - ↑(#s)) / ((↑(card α) - ↑n) * ↑((card α).choose n)))

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
have : ∀ t : Finset α,
  (card α - #(truncatedSup {s} t) : ℚ) / ((card α - #t) * (card α).choose #t) =
  if t ⊆ s then (card α - #s : ℚ) / ((card α - #t) * (card α).choose #t) else 0 := by
  rintro t
  simp_rw [truncatedSup_singleton, le_iff_subset]
  split_ifs <;> simp

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
⊢ ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0

Tactic:
rintro t

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
⊢ (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq,
  ← eq_sub_iff_add_eq', supSum, ← sum_sub_distrib, ← sub_div]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ x : Finset α, (↑(card α) - ↑(#({s}.truncatedSup x))) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ ∑ j ∈ range (#s + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ∑ i ∈ range (#s + 1), ↑((#s).choose i) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑i) * ↑((card α).choose i))

Tactic:
refine sum_congr rfl fun n _ ↦ ?_

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
n : ℕ
x✝ : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    ↑((#s).choose n) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑n) * ↑((card α).choose n))

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
⊢ (↑(card α) - ↑(#(if t ⊆ s then s else ⊤))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
⊢ (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0

Tactic:
simp_rw [truncatedSup_singleton, le_iff_subset]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
⊢ (↑(card α) - ↑(#(if t ⊆ s then s else ⊤))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
n : ℕ
x✝ : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    (#s).choose n • ((↑(card α) - ↑(#s)) / ((↑(card α) - ↑n) * ↑((card α).choose n)))

Tactic:
exact sum_powersetCard n s fun m ↦ (card α - #s : ℚ) / ((card α - m) * (card α).choose m)

Result:
no goals