case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))

case refine'_2
α : Type u_1
s✝ t s a : Finset α
ha :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
⊢ a ∈ powerset s
α : Type u_1
s✝ t s : Finset α
⊢ powerset s =
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
refine' ext fun a => ⟨fun ha => _, fun ha => _⟩
case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ ∃ a_1, a_1 ∈ range (card s + 1) ∧ a ∈ powersetLen a_1 s
case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
rw [mem_disjiUnion]
no goals
case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ ∃ a_1, a_1 ∈ range (card s + 1) ∧ a ∈ powersetLen a_1 s
exact
  ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_of_subset (mem_powerset.mp ha))),
    mem_powersetLen.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
case refine'_2.intro.intro
α : Type u_1
s✝ t s a : Finset α
ha✝ :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
i : ℕ
_hi : i ∈ range (card s + 1)
ha : a ∈ powersetLen i s
⊢ a ∈ powerset s
case refine'_2
α : Type u_1
s✝ t s a : Finset α
ha :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
⊢ a ∈ powerset s
rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
no goals
case refine'_2.intro.intro
α : Type u_1
s✝ t s a : Finset α
ha✝ :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
i : ℕ
_hi : i ∈ range (card s + 1)
ha : a ∈ powersetLen i s
⊢ a ∈ powerset s
exact mem_powerset.mpr (mem_powersetLen.mp ha).1