refactor(logic/is_empty): tag is_empty.forall_iff and `is_empty.exi…

…sts_iff` as `simp` (#14660)

We tag the lemmas `forall_iff` and `exists_iff` on empty types as `simp`. We remove `forall_pempty`, `exists_pempty`, `forall_false_left`, and `exists_false_left` due to being redundant.

src/algebra/associated.lean

@@ -173,7 +173,7 @@ theorem of_irreducible_pow {α} [monoid α] {x : α} {n : ℕ} (hn : n ≠ 1) :
   irreducible (x ^ n) → is_unit x :=
 begin
   obtain hn|hn := hn.lt_or_lt,
-  { simp only [nat.lt_one_iff.mp hn, forall_false_left, not_irreducible_one, pow_zero] },
+  { simp only [nat.lt_one_iff.mp hn, is_empty.forall_iff, not_irreducible_one, pow_zero] },
   intro h,
   obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_lt hn,
   rw [pow_succ, add_comm] at h,

src/analysis/locally_convex/basic.lean

@@ -78,7 +78,7 @@ begin
   classical,
   induction t using finset.induction_on with i t ht hi,
   { simp only [finset.not_mem_empty, set.Union_false, set.Union_empty, absorbs_empty,
-    forall_false_left, implies_true_iff] },
+      is_empty.forall_iff, implies_true_iff] },
   rw [finset.set_bUnion_insert, absorbs_union, hi],
   split; intro h,
   { refine λ _ hi', (finset.mem_insert.mp hi').elim _ (h.2 _),

src/data/list/cycle.lean

@@ -828,7 +828,7 @@ theorem chain_iff_pairwise (hr : transitive r) : chain r s ↔ ∀ (a ∈ s) (b
   intros hs b hb c hc,
   rw [cycle.chain_coe_cons, chain_iff_pairwise hr] at hs,
   simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, list.not_mem_nil,
-    forall_false_left, implies_true_iff, pairwise.nil, forall_eq, true_and] at hs,
+    is_empty.forall_iff, implies_true_iff, pairwise.nil, forall_eq, true_and] at hs,
   simp only [mem_coe_iff, mem_cons_iff] at hb hc,
   rcases hb with rfl | hb;
   rcases hc with rfl | hc,

src/data/nat/nth.lean

@@ -57,7 +57,7 @@ lemma nth_set_card_aux {n : ℕ} (hp : (set_of p).finite)
 begin
   unfreezingI { induction n with k hk },
   { congr,
-    simp only [forall_false_left, nat.not_lt_zero, forall_const, and_true] },
+    simp only [is_empty.forall_iff, nat.not_lt_zero, forall_const, and_true] },
   have hp'': {i : ℕ | p i ∧ ∀ t, t < k → nth p t < i}.finite,
   { refine hp.subset (λ x hx, _),
     rw set.mem_set_of_eq at hx,

src/data/polynomial/laurent.lean

@@ -291,7 +291,7 @@ begin
     ext a,
     have := ((not_le.mp n0).trans_le (int.coe_zero_le a)).ne',
     simp only [coeff, comap_domain_apply, int.of_nat_eq_coe, coeff_zero, single_apply_eq_zero, this,
-      forall_false_left] }
+      is_empty.forall_iff] }
 end
 
 @[simp] lemma left_inverse_trunc_to_laurent :

src/data/rbtree/basic.lean

@@ -3,8 +3,9 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import tactic.interactive
 import data.rbtree.init
+import logic.is_empty
+import tactic.interactive
 
 universe u
 

src/group_theory/subgroup/basic.lean

@@ -3189,7 +3189,7 @@ begin
     { simp only [int.coe_nat_eq_zero, int.of_nat_eq_coe, zpow_coe_nat] at hgn ⊢,
       exact hH hgn },
     { suffices : g ^ (n+1) ∈ H,
-      { refine (hH this).imp _ id, simp only [forall_false_left, nat.succ_ne_zero], },
+      { refine (hH this).imp _ id, simp only [is_empty.forall_iff, nat.succ_ne_zero], },
       simpa only [inv_mem_iff, zpow_neg_succ_of_nat] using hgn, } },
   { intros h n g hgn,
     specialize h n g,

src/logic/basic.lean

@@ -146,12 +146,6 @@ instance subsingleton_pempty : subsingleton pempty := ⟨λa, a.elim⟩
 @[simp] lemma not_nonempty_pempty : ¬ nonempty pempty :=
 assume ⟨h⟩, h.elim
 
-@[simp] theorem forall_pempty {P : pempty → Prop} : (∀ x : pempty, P x) ↔ true :=
-⟨λ h, trivial, λ h x, by cases x⟩
-
-@[simp] theorem exists_pempty {P : pempty → Prop} : (∃ x : pempty, P x) ↔ false :=
-⟨λ h, by { cases h with w, cases w }, false.elim⟩
-
 lemma congr_heq {α β γ : Sort*} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : f == g)
   (h₂ : x == y) : f x = g y :=
 by { cases h₂, cases h₁, refl }
