internlm/Lean-Github huggingface dataset:
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard ↔ univ.PairwiseDisjoint s
Tactic:
refine ⟨fun hsum i _ j _ hij ↦ disjoint_iff_forall_ne.2 ?_, fun hdj ↦ encard_iUnion s hdj⟩
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ s i → ∀ ⦃b : α⦄, b ∈ s j → a ≠ b
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ s i → ∀ ⦃b : α⦄, b ∈ s j → a ≠ b
Tactic:
rintro x hxi _ hxj rfl
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
⊢ False
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
⊢ False
Tactic:
have hrw : ∀ t : Set α, encard t = encard (t \ {x}) + encard (t ∩ {x}) := by
  intro t
  rw [← encard_union_eq, diff_union_inter]
  exact disjoint_sdiff_left.mono_right inter_subset_right
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
⊢ False
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
⊢ False
Tactic:
rw [hrw, Finset.sum_congr rfl (fun i _ ↦ hrw (s i)), Finset.sum_add_distrib,
  inter_eq_self_of_subset_right (singleton_subset_iff.2 (mem_iUnion_of_mem i hxi)),
  encard_singleton, eq_comm, iUnion_diff] at hsum
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
⊢ False
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
⊢ False
Tactic:
have hlb := Finset.sum_le_sum_of_subset
  (f := fun i ↦ (s i ∩ {x}).encard) (Finset.subset_univ {i,j})
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : ∑ x_1 ∈ {i, j}, (fun i => (s i ∩ {x}).encard) x_1 ≤ ∑ x_1 : ι, (fun i => (s i ∩ {x}).encard) x_1
⊢ False
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : ∑ x_1 ∈ {i, j}, (fun i => (s i ∩ {x}).encard) x_1 ≤ ∑ x_1 : ι, (fun i => (s i ∩ {x}).encard) x_1
⊢ False
Tactic:
simp_rw [Finset.sum_pair hij] at hlb
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : (s i ∩ {x}).encard + (s j ∩ {x}).encard ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ False
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : (s i ∩ {x}).encard + (s j ∩ {x}).encard ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ False
Tactic:
rw [inter_eq_self_of_subset_right (by simpa), inter_eq_self_of_subset_right (by simpa),
  encard_singleton] at hlb
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ False
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ False
Tactic:
have hcon := ((add_le_add_left hlb _).trans hsum.le).trans
  (add_le_add_right (encard_iUnion_le _) 1)
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + (1 + 1) ≤ ∑ i : ι, (s i \ {x}).encard + 1
⊢ False
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + (1 + 1) ≤ ∑ i : ι, (s i \ {x}).encard + 1
⊢ False
Tactic:
rw [← add_assoc, WithTop.add_le_add_iff_right (by simp), ENat.add_one_le_iff] at hcon
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard < ∑ i : ι, (s i \ {x}).encard
⊢ False

