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

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard
Tactic:
obtain (⟨i, hi⟩ | h) := em <| ∃ i, (s i).Infinite
State after:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard

case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ¬∃ i, (s i).Infinite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard

State before:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ¬∃ i, (s i).Infinite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard
Tactic:
simp_rw [not_exists, not_infinite] at h
State after:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard

State before:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard
Tactic:
rw [(finite_iUnion h).encard_eq_coe_toFinset_card]
State after:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ↑⋯.toFinset.card = ∑ i : ι, (s i).encard

State before:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ↑⋯.toFinset.card = ∑ i : ι, (s i).encard
Tactic:
simp_rw [(h _).encard_eq_coe_toFinset_card]
State after:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ↑⋯.toFinset.card = ∑ x : ι, ↑⋯.toFinset.card

State before:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ↑⋯.toFinset.card = ∑ x : ι, ↑⋯.toFinset.card
Tactic:
have h_eq := Finset.card_biUnion (s := Finset.univ) (t := fun i ↦ (h i).toFinset) ?_
State after:
case inr.refine_2
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ↑⋯.toFinset.card = ∑ x : ι, ↑⋯.toFinset.card

case inr.refine_1
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ∀ x ∈ Finset.univ, ∀ y ∈ Finset.univ, x ≠ y → Disjoint ((fun i => ⋯.toFinset) x) ((fun i => ⋯.toFinset) y)

State before:
case inr.refine_1
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ∀ x ∈ Finset.univ, ∀ y ∈ Finset.univ, x ≠ y → Disjoint ((fun i => ⋯.toFinset) x) ((fun i => ⋯.toFinset) y)
Tactic:
simp only [Finset.mem_univ, ne_eq, Finite.disjoint_toFinset, forall_true_left]
State after:
case inr.refine_1
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ∀ (x y : ι), ¬x = y → Disjoint (s x) (s y)

State before:
case inr.refine_1
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ∀ (x y : ι), ¬x = y → Disjoint (s x) (s y)
Tactic:
exact fun i j hij ↦ hs (mem_univ i) (mem_univ j) hij
State after:
no goals

State before:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard
Tactic:
rw [(hi.mono (subset_iUnion s i)).encard_eq]
State after:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
⊢ ⊤ = ∑ i : ι, (s i).encard

State before:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
⊢ ⊤ = ∑ i : ι, (s i).encard
Tactic:
have hle := Finset.sum_le_sum_of_subset (f := fun i ↦ encard (s i)) (Finset.subset_univ {i})
State after:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
hle : ∑ x ∈ {i}, (fun i => (s i).encard) x ≤ ∑ x : ι, (fun i => (s i).encard) x
⊢ ⊤ = ∑ i : ι, (s i).encard

State before:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
hle : ∑ x ∈ {i}, (fun i => (s i).encard) x ≤ ∑ x : ι, (fun i => (s i).encard) x
⊢ ⊤ = ∑ i : ι, (s i).encard
Tactic:
simp_rw [Finset.sum_singleton, hi.encard_eq, top_le_iff, eq_comm] at hle
State after:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
hle : ⊤ = ∑ x : ι, (s x).encard
⊢ ⊤ = ∑ i : ι, (s i).encard

State before:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
hle : ⊤ = ∑ x : ι, (s x).encard
⊢ ⊤ = ∑ i : ι, (s i).encard
Tactic:
exact hle
State after:
no goals

State before:
case inr.refine_2
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ↑⋯.toFinset.card = ∑ x : ι, ↑⋯.toFinset.card
Tactic:
convert congr_arg ((↑) : ℕ → ℕ∞) h_eq
State after:
case h.e'_2.h.e'_3.h.e'_2
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ⋯.toFinset = Finset.univ.biUnion fun i => ⋯.toFinset

case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ∑ x : ι, ↑⋯.toFinset.card = ↑(∑ u : ι, ⋯.toFinset.card)

State before:
case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ∑ x : ι, ↑⋯.toFinset.card = ↑(∑ u : ι, ⋯.toFinset.card)
Tactic:
simp only [Nat.cast_sum]
State after:
no goals

State before:
case h.e'_2.h.e'_3.h.e'_2
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ⋯.toFinset = Finset.univ.biUnion fun i => ⋯.toFinset
Tactic:
ext x
State after:
case h.e'_2.h.e'_3.h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ Finset.univ.biUnion fun i => ⋯.toFinset

State before:
case h.e'_2.h.e'_3.h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ Finset.univ.biUnion fun i => ⋯.toFinset
Tactic:
simp
State after:
no goals