From ade60278d0003bef577f642b8917f2c9f1ba65eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jul 2015 05:28:53 -0400 Subject: [PATCH] refactor(library): rename iff.mp' to iff.mpr --- library/algebra/order.lean | 8 ++++---- library/algebra/ordered_field.lean | 10 +++++----- library/algebra/ordered_group.lean | 6 +++--- library/algebra/ordered_ring.lean | 10 +++++----- library/data/finset/basic.lean | 2 +- library/data/int/div.lean | 6 +++--- library/data/int/order.lean | 14 +++++++------- library/data/list/basic.lean | 4 ++-- library/data/list/perm.lean | 6 +++--- library/data/nat/parity.lean | 4 ++-- library/data/pnat.lean | 8 ++++---- library/data/rat/basic.lean | 4 ++-- library/data/rat/order.lean | 16 ++++++++-------- library/data/real/basic.lean | 4 ++-- library/data/real/order.lean | 16 ++++++++-------- library/data/set/function.lean | 4 ++-- library/init/logic.lean | 14 +++++++------- library/logic/connectives.lean | 2 +- library/logic/quantifiers.lean | 4 ++-- library/theories/number_theory/primes.lean | 2 +- 20 files changed, 72 insertions(+), 72 deletions(-) diff --git a/library/algebra/order.lean b/library/algebra/order.lean index e549024cc..3130c7fc3 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -252,7 +252,7 @@ theorem lt_or_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a iff.mp le_iff_lt_or_eq le_ab theorem le_of_lt_or_eq [s : strong_order_pair A] {a b : A} (lt_or_eq : a < b ∨ a = b) : a ≤ b := -iff.mp' le_iff_lt_or_eq lt_or_eq +iff.mpr le_iff_lt_or_eq lt_or_eq private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a := !strong_order_pair.lt_irrefl @@ -268,7 +268,7 @@ iff.intro or_resolve_left Hor (and.right Hand)) theorem lt_of_le_of_ne [s : strong_order_pair A] {a b : A} : a ≤ b → a ≠ b → a < b := -take H1 H2, iff.mp' lt_iff_le_and_ne (and.intro H1 H2) +take H1 H2, iff.mpr lt_iff_le_and_ne (and.intro H1 H2) private theorem ne_of_lt' [s : strong_order_pair A] {a b : A} (H : a < b) : a ≠ b := and.right ((iff.mp lt_iff_le_and_ne) H) @@ -282,7 +282,7 @@ have ne_ac : a ≠ c, from have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, have eq_ab : a = b, from le.antisymm (le_of_lt' _ _ lt_ab) le_ba, show false, from ne_of_lt' lt_ab eq_ab, -show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac) +show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac) theorem lt_of_le_of_lt' [s : strong_order_pair A] (a b c : A) : a ≤ b → b < c → a < c := assume le_ab : a ≤ b, @@ -293,7 +293,7 @@ have ne_ac : a ≠ c, from have le_cb : c ≤ b, from eq_ac ▸ le_ab, have eq_bc : b = c, from le.antisymm (le_of_lt' _ _ lt_bc) le_cb, show false, from ne_of_lt' lt_bc eq_bc, -show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac) +show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac) definition strong_order_pair.to_order_pair [trans-instance] [coercion] [reducible] [s : strong_order_pair A] : order_pair A := diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index eef06d60e..4a6672a9e 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -64,7 +64,7 @@ section linear_ordered_field (iff.mp (one_le_div_iff_le Hb)) H theorem one_le_div_of_le (Hb : b > 0) (H : b ≤ a) : 1 ≤ a / b := - (iff.mp' (one_le_div_iff_le Hb)) H + (iff.mpr (one_le_div_iff_le Hb)) H theorem one_lt_div_iff_lt (Hb : b > 0) : 1 < a / b ↔ b < a := have Hb' : b ≠ 0, from ne.symm (ne_of_lt Hb), @@ -83,7 +83,7 @@ section linear_ordered_field (iff.mp (one_lt_div_iff_lt Hb)) H theorem one_lt_div_of_lt (Hb : b > 0) (H : b < a) : 1 < a / b := - (iff.mp' (one_lt_div_iff_lt Hb)) H + (iff.mpr (one_lt_div_iff_lt Hb)) H theorem exists_lt : ∃ x, x < a := have H : a - 1 < a, from add_lt_of_le_of_neg (le.refl _) zero_gt_neg_one, @@ -296,7 +296,7 @@ theorem nonneg_le_nonneg_of_squares_le (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a end theorem div_two : (a + a) / 2 = a := - symm (iff.mp' (eq_div_iff_mul_eq (ne_of_gt (add_pos zero_lt_one zero_lt_one))) + symm (iff.mpr (eq_div_iff_mul_eq (ne_of_gt (add_pos zero_lt_one zero_lt_one))) (by rewrite [left_distrib, *mul_one])) @@ -434,7 +434,7 @@ section discrete_linear_ordered_field rewrite -mul_sub_left_distrib, apply mul_neg_of_pos_of_neg, exact Hc, - apply iff.mp' (sub_neg_iff_lt _ _), + apply iff.mpr (sub_neg_iff_lt _ _), apply div_lt_div_of_lt, exact Hb, exact H end @@ -457,7 +457,7 @@ section discrete_linear_ordered_field ... ≥ b - c : sub_le_of_nonneg _ _ (le.trans !abs_nonneg H)) else (have Habs : b - a ≤ c, by rewrite [abs_of_neg (lt_of_not_ge Hz) at H, neg_sub at H]; apply H, - have Habs' : b ≤ c + a, from (iff.mp' !le_add_iff_sub_right_le) Habs, + have Habs' : b ≤ c + a, from (iff.mpr !le_add_iff_sub_right_le) Habs, (iff.mp !le_add_iff_sub_left_le) Habs') theorem ge_sub_of_abs_sub_le_right (H : abs (a - b) ≤ c) : b ≥ a - c := diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 13f6296da..994e9787b 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -439,7 +439,7 @@ section assume H₂ : d ≤ a + c, have H : d - a ≤ min b c, from le_min (iff.mp !le_add_iff_sub_left_le H₁) (iff.mp !le_add_iff_sub_left_le H₂), - show d ≤ a + min b c, from iff.mp' !le_add_iff_sub_left_le H)) + show d ≤ a + min b c, from iff.mpr !le_add_iff_sub_left_le H)) theorem min_add_add_right : min (a + c) (b + c) = min a b + c := by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply min_add_add_left @@ -451,7 +451,7 @@ section (λ d H₁ H₂, have H : max b c ≤ d - a, from max_le (iff.mp !add_le_iff_le_sub_left H₁) (iff.mp !add_le_iff_le_sub_left H₂), - show a + max b c ≤ d, from iff.mp' !add_le_iff_le_sub_left H)) + show a + max b c ≤ d, from iff.mpr !add_le_iff_le_sub_left H)) theorem max_add_add_right : max (a + c) (b + c) = max a b + c := by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply max_add_add_left @@ -630,7 +630,7 @@ section (assume H2 : 0 ≤ a + b, aux2 H2) (assume H2 : a + b ≤ 0, assert H3 : -a + -b = -(a + b), by rewrite neg_add, - assert H4 : -(a + b) ≥ 0, from iff.mp' (neg_nonneg_iff_nonpos (a+b)) H2, + assert H4 : -(a + b) ≥ 0, from iff.mpr (neg_nonneg_iff_nonpos (a+b)) H2, have H5 : -a + -b ≥ 0, begin rewrite -H3 at H4, exact H4 end, calc abs (a + b) = abs (-a + -b) : by rewrite [-abs_neg, neg_add] diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index f14ac8f8b..80cf0ccb5 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -249,7 +249,7 @@ section include s theorem mul_le_mul_of_nonpos_left (H : b ≤ a) (Hc : c ≤ 0) : c * a ≤ c * b := - have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc, + have Hc' : -c ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos Hc, assert H1 : -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left H Hc', have H2 : -(c * b) ≤ -(c * a), begin @@ -259,7 +259,7 @@ section iff.mp !neg_le_neg_iff_le H2 theorem mul_le_mul_of_nonpos_right (H : b ≤ a) (Hc : c ≤ 0) : a * c ≤ b * c := - have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc, + have Hc' : -c ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos Hc, assert H1 : b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right H Hc', have H2 : -(b * c) ≤ -(a * c), begin @@ -276,7 +276,7 @@ section end theorem mul_lt_mul_of_neg_left (H : b < a) (Hc : c < 0) : c * a < c * b := - have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc, + have Hc' : -c > 0, from iff.mpr !neg_pos_iff_neg Hc, assert H1 : -c * b < -c * a, from mul_lt_mul_of_pos_left H Hc', have H2 : -(c * b) < -(c * a), begin @@ -286,7 +286,7 @@ section iff.mp !neg_lt_neg_iff_lt H2 theorem mul_lt_mul_of_neg_right (H : b < a) (Hc : c < 0) : a * c < b * c := - have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc, + have Hc' : -c > 0, from iff.mpr !neg_pos_iff_neg Hc, assert H1 : b * -c < a * -c, from mul_lt_mul_of_pos_right H Hc', have H2 : -(b * c) < -(a * c), begin @@ -413,7 +413,7 @@ section theorem gt_of_mul_lt_mul_neg_left {a b c : A} (H : c * a < c * b) (Hc : c ≤ 0) : a > b := have nhc : -c ≥ 0, from neg_nonneg_of_nonpos Hc, - have H2 : -(c * b) < -(c * a), from iff.mp' (neg_lt_neg_iff_lt _ _) H, + have H2 : -(c * b) < -(c * a), from iff.mpr (neg_lt_neg_iff_lt _ _) H, have H3 : (-c) * b < (-c) * a, from calc (-c) * b = - (c * b) : neg_mul_eq_neg_mul ... < -(c * a) : H2 diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index 88b80d5c7..87dc7b029 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -123,7 +123,7 @@ theorem not_mem_empty [rewrite] (a : A) : a ∉ ∅ := λ aine : a ∈ ∅, aine theorem mem_empty_iff [rewrite] (x : A) : x ∈ ∅ ↔ false := -iff.mp' !iff_false_iff_not !not_mem_empty +iff.mpr !iff_false_iff_not !not_mem_empty theorem mem_empty_eq (x : A) : x ∈ ∅ = false := propext !mem_empty_iff diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 6f533b054..0ce97ca31 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -304,7 +304,7 @@ have H2 : a mod (abs b) ≥ 0, from calc -[1+m] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 ... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] - ... ≥ 0 : iff.mp' !sub_nonneg_iff_le H3), + ... ≥ 0 : iff.mpr !sub_nonneg_iff_le H3), !mod_abs ▸ H2 theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b < (abs b) := @@ -419,7 +419,7 @@ by rewrite [↑modulo, !mul_div_mul_of_pos H, mul_sub_left_distrib, mul.left_com theorem lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : b > 0) : a < (a div b + 1) * b := have H : a - a div b * b < b, from !mod_lt_of_pos H, calc - a < a div b * b + b : iff.mp' !lt_add_iff_sub_lt_left H + a < a div b * b + b : iff.mpr !lt_add_iff_sub_lt_left H ... = (a div b + 1) * b : by rewrite [mul.right_distrib, one_mul] theorem div_le_of_nonneg_of_nonneg {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) : a div b ≤ a := @@ -488,7 +488,7 @@ nat.by_cases_zero_pos n theorem of_nat_dvd_of_nat_of_dvd {m n : ℕ} (H : #nat m ∣ n) : of_nat m ∣ of_nat n := nat.dvd.elim H (take k, assume H1 : #nat n = m * k, - dvd.intro (!iff.mp' !of_nat_eq_of_nat H1⁻¹)) + dvd.intro (!iff.mpr !of_nat_eq_of_nat H1⁻¹)) theorem of_nat_dvd_of_nat (m n : ℕ) : of_nat m ∣ of_nat n ↔ (#nat m ∣ n) := iff.intro dvd_of_of_nat_dvd_of_nat of_nat_dvd_of_nat_of_dvd diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 617ddc8b0..1f82124cb 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -40,7 +40,7 @@ show nonneg (b - a), from H1⁻¹ ▸ H2 theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b := obtain (n : ℕ) (H1 : b - a = n), from nonneg.elim H, -exists.intro n (!add.comm ▸ iff.mp' !add_eq_iff_eq_add_neg (H1⁻¹)) +exists.intro n (!add.comm ▸ iff.mpr !add_eq_iff_eq_add_neg (H1⁻¹)) theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a := or.elim (nonneg_or_nonneg_neg (b - a)) @@ -91,7 +91,7 @@ theorem lt_of_of_nat_lt_of_nat {m n : ℕ} (H : of_nat m < of_nat n) : #nat m < iff.mp !of_nat_lt_of_nat H theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : #nat m < n) : of_nat m < of_nat n := -iff.mp' !of_nat_lt_of_nat H +iff.mpr !of_nat_lt_of_nat H /- show that the integers form an ordered additive group -/ @@ -186,7 +186,7 @@ le.intro H2 theorem add_lt_add_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b := let H' := le_of_lt H in -(iff.mp' (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _) +(iff.mpr (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _) (take Heq, let Heq' := add_left_cancel Heq in !lt.irrefl (Heq' ▸ H))) @@ -228,13 +228,13 @@ theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a := theorem lt_of_lt_of_le {a b c : ℤ} (Hab : a < b) (Hbc : b ≤ c) : a < c := let Hab' := le_of_lt Hab in let Hac := le.trans Hab' Hbc in - (iff.mp' !lt_iff_le_and_ne) (and.intro Hac + (iff.mpr !lt_iff_le_and_ne) (and.intro Hac (assume Heq, not_le_of_gt (Heq ▸ Hab) Hbc)) theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c := let Hbc' := le_of_lt Hbc in let Hac := le.trans Hab Hbc' in - (iff.mp' !lt_iff_le_and_ne) (and.intro Hac + (iff.mpr !lt_iff_le_and_ne) (and.intro Hac (assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) section migrate_algebra @@ -308,7 +308,7 @@ obtain (n : ℕ) (H1 : 0 + of_nat n = a), from le.elim H, exists.intro n (!zero_add ▸ (H1⁻¹)) theorem exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -(of_nat n) := -have H2 : -a ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H, +have H2 : -a ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H, obtain (n : ℕ) (Hn : -a = of_nat n), from exists_eq_of_nat H2, exists.intro n (eq_neg_of_eq_neg (Hn⁻¹)) @@ -317,7 +317,7 @@ obtain (n : ℕ) (Hn : a = of_nat n), from exists_eq_of_nat H, Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n) theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : of_nat (nat_abs a) = -a := -have H1 : (-a) ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H, +have H1 : (-a) ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H, calc of_nat (nat_abs a) = of_nat (nat_abs (-a)) : nat_abs_neg ... = -a : of_nat_nat_abs_of_nonneg H1 diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 591b90ad0..27adc5e90 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -368,10 +368,10 @@ theorem cons_sub_cons {l₁ l₂ : list T} (a : T) (s : l₁ ⊆ l₂) : (a::l (λ i : b ∈ l₁, or.inr (s i)) theorem sub_append_left [rewrite] (l₁ l₂ : list T) : l₁ ⊆ l₁++l₂ := -λ b i, iff.mp' (mem_append_iff b l₁ l₂) (or.inl i) +λ b i, iff.mpr (mem_append_iff b l₁ l₂) (or.inl i) theorem sub_append_right [rewrite] (l₁ l₂ : list T) : l₂ ⊆ l₁++l₂ := -λ b i, iff.mp' (mem_append_iff b l₁ l₂) (or.inr i) +λ b i, iff.mpr (mem_append_iff b l₁ l₂) (or.inr i) theorem sub_cons_of_sub (a : T) {l₁ l₂ : list T} : l₁ ⊆ l₂ → l₁ ⊆ (a::l₂) := λ (s : l₁ ⊆ l₂) (x : T) (i : x ∈ l₁), or.inr (s i) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 190b44274..2ed44bdd1 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -685,7 +685,7 @@ open eq.ops theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a, a ∈ l₁ ↔ a ∈ l₂) → l₁ ~ l₂ | [] [] d₁ d₂ e := !perm.nil -| [] (a₂::t₂) d₁ d₂ e := absurd (iff.mp' (e a₂) !mem_cons) (not_mem_nil a₂) +| [] (a₂::t₂) d₁ d₂ e := absurd (iff.mpr (e a₂) !mem_cons) (not_mem_nil a₂) | (a₁::t₁) [] d₁ d₂ e := absurd (iff.mp (e a₁) !mem_cons) (not_mem_nil a₁) | (a₁::t₁) (a₂::t₂) d₁ d₂ e := have a₁inl₂ : a₁ ∈ a₂::t₂, from iff.mp (e a₁) !mem_cons, @@ -711,13 +711,13 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a (λ ains₁s₂ : a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append ains₁s₂) (λ ains₁ : a ∈ s₁, have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁), - have aina₁t₁ : a ∈ a₁::t₁, from iff.mp' (e a) aina₂t₂, + have aina₁t₁ : a ∈ a₁::t₁, from iff.mpr (e a) aina₂t₂, or.elim (eq_or_mem_of_mem_cons aina₁t₁) (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₁) na₁s₁) (λ aint₁ : a ∈ t₁, aint₁)) (λ ains₂ : a ∈ s₂, have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)), - have aina₁t₁ : a ∈ a₁::t₁, from iff.mp' (e a) aina₂t₂, + have aina₁t₁ : a ∈ a₁::t₁, from iff.mpr (e a) aina₂t₂, or.elim (eq_or_mem_of_mem_cons aina₁t₁) (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₂) na₁s₂) (λ aint₁ : a ∈ t₁, aint₁))), diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean index d5803f3c9..6f8c3e64c 100644 --- a/library/data/nat/parity.lean +++ b/library/data/nat/parity.lean @@ -45,13 +45,13 @@ lemma odd_iff_not_even : ∀ n, odd n ↔ ¬ even n := λ n, !iff.refl lemma odd_of_not_even {n} : ¬ even n → odd n := -λ h, iff.mp' !odd_iff_not_even h +λ h, iff.mpr !odd_iff_not_even h lemma even_of_not_odd {n} : ¬ odd n → even n := λ h, not_not_elim (iff.mp (not_iff_not_of_iff !odd_iff_not_even) h) lemma not_odd_of_even {n} : even n → ¬ odd n := -λ h, iff.mp' (not_iff_not_of_iff !odd_iff_not_even) (not_not_intro h) +λ h, iff.mpr (not_iff_not_of_iff !odd_iff_not_even) (not_not_intro h) lemma not_even_of_odd {n} : odd n → ¬ even n := λ h, iff.mp !odd_iff_not_even h diff --git a/library/data/pnat.lean b/library/data/pnat.lean index b171b42a3..c06c5ef04 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -106,16 +106,16 @@ theorem pnat.to_rat_of_nat (n : ℕ+) : rat_of_pnat n = of_nat n~ := theorem rat_of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial theorem rat_of_pnat_ge_one (n : ℕ+) : rat_of_pnat n ≥ 1 := - pnat.rec_on n (λ m h, (iff.mp' !of_nat_le_of_nat) (succ_le_of_lt h)) + pnat.rec_on n (λ m h, (iff.mpr !of_nat_le_of_nat) (succ_le_of_lt h)) theorem rat_of_pnat_is_pos (n : ℕ+) : rat_of_pnat n > 0 := - pnat.rec_on n (λ m h, (iff.mp' !of_nat_pos) h) + pnat.rec_on n (λ m h, (iff.mpr !of_nat_pos) h) theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : m ≤ n) : of_nat m ≤ of_nat n := - (iff.mp' !of_nat_le_of_nat) H + (iff.mpr !of_nat_le_of_nat) H theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : m < n) : of_nat m < of_nat n := - (iff.mp' !of_nat_lt_of_nat) H + (iff.mpr !of_nat_lt_of_nat) H theorem rat_of_pnat_le_of_pnat_le {m n : ℕ+} (H : m ≤ n) : rat_of_pnat m ≤ rat_of_pnat n := begin diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 1c97bc994..409f874de 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -511,7 +511,7 @@ end migrate_algebra theorem eq_num_div_denom (a : ℚ) : a = num a / denom a := have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'), -iff.mp' (eq_div_iff_mul_eq H) (mul_denom a) +iff.mpr (eq_div_iff_mul_eq H) (mul_denom a) theorem of_nat_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b := decidable.by_cases @@ -523,7 +523,7 @@ decidable.by_cases int.dvd.elim H (take c, assume Hc : a = b * c, by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]), - iff.mp' (eq_div_iff_mul_eq bnz') H') + iff.mpr (eq_div_iff_mul_eq bnz') H') end rat diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index 6be4c4128..373e9cca0 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -181,7 +181,7 @@ theorem of_nat_pos (a : ℕ) : (of_nat a > 0) ↔ (#nat a > nat.zero) := !of_nat_lt_of_nat theorem of_nat_nonneg (a : ℕ) : (of_nat a ≥ 0) := -iff.mp' !of_nat_le_of_nat !nat.zero_le +iff.mpr !of_nat_le_of_nat !nat.zero_le theorem le.refl (a : ℚ) : a ≤ a := by rewrite [↑rat.le, sub_self]; apply nonneg_zero @@ -223,7 +223,7 @@ iff.intro (assume H : a ≤ b, decidable.by_cases (assume H1 : a = b, or.inr H1) - (assume H1 : a ≠ b, or.inl (iff.mp' !lt_iff_le_and_ne (and.intro H H1)))) + (assume H1 : a ≠ b, or.inl (iff.mpr !lt_iff_le_and_ne (and.intro H H1)))) (assume H : a < b ∨ a = b, or.elim H (assume H1 : a < b, and.left (iff.mp !lt_iff_le_and_ne H1)) @@ -251,7 +251,7 @@ have H : pos (a * b), from pos_mul (to_pos H1) (to_pos H2), definition decidable_lt [instance] : decidable_rel rat.lt := take a b, decidable_pos (b - a) -theorem le_of_lt (H : a < b) : a ≤ b := iff.mp' !le_iff_lt_or_eq (or.inl H) +theorem le_of_lt (H : a < b) : a ≤ b := iff.mpr !le_iff_lt_or_eq (or.inl H) theorem lt_irrefl (a : ℚ) : ¬ a < a := take Ha, @@ -266,20 +266,20 @@ theorem not_le_of_gt (H : a < b) : ¬ b ≤ a := theorem lt_of_lt_of_le (Hab : a < b) (Hbc : b ≤ c) : a < c := let Hab' := le_of_lt Hab in let Hac := le.trans Hab' Hbc in - (iff.mp' !lt_iff_le_and_ne) (and.intro Hac + (iff.mpr !lt_iff_le_and_ne) (and.intro Hac (assume Heq, not_le_of_gt (Heq ▸ Hab) Hbc)) theorem lt_of_le_of_lt (Hab : a ≤ b) (Hbc : b < c) : a < c := let Hbc' := le_of_lt Hbc in let Hac := le.trans Hab Hbc' in - (iff.mp' !lt_iff_le_and_ne) (and.intro Hac + (iff.mpr !lt_iff_le_and_ne) (and.intro Hac (assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) theorem zero_lt_one : (0 : ℚ) < 1 := trivial theorem add_lt_add_left (H : a < b) (c : ℚ) : c + a < c + b := let H' := le_of_lt H in -(iff.mp' (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _) +(iff.mpr (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _) (take Heq, let Heq' := add_left_cancel Heq in !lt_irrefl (Heq' ▸ H))) @@ -334,9 +334,9 @@ definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a)) theorem ubound_ge (a : ℚ) : of_nat (ubound a) ≥ a := have H : abs a * abs (of_int (denom a)) = abs (of_int (num a)), from !abs_mul ▸ !mul_denom ▸ rfl, have H'' : 1 ≤ abs (of_int (denom a)), begin - have J : of_int (denom a) > 0, from (iff.mp' !of_int_pos) !denom_pos, + have J : of_int (denom a) > 0, from (iff.mpr !of_int_pos) !denom_pos, rewrite (abs_of_pos J), - apply iff.mp' !of_int_le_of_int, + apply iff.mpr !of_int_le_of_int, apply denom_pos end, have H' : abs a ≤ abs (of_int (num a)), from diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 5c1b7fb7c..41e5e1ad9 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -31,7 +31,7 @@ theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c ∧ c > 0 have H3 [visible] : (a + a) / (1 + 1) > ((b + b) + (a - b)) / (1 + 1), from div_lt_div_of_lt_of_pos H2 dec_trivial, by rewrite [div_two at H3, -div_add_div_same at H3, div_two at H3]; exact H3) - (pos_div_of_pos_of_pos (iff.mp' !sub_pos_iff_lt H) dec_trivial)) + (pos_div_of_pos_of_pos (iff.mpr !sub_pos_iff_lt H) dec_trivial)) theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := sorry @@ -73,7 +73,7 @@ theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a apply (exists.elim (find_midpoint Hb)), intro c Hc, let Hc' := H c (and.right Hc), - apply (rat.not_le_of_gt (and.left Hc)) ((iff.mp' !le_add_iff_sub_right_le) Hc') + apply (rat.not_le_of_gt (and.left Hc)) (iff.mpr !le_add_iff_sub_right_le Hc') end theorem rewrite_helper (a b c d : ℚ) : a * b - c * d = a * (b - d) + (a - c) * d := diff --git a/library/data/real/order.lean b/library/data/real/order.lean index 666319da2..b8ef6bc9a 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -66,9 +66,9 @@ theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) : existsi N, intro m Hm, have Habs : abs (s m - s n) ≥ s n - s m, by rewrite abs_sub; apply le_abs_self, - have Habs' : s m + abs (s m - s n) ≥ s n, from (iff.mp' (le_add_iff_sub_left_le _ _ _)) Habs, + have Habs' : s m + abs (s m - s n) ≥ s n, from (iff.mpr (le_add_iff_sub_left_le _ _ _)) Habs, have HN' : N⁻¹ + N⁻¹ ≤ s n - n⁻¹, begin - apply iff.mp' (le_add_iff_sub_right_le _ _ _), + apply iff.mpr (le_add_iff_sub_right_le _ _ _), rewrite [sub_neg_eq_add, add.comm, -add.assoc], apply le_of_lt HN end, @@ -164,7 +164,7 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos have Hs4 : N⁻¹ ≤ s (2 * 2 * N), from HN _ (!mul_le_mul_left), apply lt_of_lt_of_le, rotate 1, - apply iff.mp' (rat.add_le_add_right_iff _ _ _), + apply iff.mpr (rat.add_le_add_right_iff _ _ _), apply Hs4, rewrite [*pnat.mul.assoc, pnat.add_halves, -(add_halves N), rat.add_sub_cancel], apply inv_two_mul_lt_inv @@ -443,7 +443,7 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_ ... ≥ 0 - n⁻¹: begin apply rat.sub_le_sub_right, apply le_of_lt, - apply (iff.mp' (sub_pos_iff_lt _ _)), + apply (iff.mpr (sub_pos_iff_lt _ _)), apply HN end ... = -n⁻¹ : by rewrite zero_sub), @@ -464,7 +464,7 @@ theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le apply exists.elim Hlt, intro N HN, let LeN := Le N, - let HN' := (iff.mp' (neg_lt_neg_iff_lt _ _)) HN, + let HN' := (iff.mpr (neg_lt_neg_iff_lt _ _)) HN, rewrite [↑sadd at HN', ↑sneg at HN', neg_add at HN', neg_neg at HN', add.comm at HN'], let HN'' := not_le_of_gt HN', apply absurd LeN HN'' @@ -819,11 +819,11 @@ theorem sep_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : apply or.elim Hor, intro Hlt, apply or.inl, - apply iff.mp' (lt_well_defined Hs Ht Hu Hv Hsu Htv), + apply iff.mpr (lt_well_defined Hs Ht Hu Hv Hsu Htv), assumption, intro Hlt, apply or.inr, - apply iff.mp' (lt_well_defined Ht Hs Hv Hu Htv Hsu), + apply iff.mpr (lt_well_defined Ht Hs Hv Hu Htv Hsu), assumption end @@ -920,7 +920,7 @@ theorem const_le_const_of_le {a b : ℚ} (H : a ≤ b) : s_le (const a) (const b apply rat.neg_nonpos_of_nonneg, apply rat.le_of_lt, apply inv_pos, - apply iff.mp' !rat.sub_nonneg_iff_le, + apply iff.mpr !rat.sub_nonneg_iff_le, apply H end diff --git a/library/data/set/function.lean b/library/data/set/function.lean index 2edb267b2..30ee2aff9 100644 --- a/library/data/set/function.lean +++ b/library/data/set/function.lean @@ -196,8 +196,8 @@ iff.intro (assume H, obtain Hmaps Hinj Hsurj, from H, (and.intro - (iff.mp' !injective_iff_inj_on_univ Hinj) - (iff.mp' !surjective_iff_surj_on_univ Hsurj))) + (iff.mpr !injective_iff_inj_on_univ Hinj) + (iff.mpr !surjective_iff_surj_on_univ Hsurj))) /- left inverse -/ diff --git a/library/init/logic.lean b/library/init/logic.lean index cae5a0d7e..b180b5a80 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -227,7 +227,7 @@ namespace iff theorem elim_right (H : a ↔ b) : b → a := elim (assume H₁ H₂, H₂) H - definition mp' := @elim_right + definition mpr := @elim_right theorem refl (a : Prop) : a ↔ a := intro (assume H, H) (assume H, H) @@ -597,14 +597,14 @@ decidable.rec theorem dif_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A} (h_c : b ↔ c) - (h_t : ∀ (h : c), x (iff.mp' h_c h) = u h) - (h_e : ∀ (h : ¬c), y (iff.mp' (not_iff_not_of_iff h_c) h) = v h) : + (h_t : ∀ (h : c), x (iff.mpr h_c h) = u h) + (h_e : ∀ (h : ¬c), y (iff.mpr (not_iff_not_of_iff h_c) h) = v h) : (@dite b dec_b A x y) = (@dite c dec_c A u v) := decidable.rec_on dec_b (λ hp : b, calc (if h : b then x h else y h) = x hp : dif_pos hp - ... = x (iff.mp' h_c (iff.mp h_c hp)) : proof_irrel + ... = x (iff.mpr h_c (iff.mp h_c hp)) : proof_irrel ... = u (iff.mp h_c hp) : h_t ... = (if h : c then u h else v h) : dif_pos (iff.mp h_c hp)) (λ hn : ¬b, @@ -612,15 +612,15 @@ decidable.rec_on dec_b calc (if h : b then x h else y h) = y hn : dif_neg hn - ... = y (iff.mp' h_nc (iff.mp h_nc hn)) : proof_irrel + ... = y (iff.mpr h_nc (iff.mp h_nc hn)) : proof_irrel ... = v (iff.mp h_nc hn) : h_e ... = (if h : c then u h else v h) : dif_neg (iff.mp h_nc hn)) theorem dif_ctx_rw_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A} (h_c : b ↔ c) - (h_t : ∀ (h : c), x (iff.mp' h_c h) = u h) - (h_e : ∀ (h : ¬c), y (iff.mp' (not_iff_not_of_iff h_c) h) = v h) : + (h_t : ∀ (h : c), x (iff.mpr h_c h) = u h) + (h_e : ∀ (h : ¬c), y (iff.mpr (not_iff_not_of_iff h_c) h) = v h) : (@dite b dec_b A x y) = (@dite c (decidable_of_decidable_of_iff dec_b h_c) A u v) := @dif_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 7c893134d..3e697dd24 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -251,7 +251,7 @@ definition iff.def : (a ↔ b) = ((a → b) ∧ (b → a)) := theorem iff_true [rewrite] (a : Prop) : (a ↔ true) ↔ a := iff.intro - (assume H, iff.mp' H trivial) + (assume H, iff.mpr H trivial) (assume H, iff.intro (assume H1, trivial) (assume H1, H)) theorem true_iff [rewrite] (a : Prop) : (true ↔ a) ↔ a := diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index a1a83be0b..f2e119c91 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -106,12 +106,12 @@ section theorem congr_forall : (∀x, p₁ x) ↔ (∀x, p₂ x) := iff.intro (assume H', take x, iff.mp (H x) (H' x)) - (assume H', take x, iff.mp' (H x) (H' x)) + (assume H', take x, iff.mpr (H x) (H' x)) theorem congr_exists : (∃x, p₁ x) ↔ (∃x, p₂ x) := iff.intro (assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mp (H x) H₁))) - (assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mp' (H x) H₁))) + (assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mpr (H x) H₁))) include H theorem congr_exists_unique : (∃!x, p₁ x) ↔ (∃!x, p₂ x) := diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index 186d42242..f9ae6eb56 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -71,7 +71,7 @@ lt_of_succ_le (le.trans h₂ h₃) definition sub_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≠ 1 ∧ m ≠ n} := assume h₁ h₂, -have h₃ : ¬ prime_ext n, from iff.mp' (not_iff_not_of_iff !prime_ext_iff_prime) h₂, +have h₃ : ¬ prime_ext n, from iff.mpr (not_iff_not_of_iff !prime_ext_iff_prime) h₂, have h₄ : ¬ n ≥ 2 ∨ ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from iff.mp !not_and_iff_not_or_not h₃, have h₅ : ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from or_resolve_right h₄ (not_not_intro h₁), have h₆ : ¬ (∀ m, m < succ n → m ∣ n → m = 1 ∨ m = n), from