rintro a 𝒜 h𝒜₀ h𝒜₁ h𝒜
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
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
h𝒜₀ :
  (↑(nonMemberSubfamily a 𝒜)).OrdConnected →
    (nonMemberSubfamily a 𝒜 \₊ nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).card
h𝒜₁ :
  (↑(memberSubfamily a 𝒜)).OrdConnected → (memberSubfamily a 𝒜 \₊ memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).card
h𝒜 : (↑𝒜).OrdConnected
⊢ (𝒜 \₊ 𝒜).card ≤ 𝒜.card