-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : #s ≤ Fintype.card α
inr :
  ∀ (f : ι → Finset (Finset α))
    (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑(f i) : Set (Finset α)).Intersecting)
    (hs : card.{u_1} (α := ι) ∅ ≤ Fintype.card α),
    #(Finset.biUnion ∅ f) ≤
      HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - card.{u_1} (α := ι) ∅)
inr₁ :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih :
      ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
        #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s))
    (f : ι → Finset (Finset α)) (hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting)
    (hs : #(cons i s hi) ≤ Fintype.card α),
    #((cons i s hi).biUnion f) ≤
      HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)

Tactic:
induction s using Finset.cons_induction generalizing f with
  | empty => simp
  | cons i s hi ih =>
  set f' : ι → Finset (Finset α) :=
    fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
  have hf₁ : ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * #(f' j) =
      2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting := by
    rintro j hj
    simp_rw [f', dif_pos hj, ← Fintype.card_finset]
    exact Classical.choose_spec (hf j hj).exists_card_eq
  have hf₂ : ∀ j, j ∈ cons i s hi → IsUpperSet (f' j : Set (Finset α)) := by
    refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)
    rw [Fintype.card_finset]
    exact (hf₁ _ hj).2.1
  refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
  nth_rw 1 [cons_eq_insert i]
  rw [biUnion_insert]
  refine (card_mono <| @le_sup_sdiff _ _ _ <| f' i).trans ((card_union_le _ _).trans ?_)
  rw [union_sdiff_left, sdiff_eq_inter_compl]
  refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
  rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
  refine (add_le_add
      ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2
      (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
      (mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans ?_
  · rw [coe_biUnion]
    exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
  · rw [coe_compl]
    exact (hf₂ _ <| mem_cons_self _ _).compl
  rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
    (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
    mul_assoc, ← add_mul, mul_comm]
  gcongr
  refine (add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).trans ?_
  rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]

Premises used: add_mul, pow_pos, Finset.coe_biUnion, add_tsub_assoc_of_le, Finset.cons, Finset.card_compl, pow_succ, mul_assoc, two_mul, Fintype.card, add_tsub_cancel_left, mul_left_comm, Finset.coe_compl, Fintype.card_finset, tsub_le_self, Finset.biUnion_insert, le_of_mul_le_mul_left, tsub_add_eq_add_tsub, add_tsub_add_eq_tsub_right, HAdd.hAdd, pow_right_mono₀, Finset.card_cons, Nat, zero_lt_two', mul_comm, one_le_two, mul_add, OfNat.ofNat, Finset.union_sdiff_left, mul_two, pow_succ', mul_tsub, Finset.sdiff_eq_inter_compl