-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
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 α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))
inr :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) - 2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
inr₁ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
inr₂ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi) + 1)
inr₃ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
      (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi) + 1)
inr₄ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
      (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      HPow.hPow (α := ℕ) 2 (Fintype.card α + 1 - #(cons i s hi))
inr₅ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
      (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      HPow.hPow (α := ℕ) 2 (Fintype.card α + 1 - (#s + 1))
inr₆ inr₇ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
      (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
      (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s)
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))

Tactic:
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_tsub_assoc_of_le, two_mul, tsub_le_self, tsub_add_eq_add_tsub, add_tsub_add_eq_tsub_right, pow_right_mono₀, Finset.card_cons, one_le_two, pow_succ', mul_tsub