refactor(logic/basic): turn *_prop_of_* into congr lemma (#6406)

Alternative solution to the exists part of #6404.

src/category_theory/filtered.lean

@@ -176,8 +176,8 @@ begin
       by_cases hf : f = f',
       { subst hf,
         apply coeq_condition, },
-      { rw w' _ _ (by finish), }, },
-    { rw w' _ _ (by finish), }, },
+      { rw @w' _ _ mX mY f' (by simpa [hf ∘ eq.symm] using mf') }, },
+    { rw @w' _ _ mX' mY' f' (by finish), }, },
 end
 
 /--

src/combinatorics/composition.lean

@@ -288,8 +288,7 @@ begin
   have i_pos : (0 : ℕ) < i,
   { by_contradiction i_pos,
     push_neg at i_pos,
-    simp [nonpos_iff_eq_zero.mp i_pos, c.size_up_to_zero] at H,
-    exact nat.not_succ_le_zero j H },
+    revert H, simp [nonpos_iff_eq_zero.1 i_pos, c.size_up_to_zero] },
   let i₁ := (i : ℕ).pred,
   have i₁_lt_i : i₁ < i := nat.pred_lt (ne_of_gt i_pos),
   have i₁_succ : i₁.succ = i := nat.succ_pred_eq_of_pos i_pos,

src/data/multiset/pi.lean

@@ -106,7 +106,7 @@ lemma mem_pi (m : multiset α) (t : Πa, multiset (δ a)) :
 begin
   refine multiset.induction_on m (λ f, _) (λ a m ih f, _),
   { simpa using show f = pi.empty δ, by funext a ha; exact ha.elim },
-  simp, split,
+  simp only [mem_bind, exists_prop, mem_cons, pi_cons, mem_map], split,
   { rintro ⟨b, hb, f', hf', rfl⟩ a' ha',
     rw [ih] at hf',
     by_cases a' = a,

src/data/nat/basic.lean

@@ -113,6 +113,8 @@ instance nat.comm_cancel_monoid_with_zero : comm_cancel_monoid_with_zero ℕ :=
   mul_right_cancel_of_ne_zero := λ _ _ _ h1 h2, nat.eq_of_mul_eq_mul_right (nat.pos_of_ne_zero h1) h2,
   .. (infer_instance : comm_monoid_with_zero ℕ) }
 
+attribute [simp] nat.not_lt_zero
+
 /-!
 Inject some simple facts into the type class system.
 This `fact` should not be confused with the factorial function `nat.fact`!

src/data/set/intervals/basic.lean

@@ -1262,7 +1262,7 @@ lemma nonempty_Ico_sdiff {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) :
   nonempty ↥(Ico x (x + dx) \ Ico y (y + dy)) :=
 begin
   cases lt_or_le x y with h' h',
-  { use x, simp* },
+  { use x, simp [*, not_le.2 h'], },
   { use max x (x + dy), simp [*, le_refl] }
 end
 

src/data/vector2.lean

@@ -121,7 +121,7 @@ begin
   simp only [list.nodup_iff_nth_le_inj],
   split,
   { intros h i j hij,
-    cases i, cases j, simp [nth_eq_nth_le] at *, tauto },
+    cases i, cases j, ext, apply h, simpa },
   { intros h i j hi hj hij,
     have := @h ⟨i, hi⟩ ⟨j, hj⟩, simp [nth_eq_nth_le] at *, tauto }
 end

src/logic/basic.lean

@@ -928,26 +928,54 @@ theorem Exists.fst {p : b → Prop} : Exists p → b
 theorem Exists.snd {p : b → Prop} : ∀ h : Exists p, p h.fst
 | ⟨_, h⟩ := h
 
-@[simp] theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h :=
+theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h :=
 @forall_const (q h) p ⟨h⟩
 
-@[simp] theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃ h' : p, q h') ↔ q h :=
+theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃ h' : p, q h') ↔ q h :=
 @exists_const (q h) p ⟨h⟩
 
-@[simp] theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) :
+theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) :
   (∀ h' : p, q h') ↔ true :=
 iff_true_intro $ λ h, hn.elim h
 