@@ -1281,12 +1275,10 @@ mt Exists.fst
   (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : Exists q = ∃ h : p', q' (hp.2 h) :=
 propext (exists_prop_congr hq _)
 
+/-- See `is_empty.exists_iff` for the `false` version. -/
 @[simp] lemma exists_true_left (p : true → Prop) : (∃ x, p x) ↔ p true.intro :=
 exists_prop_of_true _
 
-@[simp] lemma exists_false_left (p : false → Prop) : ¬ ∃ x, p x :=
-exists_prop_of_false not_false
-
 lemma exists_unique.unique {α : Sort*} {p : α → Prop} (h : ∃! x, p x)
   {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
 unique_of_exists_unique h py₁ py₂
@@ -1299,12 +1291,10 @@ unique_of_exists_unique h py₁ py₂
   (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
 propext (forall_prop_congr hq _)
 
+/-- See `is_empty.forall_iff` for the `false` version. -/
 @[simp] lemma forall_true_left (p : true → Prop) : (∀ x, p x) ↔ p true.intro :=
 forall_prop_of_true _
 
-@[simp] lemma forall_false_left (p : false → Prop) : (∀ x, p x) ↔ true :=
-forall_prop_of_false not_false
-
 lemma exists_unique.elim2 {α : Sort*} {p : α → Sort*} [∀ x, subsingleton (p x)]
   {q : Π x (h : p x), Prop} {b : Prop} (h₂ : ∃! x (h : p x), q x h)
   (h₁ : ∀ x (h : p x), q x h → (∀ y (hy : p y), q y hy → y = x) → b) : b :=
@@ -1494,12 +1484,18 @@ section ite
 variables {α β γ : Sort*} {σ : α → Sort*} (f : α → β) {P Q : Prop} [decidable P] [decidable Q]
   {a b c : α} {A : P → α} {B : ¬ P → α}
 
-lemma dite_eq_iff : dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c := by by_cases P; simp *
+lemma dite_eq_iff : dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c :=
+by by_cases P; simp [*, exists_prop_of_false not_false]
+
 lemma ite_eq_iff : ite P a b = c ↔ P ∧ a = c ∨ ¬ P ∧ b = c :=
 dite_eq_iff.trans $ by rw [exists_prop, exists_prop]
 
-@[simp] lemma dite_eq_left_iff : dite P (λ _, a) B = a ↔ ∀ h, B h = a := by by_cases P; simp *
-@[simp] lemma dite_eq_right_iff : dite P A (λ _, b) = b ↔ ∀ h, A h = b := by by_cases P; simp *
+@[simp] lemma dite_eq_left_iff : dite P (λ _, a) B = a ↔ ∀ h, B h = a :=
+by by_cases P; simp [*, forall_prop_of_false not_false]
+
+@[simp] lemma dite_eq_right_iff : dite P A (λ _, b) = b ↔ ∀ h, A h = b :=
+by by_cases P; simp [*, forall_prop_of_false not_false]
+
 @[simp] lemma ite_eq_left_iff : ite P a b = a ↔ (¬ P → b = a) := dite_eq_left_iff
 @[simp] lemma ite_eq_right_iff : ite P a b = b ↔ (P → a = b) := dite_eq_right_iff
 

src/logic/is_empty.lean

@@ -84,10 +84,10 @@ is_empty_iff
 
 variables [is_empty α]
 
-lemma forall_iff {p : α → Prop} : (∀ a, p a) ↔ true :=
+@[simp] lemma forall_iff {p : α → Prop} : (∀ a, p a) ↔ true :=
 iff_true_intro is_empty_elim
 
-lemma exists_iff {p : α → Prop} : (∃ a, p a) ↔ false :=
+@[simp] lemma exists_iff {p : α → Prop} : (∃ a, p a) ↔ false :=
 iff_false_intro $ λ ⟨x, hx⟩, is_empty.false x
 
 @[priority 100] -- see Note [lower instance priority]

src/measure_theory/covering/besicovitch.lean

@@ -726,7 +726,7 @@ begin
   { assume n,
     induction n with n IH,
     { simp only [u, P, prod.forall, id.def, function.iterate_zero],
-      simp only [finset.not_mem_empty, forall_false_left, finset.coe_empty, forall_2_true_iff,
+      simp only [finset.not_mem_empty, is_empty.forall_iff, finset.coe_empty, forall_2_true_iff,
         and_self, pairwise_disjoint_empty] },
     { rw u_succ,
       exact (hF (u n) IH).2.1 } },

src/measure_theory/function/strongly_measurable.lean

@@ -650,7 +650,8 @@ begin
         simp only [hy, exists_true_left, not_true, and_false, or_false]},
       { rw dif_neg hy,
         have A : y ∈ t, by simpa [hy] using h (mem_univ y),
-        simp only [A, hy, false_or, exists_false_left, not_false_iff, and_true, exists_true_left] }
+        simp only [A, hy, false_or, is_empty.exists_iff, not_false_iff, and_true,
+          exists_true_left] }
     end,
     finite_range' :=
     begin

src/measure_theory/integral/set_to_l1.lean

@@ -156,7 +156,7 @@ lemma map_Union_fin_meas_set_eq_sum (T : set α → β) (T_empty : T ∅ = 0)
 begin
   revert hSp h_disj,
   refine finset.induction_on sι _ _,
-  { simp only [finset.not_mem_empty, forall_false_left, Union_false, Union_empty, sum_empty,
+  { simp only [finset.not_mem_empty, is_empty.forall_iff, Union_false, Union_empty, sum_empty,
     forall_2_true_iff, implies_true_iff, forall_true_left, not_false_iff, T_empty], },
   intros a s has h hps h_disj,
   rw [finset.sum_insert has, ← h],

src/order/filter/basic.lean

@@ -1901,7 +1901,7 @@ comap_fst_ne_bot_iff.2 ⟨‹_›, ‹_›⟩
 begin
   casesI is_empty_or_nonempty α with hα hα,
   { rw [filter_eq_bot_of_is_empty (f.comap _), ← not_iff_not];
-      [simpa using hα.elim, apply_instance] },
+      [simp, apply_instance] },
   { simp [comap_ne_bot_iff_frequently, hα] }
 end
 
@@ -1914,7 +1914,7 @@ lemma comap_eval_ne_bot_iff' {ι : Type*} {α : ι → Type*} {i : ι} {f : filt
 begin
   casesI is_empty_or_nonempty (Π j, α j) with H H,
   { rw [filter_eq_bot_of_is_empty (f.comap _), ← not_iff_not]; [skip, assumption],
-    simpa [← classical.nonempty_pi] using H.elim },
+    simp [← classical.nonempty_pi] },
   { haveI : ∀ j, nonempty (α j), from classical.nonempty_pi.1 H,
     simp [comap_ne_bot_iff_frequently, *] }
 end

src/order/partition/finpartition.lean

@@ -482,7 +482,7 @@ by simp only [atomise, of_erase, bot_eq_empty, mem_erase, mem_image, nonempty_if
 
 lemma atomise_empty (hs : s.nonempty) : (atomise s ∅).parts = {s} :=
 begin
-  simp only [atomise, powerset_empty, image_singleton, not_mem_empty, forall_false_left,
+  simp only [atomise, powerset_empty, image_singleton, not_mem_empty, is_empty.forall_iff,
     implies_true_iff, filter_true],
   exact erase_eq_of_not_mem (not_mem_singleton.2 hs.ne_empty.symm),
 end

src/order/well_founded_set.lean

@@ -893,7 +893,7 @@ begin
   { simpa only [forall_true_left, finset.mem_univ] using this finset.univ, },
   apply' finset.induction,
   { intros f hf, existsi rel_embedding.refl (≤),
-    simp only [forall_false_left, implies_true_iff, forall_const, finset.not_mem_empty], },
+    simp only [is_empty.forall_iff, implies_true_iff, forall_const, finset.not_mem_empty], },
   { intros x s hx ih f hf,
     obtain ⟨g, hg⟩ := (is_well_order.wf.is_wf (set.univ : set _)).is_pwo.exists_monotone_subseq
       ((λ mo : Π s : σ, α s, mo x) ∘ f) (set.subset_univ _),

src/probability/hitting_time.lean

@@ -58,7 +58,7 @@ begin
   { push_neg,
     intro j,
     rw set.Icc_eq_empty_of_lt h,
-    simp only [set.mem_empty_eq, forall_false_left], },
+    simp only [set.mem_empty_eq, is_empty.forall_iff], },
   simp only [h_not, if_false],
 end