α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
⊢ ∑ x_1 : ι, (s x_1 \ {x}).encard ≠ ⊤
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
⊢ ∑ x_1 : ι, (s x_1 \ {x}).encard ≠ ⊤
Tactic:
refine (WithTop.sum_lt_top (fun i _ ↦ ?_)).ne
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i✝ : ι
x✝² : i✝ ∈ univ
j : ι
x✝¹ : j ∈ univ
hij : i✝ ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i✝
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
i : ι
x✝ : i ∈ Finset.univ
⊢ (s i \ {x}).encard ≠ ⊤
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i✝ : ι
x✝² : i✝ ∈ univ
j : ι
x✝¹ : j ∈ univ
hij : i✝ ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i✝
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
i : ι
x✝ : i ∈ Finset.univ
⊢ (s i \ {x}).encard ≠ ⊤
Tactic:
rw [encard_ne_top_iff]
Proof state after:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i✝ : ι
x✝² : i✝ ∈ univ
j : ι
x✝¹ : j ∈ univ
hij : i✝ ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i✝
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
i : ι
x✝ : i ∈ Finset.univ
⊢ (s i \ {x}).Finite
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i✝ : ι
x✝² : i✝ ∈ univ
j : ι
x✝¹ : j ∈ univ
hij : i✝ ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i✝
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
i : ι
x✝ : i ∈ Finset.univ
⊢ (s i \ {x}).Finite
Tactic:
exact (hfin i).diff _
Proof state after:
no goals
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
⊢ ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
Tactic:
intro t
Proof state after:
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
t : Set α
⊢ t.encard = (t \ {x}).encard + (t ∩ {x}).encard
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
t : Set α
⊢ t.encard = (t \ {x}).encard + (t ∩ {x}).encard
Tactic:
rw [← encard_union_eq, diff_union_inter]
Proof state after:
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
t : Set α
⊢ Disjoint (t \ {x}) (t ∩ {x})
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hxi : x ∈ s i
hxj : x ∈ s j
t : Set α
⊢ Disjoint (t \ {x}) (t ∩ {x})
Tactic:
exact disjoint_sdiff_left.mono_right inter_subset_right
Proof state after:
no goals
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : (s i ∩ {x}).encard + (s j ∩ {x}).encard ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ {x} ⊆ s i
Tactic:
simpa
Proof state after:
no goals
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : {x}.encard + (s j ∩ {x}).encard ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ {x} ⊆ s j
Tactic:
simpa
Proof state after:
no goals
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 + 1 ≤ ∑ i : ι, (s i \ {x}).encard + 1
⊢ 1 ≠ ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard < ∑ i : ι, (s i \ {x}).encard
⊢ False
Tactic:
exact hcon.ne rfl
Proof state after:
no goals
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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 ι), _) = _ ↔ _
Proof 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
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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]
Proof 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
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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)
Proof 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
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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 ↦ ?_⟩
Proof 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
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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)
Proof state after:
no goals
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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
Proof state after:
no goals
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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))]
Proof state after:
no goals
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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]
Proof state after:
no goals
Theorem: encard_biUnion_eq_sum_iff_pairwiseDisjoint
Proof 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
Proof state after:
no goals
Theorem: pairwiseDisjoint_of_encard_sum_le_encard_iUnion
Proof state before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hle : ∑ i : ι, (s i).encard ≤ (⋃ i, s i).encard
⊢ univ.PairwiseDisjoint s
Tactic:
rw [← encard_iUnion_eq_sum_iff_pairwiseDisjoint hfin, hle.antisymm (encard_iUnion_le s)]
Proof state after:
no goals
Theorem: ClMatroid.cl_subset_ground
Proof state before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
X : Set α
⊢ M.cl X ⊆ M.E
Tactic:
rw [← M.cl_inter_inter_ground]
Proof state after:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
X : Set α
⊢ M.cl (X ∩ M.E) ∩ M.E ⊆ M.E
Theorem: ClMatroid.cl_subset_ground
Proof state before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
X : Set α
⊢ M.cl (X ∩ M.E) ∩ M.E ⊆ M.E
Tactic:
apply inter_subset_right
Proof state after:
no goals
Theorem: ClMatroid.cl_inter_ground
Proof state before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
X : Set α
⊢ M.cl (X ∩ M.E) = M.cl X
Tactic:
rw [← inter_eq_self_of_subset_left (M.cl_subset_ground (X ∩ M.E)), M.cl_inter_inter_ground]
Proof state after:
no goals
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X : Set α
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
obtain ⟨I, hI⟩ := (M.matroidOnUniv hM).exists_basis X (by simp [hM])
Proof state after:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
have hi := hI.indep
Proof state after:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.matroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.matroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
simp [matroidOnUniv, M.clIndep_iff] at hi
Proof state after:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Theorem: ClMatroid.matroidOnUniv_cl_eq
Proof state before:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
refine subset_antisymm ?_ ?_
Proof state after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X ⊆ M.cl X

case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ M.cl X ⊆ (M.matroidOnUniv hM).cl X