α : Type u_1
ι : Sort ?u.15793
κ : ι → Sort ?u.15798
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r in Iic (Fintype.card α), card (𝒜 # r) = card 𝒜
α : Type u_1
ι : Sort ?u.15793
κ : ι → Sort ?u.15798
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
⊢ ∑ r in Iic (Fintype.card α), card (𝒜 # r) = card 𝒜
letI := Classical.decEq α
α : Type u_1
ι : Sort ?u.15793
κ : ι → Sort ?u.15798
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∀ (x : ℕ), x ∈ Iic (Fintype.card α) → ∀ (y : ℕ), y ∈ Iic (Fintype.card α) → x ≠ y → Disjoint (𝒜 # x) (𝒜 # y)
α : Type u_1
ι : Sort ?u.15793
κ : ι → Sort ?u.15798
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r in Iic (Fintype.card α), card (𝒜 # r) = card 𝒜
rw [← card_biUnion, biUnion_slice]
no goals
α : Type u_1
ι : Sort ?u.15793
κ : ι → Sort ?u.15798
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∀ (x : ℕ), x ∈ Iic (Fintype.card α) → ∀ (y : ℕ), y ∈ Iic (Fintype.card α) → x ≠ y → Disjoint (𝒜 # x) (𝒜 # y)
exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)