refine' Finset.memberFamily_induction_on 𝒜 _ _ _
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑∅).OrdConnected → (∅ \₊ ∅).card ≤ ∅.card

case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑{∅}).OrdConnected → ({∅} \₊ {∅}).card ≤ {∅}.card

case refine'_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    ((↑(nonMemberSubfamily a 𝒜)).OrdConnected →
        (nonMemberSubfamily a 𝒜 \₊ nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).card) →
      ((↑(memberSubfamily a 𝒜)).OrdConnected →
          (memberSubfamily a 𝒜 \₊ memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).card) →
        (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card