internlm/Lean-Github huggingface dataset:
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ Nonempty (Fin n ↪ ↑s) ↔ ↑n ≤ s.encard
Tactic:
refine ⟨fun ⟨i⟩ ↦ ?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n ≤ s.encard

case refine_2
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : ↑n ≤ s.encard
⊢ Nonempty (Fin n ↪ ↑s)
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : ↑n ≤ s.encard
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
obtain ⟨t, hts, hcard⟩ := exists_subset_encard_eq h
Proof state after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
⊢ Nonempty (Fin n ↪ ↑s)
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
have ht : t.Finite := finite_of_encard_eq_coe hcard
Proof state after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
ht : t.Finite
⊢ Nonempty (Fin n ↪ ↑s)
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
ht : t.Finite
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
rw [← ht.cast_ncard_eq, Nat.cast_inj, ncard_eq_toFinset_card t ht] at hcard
Proof state after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ Nonempty (Fin n ↪ ↑s)
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
refine ⟨(Finset.equivFinOfCardEq hcard).symm.toEmbedding.trans ?_ ⟩
Proof state after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ ht.toFinset } ↪ ↑s
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ ht.toFinset } ↪ ↑s
Tactic:
simp only [Finite.mem_toFinset]
Proof state after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ t } ↪ ↑s
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ t } ↪ ↑s
Tactic:
exact embeddingOfSubset t s hts
Proof state after:
no goals
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case refine_1
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n ≤ s.encard
Tactic:
convert ((Equiv.Set.univ (Fin n)).toEmbedding.trans i).enccard_le
Proof state after:
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n = univ.encard
Theorem: Fin.nonempty_embedding_iff_le_encard
Proof state before:
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n = univ.encard
Tactic:
simp [encard_univ]
Proof state after:
no goals
Theorem: encard_univ_fin
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n a : ℕ
⊢ univ.encard = ↑a
Tactic:
simp [encard_eq_coe_toFinset_card]
Proof state after:
no goals
Theorem: Fin.nonempty_equiv_iff_encard_eq
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ Nonempty (↑s ≃ Fin n) ↔ s.encard = ↑n
Tactic:
refine ⟨fun ⟨e⟩ ↦ by simpa using e.encard_univ_eq, fun h ↦ ?_⟩
Proof state after:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
⊢ Nonempty (↑s ≃ Fin n)
Theorem: Fin.nonempty_equiv_iff_encard_eq
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
⊢ Nonempty (↑s ≃ Fin n)
Tactic:
have _ := Finite.fintype (finite_of_encard_eq_coe h).to_subtype
Proof state after:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
x✝ : Fintype ↑s
⊢ Nonempty (↑s ≃ Fin n)
Theorem: Fin.nonempty_equiv_iff_encard_eq
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
x✝ : Fintype ↑s
⊢ Nonempty (↑s ≃ Fin n)
Tactic:
exact ⟨Fintype.equivFinOfCardEq <| by simpa [encard_eq_coe_toFinset_card, Nat.cast_inj] using h⟩
Proof state after:
no goals
Theorem: Fin.nonempty_equiv_iff_encard_eq
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (↑s ≃ Fin n)
e : ↑s ≃ Fin n
⊢ s.encard = ↑n
Tactic:
simpa using e.encard_univ_eq
Proof state after:
no goals
Theorem: Fin.nonempty_equiv_iff_encard_eq
Proof state before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
x✝ : Fintype ↑s
⊢ Fintype.card ↑s = n
Tactic:
simpa [encard_eq_coe_toFinset_card, Nat.cast_inj] using h
Proof state after:
no goals
Theorem: PartENat.card_option
Proof state before:
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
⊢ card (Option α) = card α + 1
Tactic:
obtain (hα | hα) := finite_or_infinite α
Proof state after:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
⊢ card (Option α) = card α + 1

