Theorem: encard_biUnion (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ (⋃ i ∈ t, s i).encard = ∑ i ∈ t, (s i).encard
Tactic:
convert encard_iUnion (fun i : t ↦ s i) ?_
State after:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ ⋃ i ∈ t, s i = ⋃ i, s ↑i

case h.e'_3
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ ∑ i ∈ t, (s i).encard = ∑ i : { x // x ∈ t }, (s ↑i).encard

α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ univ.PairwiseDisjoint fun i => s ↑i

State before:
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ univ.PairwiseDisjoint fun i => s ↑i
Tactic:
rintro ⟨i, hi⟩ - ⟨j, hj⟩ - hne
State after:
case mk.mk
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
hne : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (Disjoint on fun i => s ↑i) ⟨i, hi⟩ ⟨j, hj⟩

State before:
case mk.mk
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
hne : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (Disjoint on fun i => s ↑i) ⟨i, hi⟩ ⟨j, hj⟩
Tactic:
exact disjoint_iff_forall_ne.2 (ht hi hj (by simpa using hne)).ne_of_mem
State after:
no goals

State before:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ ⋃ i ∈ t, s i = ⋃ i, s ↑i
Tactic:
ext x
State after:
case h.e'_2.h.e'_2.h
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
x : α
⊢ x ∈ ⋃ i ∈ t, s i ↔ x ∈ ⋃ i, s ↑i

State before:
case h.e'_2.h.e'_2.h
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
x : α
⊢ x ∈ ⋃ i ∈ t, s i ↔ x ∈ ⋃ i, s ↑i
Tactic:
simp
State after:
no goals

State before:
case h.e'_3
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ ∑ i ∈ t, (s i).encard = ∑ i : { x // x ∈ t }, (s ↑i).encard
Tactic:
rw [Finset.univ_eq_attach, Finset.sum_attach _ (f := fun i ↦ (s i).encard)]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
hne : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ i ≠ j
Tactic:
simpa using hne
State after:
no goals