-@[simp] theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬ p → ¬ (∃ h' : p, q h') :=
+theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬ p → ¬ (∃ h' : p, q h') :=
 mt Exists.fst
 
+@[congr] lemma exists_prop_congr {p p' : Prop} {q q' : p → Prop}
+  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : Exists q ↔ ∃ h : p', q' (hp.2 h) :=
+⟨λ ⟨_, _⟩, ⟨hp.1 ‹_›, (hq _).1 ‹_›⟩, λ ⟨_, _⟩, ⟨_, (hq _).2 ‹_›⟩⟩
+
+@[congr] lemma exists_prop_congr' {p p' : Prop} {q q' : p → Prop}
+  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : Exists q = ∃ h : p', q' (hp.2 h) :=
+propext (exists_prop_congr hq _)
+
+@[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.exists {α : Sort*} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x :=
 exists.elim h (λ x hx, ⟨x, and.left hx⟩)
 
 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₂
 
+@[congr] lemma forall_prop_congr {p p' : Prop} {q q' : p → Prop}
+  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) ↔ ∀ h : p', q' (hp.2 h) :=
+⟨λ h1 h2, (hq _).1 (h1 (hp.2 _)), λ h1 h2, (hq _).2 (h1 (hp.1 h2))⟩
+
+@[congr] lemma forall_prop_congr' {p p' : Prop} {q q' : p → Prop}
+  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
+propext (forall_prop_congr hq _)
+
+@[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
+
 @[simp] lemma exists_unique_iff_exists {α : Sort*} [subsingleton α] {p : α → Prop} :
   (∃! x, p x) ↔ ∃ x, p x :=
 ⟨λ h, h.exists, Exists.imp $ λ x hx, ⟨hx, λ y _, subsingleton.elim y x⟩⟩

src/measure_theory/outer_measure.lean

@@ -458,7 +458,8 @@ lemma is_caratheodory_sum {s : ℕ → set α} (h : ∀i, is_caratheodory (s i))
 | (nat.succ n) := begin
   simp [Union_lt_succ, range_succ],
   rw [measure_inter_union m _ (h n), is_caratheodory_sum],
-  intro a, simpa [range_succ] using λ h₁ i hi h₂, hd _ _ (ne_of_gt hi) ⟨h₁, h₂⟩
+  intro a,
+  simpa [range_succ] using λ (h₁ : a ∈ s n) i (hi : i < n) h₂, hd _ _ (ne_of_gt hi) ⟨h₁, h₂⟩
 end
 
 lemma is_caratheodory_Union_nat {s : ℕ → set α} (h : ∀i, is_caratheodory (s i))

src/testing/slim_check/gen.lean

@@ -153,7 +153,8 @@ def freq (xs : list (ℕ+ × gen α)) (pos : 0 < xs.length) : gen α :=
 let s := (xs.map (subtype.val ∘ prod.fst)).sum in
 have ha : 1 ≤ s, from
   (le_trans pos $
-    list.length_map (subtype.val ∘ prod.fst) xs ▸ (list.length_le_sum_of_one_le _ (λ i, by simp; intros h _; exact h))),
+    list.length_map (subtype.val ∘ prod.fst) xs ▸
+      (list.length_le_sum_of_one_le _ (λ i, by { simp, intros, assumption }))),
 have 0 ≤ s - 1, from nat.le_sub_right_of_add_le ha,
 uliftable.adapt_up gen.{0} gen.{u} (choose_nat 0 (s-1) this) $ λ i,
 freq_aux xs i.1 (by rcases i with ⟨i,h₀,h₁⟩; rwa nat.le_sub_right_iff_add_le at h₁; exact ha)