case inr
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Infinite α
⊢ card (Option α) = card α + 1
Theorem: PartENat.card_option
Proof state before:
case inr
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Infinite α
⊢ card (Option α) = card α + 1
Tactic:
simp
Proof state after:
no goals
Theorem: PartENat.card_option
Proof state before:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
⊢ card (Option α) = card α + 1
Tactic:
have _ := Fintype.ofFinite α
Proof state after:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
x✝ : Fintype α
⊢ card (Option α) = card α + 1
Theorem: PartENat.card_option
Proof state before:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
x✝ : Fintype α
⊢ card (Option α) = card α + 1
Tactic:
simp
Proof state after:
no goals
Theorem: encard_iUnion
Proof 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
Proof 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
Theorem: encard_iUnion
Proof 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
Proof 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
Theorem: encard_iUnion
Proof 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]
Proof 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
Theorem: encard_iUnion
Proof 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]
Proof 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
Theorem: encard_iUnion
Proof 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) ?_
Proof 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)
Theorem: encard_iUnion
Proof 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]
Proof 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)
Theorem: encard_iUnion
Proof 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
Proof state after:
no goals
Theorem: encard_iUnion
Proof 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]
Proof 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
Theorem: encard_iUnion
Proof 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})
Proof 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
Theorem: encard_iUnion
Proof 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
Proof 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
Theorem: encard_iUnion
Proof 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
Proof state after:
no goals
Theorem: encard_iUnion
Proof 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
Proof 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)
Theorem: encard_iUnion
Proof 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]
Proof state after:
no goals
Theorem: encard_iUnion
Proof 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
Proof 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
Theorem: encard_iUnion
Proof 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
Proof state after:
no goals
Theorem: encard_biUnion
Proof 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) ?_
Proof 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
Theorem: encard_biUnion
Proof 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
Proof 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⟩
Theorem: encard_biUnion
Proof 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
Proof state after:
no goals
Theorem: encard_biUnion
Proof 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
Proof 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
Theorem: encard_biUnion
Proof 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
Proof state after:
no goals
Theorem: encard_biUnion
Proof 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)]
Proof state after:
no goals
Theorem: encard_biUnion
Proof 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
Proof state after:
no goals
Theorem: encard_iUnion_le
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Tactic:
obtain (⟨i, hi⟩ | h) := em <| ∃ i, (s i).Infinite
Proof state after:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
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 α
h : ¬∃ i, (s i).Infinite
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Theorem: encard_iUnion_le
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ¬∃ i, (s i).Infinite
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Tactic:
simp_rw [not_exists, not_infinite] at h
Proof state after:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Theorem: encard_iUnion_le
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Tactic:
convert (Nat.cast_le (α := ℕ∞)).2
  (Finset.card_biUnion_le (s := Finset.univ) (t := fun i ↦ (h i).toFinset))
Proof state after:
case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard = ↑(Finset.univ.biUnion fun i => ⋯.toFinset).card

case h.e'_4
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ∑ i : ι, (s i).encard = ↑(∑ a : ι, ⋯.toFinset.card)
Theorem: encard_iUnion_le
Proof state before:
case h.e'_4
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ∑ i : ι, (s i).encard = ↑(∑ a : ι, ⋯.toFinset.card)
Tactic:
rw [Nat.cast_sum]
Proof state after:
case h.e'_4
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ∑ i : ι, (s i).encard = ∑ x : ι, ↑⋯.toFinset.card
Theorem: encard_iUnion_le
Proof state before:
case h.e'_4
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ∑ i : ι, (s i).encard = ∑ x : ι, ↑⋯.toFinset.card
Tactic:
exact Finset.sum_congr rfl (fun x _ ↦ (h x).encard_eq_coe_toFinset_card)
Proof state after:
no goals
Theorem: encard_iUnion_le
Proof state before:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
i : ι
hi : (s i).Infinite
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Tactic:
have hle := Finset.sum_le_sum_of_subset (f := fun i ↦ encard (s i)) (Finset.subset_univ {i})
Proof state after:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
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 ≤ ∑ i : ι, (s i).encard
Theorem: encard_iUnion_le
Proof state before:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
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 ≤ ∑ i : ι, (s i).encard
Tactic:
simp_rw [Finset.sum_singleton, hi.encard_eq] at hle
Proof state after:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
i : ι
hi : (s i).Infinite
hle : ⊤ ≤ ∑ x : ι, (s x).encard
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Theorem: encard_iUnion_le
Proof state before:
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
i : ι
hi : (s i).Infinite
hle : ⊤ ≤ ∑ x : ι, (s x).encard
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
Tactic:
exact le_top.trans hle
Proof state after:
no goals
Theorem: encard_iUnion_le
Proof state before:
case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard = ↑(Finset.univ.biUnion fun i => ⋯.toFinset).card
Tactic:
rw [(finite_iUnion h).encard_eq_coe_toFinset_card]
Proof state after:
case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ↑⋯.toFinset.card = ↑(Finset.univ.biUnion fun i => ⋯.toFinset).card
Theorem: encard_iUnion_le
Proof state before:
case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ↑⋯.toFinset.card = ↑(Finset.univ.biUnion fun i => ⋯.toFinset).card
Tactic:
congr
Proof state after:
case h.e'_3.e_a.e_s
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ⋯.toFinset = Finset.univ.biUnion fun i => ⋯.toFinset
Theorem: encard_iUnion_le
Proof state before:
case h.e'_3.e_a.e_s
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ⋯.toFinset = Finset.univ.biUnion fun i => ⋯.toFinset
Tactic:
ext x
Proof state after:
case h.e'_3.e_a.e_s.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ Finset.univ.biUnion fun i => ⋯.toFinset
Theorem: encard_iUnion_le
Proof state before:
case h.e'_3.e_a.e_s.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ Finset.univ.biUnion fun i => ⋯.toFinset
Tactic:
simp
Proof state after:
no goals