Theorem: Finset.card_posDiffs_self_le (LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : (↑𝒜).OrdConnected
⊢ (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Tactic:
revert h𝒜
State after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card

State before:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Tactic:
refine' Finset.memberFamily_induction_on 𝒜 _ _ _
State after:
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

State before:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑∅).OrdConnected → (∅ \₊ ∅).card ≤ ∅.card
Tactic:
simp
State after:
no goals

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

State before:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜✝ : (↑{∅}).OrdConnected
⊢ ({∅} \₊ {∅}).card ≤ {∅}.card
Tactic:
rfl
State after:
no goals

State before:
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
Tactic:
rintro a 𝒜 h𝒜₀ h𝒜₁ h𝒜
State after:
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

State before:
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
Tactic:
sorry
State after:
no goals