chore(*): golf proofs about filter.Coprod (#10400)

Also add some supporting lemmas.

src/data/fintype/basic.lean

@@ -1198,6 +1198,10 @@ begin
     exact λ hf, ⟨λ a ha, f a, hf, rfl⟩ }
 end
 
+@[simp] lemma coe_pi_finset (t : Π a, finset (δ a)) :
+  (pi_finset t : set (Π a, δ a)) = set.pi set.univ (λ a, t a) :=
+by { ext, simp }
+
 lemma pi_finset_subset (t₁ t₂ : Π a, finset (δ a)) (h : ∀ a, t₁ a ⊆ t₂ a) :
   pi_finset t₁ ⊆ pi_finset t₂ :=
 λ g hg, mem_pi_finset.2 $ λ a, h a $ mem_pi_finset.1 hg a

src/data/pi.lean

@@ -140,9 +140,9 @@ function.update_injective _ i
 end
 end pi
 
-section extend
 namespace function
 
+section extend
 @[to_additive]
 lemma extend_one [has_one γ] (f : α → β) :
   function.extend f (1 : α → γ) (1 : β → γ) = 1 :=
@@ -163,9 +163,22 @@ lemma extend_div [has_div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂
   function.extend f (g₁ / g₂) (e₁ / e₂) = function.extend f g₁ e₁ / function.extend f g₂ e₂ :=
 funext $ λ _, by convert (apply_dite2 (/) _ _ _ _ _).symm
 
-end function
 end extend
 
+lemma surjective_pi_map {F : Π i, f i → g i} (hF : ∀ i, surjective (F i)) :
+  surjective (λ x : Π i, f i, λ i, F i (x i)) :=
+λ y, ⟨λ i, (hF i (y i)).some, funext $ λ i, (hF i (y i)).some_spec⟩
+
+lemma injective_pi_map {F : Π i, f i → g i} (hF : ∀ i, injective (F i)) :
+  injective (λ x : Π i, f i, λ i, F i (x i)) :=
+λ x y h, funext $ λ i, hF i $ (congr_fun h i : _)
+
+lemma bijective_pi_map {F : Π i, f i → g i} (hF : ∀ i, bijective (F i)) :
+  bijective (λ x : Π i, f i, λ i, F i (x i)) :=
+⟨injective_pi_map (λ i, (hF i).injective), surjective_pi_map (λ i, (hF i).surjective)⟩
+
+end function
+
 lemma subsingleton.pi_single_eq {α : Type*} [decidable_eq I] [subsingleton I] [has_zero α]
   (i : I) (x : α) :
   pi.single i x = λ _, x :=

src/data/set/finite.lean

@@ -573,10 +573,10 @@ lemma finite.pi {δ : Type*} [fintype δ] {κ : δ → Type*} {t : Π d, set (κ
   (ht : ∀ d, (t d).finite) :
   (pi univ t).finite :=
 begin
+  lift t to Π d, finset (κ d) using ht,
   classical,
-  convert (fintype.pi_finset (λ d, (ht d).to_finset)).finite_to_set,
-  ext,
-  simp,
+  rw ← fintype.coe_pi_finset,
+  exact (fintype.pi_finset t).finite_to_set,
 end
 
 /-- A finite union of finsets is finite. -/

src/order/boolean_algebra.lean

@@ -628,6 +628,9 @@ is_compl_compl.symm.compl_eq
 theorem compl_bijective : function.bijective (compl : α → α) :=
 compl_involutive.bijective
 
+theorem compl_surjective : function.surjective (compl : α → α) :=
+compl_involutive.surjective
+
 theorem compl_injective : function.injective (compl : α → α) :=
 compl_involutive.injective
 

src/order/filter/basic.lean

@@ -1079,12 +1079,8 @@ lemma frequently_iff_forall_eventually_exists_and {p : α → Prop} {f : filter
 lemma frequently_iff {f : filter α} {P : α → Prop} :
   (∃ᶠ x in f, P x) ↔ ∀ {U}, U ∈ f → ∃ x ∈ U, P x :=
 begin
-  rw frequently_iff_forall_eventually_exists_and,
-  split ; intro h,
-  { intros U U_in,
-    simpa [exists_prop, and_comm] using h U_in },
-  { intros H H',
-    simpa [and_comm] using h H' },
+  simp only [frequently_iff_forall_eventually_exists_and, exists_prop, and_comm (P _)],
+  refl
 end
 
 @[simp] lemma not_eventually {p : α → Prop} {f : filter α} :
@@ -2735,6 +2731,14 @@ lemma mem_Coprod_iff {s : set (Π d, κ d)} {f : Π d, filter (κ d)} :
   (s ∈ (filter.Coprod f)) ↔ (∀ d : δ, (∃ t₁ ∈ f d, (λ k : (Π d, κ d), k d) ⁻¹' t₁ ⊆ s)) :=
 by simp [filter.Coprod]
 
+lemma compl_mem_Coprod_iff {s : set (Π d, κ d)} {f : Π d, filter (κ d)} :
+  sᶜ ∈ filter.Coprod f ↔ ∃ t : Π d, set (κ d), (∀ d, (t d)ᶜ ∈ f d) ∧ s ⊆ set.pi univ t :=
+begin
+  rw [(surjective_pi_map (λ d, @compl_surjective (set (κ d)) _)).exists],
+  simp_rw [mem_Coprod_iff, classical.skolem, exists_prop, @subset_compl_comm _ _ s,
+    ← preimage_compl, ← subset_Inter_iff, ← univ_pi_eq_Inter, compl_compl]
+end
+
 lemma Coprod_ne_bot_iff' {f : Π d, filter (κ d)} :
   ne_bot (filter.Coprod f) ↔ (∀ d, nonempty (κ d)) ∧ ∃ d, ne_bot (f d) :=
 by simp only [filter.Coprod, supr_ne_bot, ← exists_and_distrib_left, ← comap_eval_ne_bot_iff']

src/order/filter/cofinite.lean

@@ -71,29 +71,12 @@ lemma Coprod_cofinite {δ : Type*} {κ : δ → Type*} [fintype δ] :
   filter.Coprod (λ d, (cofinite : filter (κ d))) = cofinite :=
 begin
   ext S,
-  simp only [mem_coprod_iff, exists_prop, mem_comap, mem_cofinite],
+  rcases compl_surjective S with ⟨S, rfl⟩,
+  simp_rw [compl_mem_Coprod_iff, mem_cofinite, compl_compl],
   split,
-  { rintros h,
-    rw mem_Coprod_iff at h,
-    choose t ht1 ht2 using h,
-    have ht1d : ∀ (d : δ), (t d)ᶜ.finite := λ d, mem_cofinite.mp (ht1 d),
-    refine (set.finite.pi ht1d).subset _,
-    have ht2d : ∀ (d : δ), Sᶜ ⊆ ((λ (k : Π (d1 : δ), (λ (d2 : δ), κ d2) d1), k d) ⁻¹' ((t d)ᶜ)) :=
-     λ d, compl_subset_compl.mpr (ht2 d),
-    convert set.subset_Inter ht2d,
-    ext,
-    simp },
-  { intro hS,
-    rw mem_Coprod_iff,
-    intros d,
-    refine ⟨((λ (k : Π (d1 : δ), κ d1), k d) '' (Sᶜ))ᶜ, _, _⟩,
-    { rw [mem_cofinite, compl_compl],
-      exact set.finite.image _ hS },
-    { intros x,
-      contrapose,
-      intros hx,
-      simp only [not_not, mem_preimage, mem_compl_eq, not_forall],
-      exact ⟨x, hx, rfl⟩ } },
+  { rintro ⟨t, htf, hsub⟩,
+    exact (finite.pi htf).subset hsub },
+  { exact λ hS, ⟨λ i, function.eval i '' S, λ i, hS.image _, subset_pi_eval_image _ _⟩ }
 end
 
 end filter

src/topology/subset_properties.lean

@@ -880,33 +880,14 @@ instance pi.compact_space [∀ i, compact_space (π i)] : compact_space (Πi, π
 lemma filter.Coprod_cocompact {δ : Type*} {κ : δ → Type*} [Π d, topological_space (κ d)] :
   filter.Coprod (λ d, filter.cocompact (κ d)) = filter.cocompact (Π d, κ d) :=
 begin
-  ext S,
-  simp only [mem_coprod_iff, exists_prop, mem_comap, filter.mem_cocompact],
+  ext S, rcases compl_surjective S with ⟨S, rfl⟩,
+  simp_rw [compl_mem_Coprod_iff, filter.mem_cocompact, compl_subset_compl],
   split,
-  { intros h,
-    rw filter.mem_Coprod_iff at h,
-    choose t ht1 ht2 using h,
-    choose t1 ht11 ht12 using λ d, filter.mem_cocompact.mp (ht1 d),
-    refine ⟨set.pi set.univ t1, _, _⟩,
-    { convert is_compact_pi_infinite ht11,
-      ext,
-      simp },
-    { refine subset.trans _ (set.Union_subset ht2),
-      intros x,
-      simp only [mem_Union, mem_univ_pi, exists_imp_distrib, mem_compl_eq, not_forall],
-      intros d h,
-      exact ⟨d, ht12 d h⟩ } },
-  { rintros ⟨t, h1, h2⟩,
-    rw filter.mem_Coprod_iff,
-    intros d,
-    refine ⟨((λ (k : Π (d : δ), κ d), k d) '' t)ᶜ, _, _⟩,
-    { rw filter.mem_cocompact,
-      refine ⟨(λ (k : Π (d : δ), κ d), k d) '' t, _, set.subset.refl _⟩,
-      exact is_compact.image h1 (continuous_pi_iff.mp (continuous_id) d) },
-    refine subset.trans _ h2,
-    intros x hx,
-    simp only [not_exists, mem_image, mem_preimage, mem_compl_eq] at hx,
-    simpa using mt (hx x) },
+  { rintro ⟨t, H, hSt⟩, choose K hKc htK using H,
+    exact ⟨set.pi univ K, is_compact_univ_pi hKc, hSt.trans $ pi_mono $ λ i _, htK i⟩ },
+  { rintro ⟨K, hKc, hSK⟩,
+    exact ⟨λ i, function.eval i '' K, λ i, ⟨_, hKc.image (continuous_apply i), subset.rfl⟩,
+      hSK.trans $ subset_pi_eval_image _ _⟩ }
 end
 
 end tychonoff