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

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (⋃ i ∈ u, s i).encard = ∑ i ∈ u, (s i).encard ↔ (↑u).PairwiseDisjoint s
Tactic:
change encard (⋃ i ∈ (u : Set ι), _) = _ ↔ _
State after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (⋃ i ∈ ↑u, s i).encard = ∑ i ∈ u, (s i).encard ↔ (↑u).PairwiseDisjoint s

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (⋃ i ∈ ↑u, s i).encard = ∑ i ∈ u, (s i).encard ↔ (↑u).PairwiseDisjoint s
Tactic:
rw [biUnion_eq_iUnion]
State after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (⋃ x, s ↑x).encard = ∑ i ∈ u, (s i).encard ↔ (↑u).PairwiseDisjoint s

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (⋃ x, s ↑x).encard = ∑ i ∈ u, (s i).encard ↔ (↑u).PairwiseDisjoint s
Tactic:
convert encard_iUnion_eq_sum_iff_pairwiseDisjoint (ι := u) (s := fun i ↦ s i) (by simpa)
State after:
case h.e'_1.h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ ∑ i ∈ u, (s i).encard = ∑ i : { x // x ∈ u }, (s ↑i).encard

case h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (↑u).PairwiseDisjoint s ↔ univ.PairwiseDisjoint fun i => s ↑i

State before:
case h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (↑u).PairwiseDisjoint s ↔ univ.PairwiseDisjoint fun i => s ↑i
Tactic:
refine ⟨fun h i _ j _ hij ↦ h i.prop j.prop (by rwa [Ne, Subtype.coe_injective.eq_iff]),
  fun h i hi j hj hij ↦ ?_⟩
State after:
case h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
h : univ.PairwiseDisjoint fun i => s ↑i
i : ι
hi : i ∈ ↑u
j : ι
hj : j ∈ ↑u
hij : i ≠ j
⊢ (Disjoint on s) i j

State before:
case h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
h : univ.PairwiseDisjoint fun i => s ↑i
i : ι
hi : i ∈ ↑u
j : ι
hj : j ∈ ↑u
hij : i ≠ j
⊢ (Disjoint on s) i j
Tactic:
exact h (mem_univ ⟨i, hi⟩) (mem_univ ⟨j,hj⟩) (by simpa)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ ∀ (i : { x // x ∈ u }), ((fun i => s ↑i) i).Finite
Tactic:
simpa
State after:
no goals

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

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
h : (↑u).PairwiseDisjoint s
i : { x // x ∈ u }
x✝¹ : i ∈ univ
j : { x // x ∈ u }
x✝ : j ∈ univ
hij : i ≠ j
⊢ ↑i ≠ ↑j
Tactic:
rwa [Ne, Subtype.coe_injective.eq_iff]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
h : univ.PairwiseDisjoint fun i => s ↑i
i : ι
hi : i ∈ ↑u
j : ι
hj : j ∈ ↑u
hij : i ≠ j
⊢ ⟨i, hi⟩ ≠ ⟨j, hj⟩
Tactic:
simpa
State after:
no goals