diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 5d2a6c632..0ed34f691 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -197,9 +197,12 @@ section group theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b := iff.intro (assume H, inv.inj H) (assume H, congr_arg _ H) - theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 := + theorem inv_eq_one_iff_eq_one (a : A) : a⁻¹ = 1 ↔ a = 1 := one_inv ▸ inv_eq_inv_iff_eq a 1 + theorem eq_one_of_inv_eq_one (a : A) : a⁻¹ = 1 → a = 1 := + iff.mp !inv_eq_one_iff_eq_one + theorem eq_inv_of_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ := by rewrite [H, inv_inv] @@ -379,9 +382,15 @@ section add_group theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b := iff.intro (assume H, neg.inj H) (assume H, congr_arg _ H) + theorem eq_of_neg_eq_neg {a b : A} : -a = -b → a = b := + iff.mp !neg_eq_neg_iff_eq + theorem neg_eq_zero_iff_eq_zero (a : A) : -a = 0 ↔ a = 0 := neg_zero ▸ !neg_eq_neg_iff_eq + theorem eq_zero_of_neg_eq_zero {a : A} : -a = 0 → a = 0 := + iff.mp !neg_eq_zero_iff_eq_zero + theorem eq_neg_of_eq_neg {a b : A} (H : a = -b) : b = -a := H⁻¹ ▸ (neg_neg b)⁻¹ diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 1eeaf9ff5..dd1f864af 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -278,87 +278,219 @@ section theorem le_neg_iff_le_neg : a ≤ -b ↔ b ≤ -a := !neg_neg ▸ !neg_le_neg_iff_le + theorem le_neg_of_le_neg : a ≤ -b → b ≤ -a := iff.mp !le_neg_iff_le_neg + theorem neg_le_iff_neg_le : -a ≤ b ↔ -b ≤ a := !neg_neg ▸ !neg_le_neg_iff_le + theorem neg_le_of_neg_le : -a ≤ b → -b ≤ a := iff.mp !neg_le_iff_neg_le + theorem lt_neg_iff_lt_neg : a < -b ↔ b < -a := !neg_neg ▸ !neg_lt_neg_iff_lt + theorem lt_neg_of_lt_neg : a < -b → b < -a := iff.mp !lt_neg_iff_lt_neg + theorem neg_lt_iff_neg_lt : -a < b ↔ -b < a := !neg_neg ▸ !neg_lt_neg_iff_lt + theorem neg_lt_of_neg_lt : -a < b → -b < a := iff.mp !neg_lt_iff_neg_lt + theorem sub_nonneg_iff_le : 0 ≤ a - b ↔ b ≤ a := !sub_self ▸ !add_le_add_right_iff + theorem sub_nonneg_of_le : b ≤ a → 0 ≤ a - b := iff.mpr !sub_nonneg_iff_le + + theorem le_of_sub_nonneg : 0 ≤ a - b → b ≤ a := iff.mp !sub_nonneg_iff_le + theorem sub_nonpos_iff_le : a - b ≤ 0 ↔ a ≤ b := !sub_self ▸ !add_le_add_right_iff + theorem sub_nonpos_of_le : a ≤ b → a - b ≤ 0 := iff.mpr !sub_nonpos_iff_le + + theorem le_of_sub_nonpos : a - b ≤ 0 → a ≤ b := iff.mp !sub_nonpos_iff_le + theorem sub_pos_iff_lt : 0 < a - b ↔ b < a := !sub_self ▸ !add_lt_add_right_iff + theorem sub_pos_of_lt : b < a → 0 < a - b := iff.mpr !sub_pos_iff_lt + + theorem lt_of_sub_pos : 0 < a - b → b < a := iff.mp !sub_pos_iff_lt + theorem sub_neg_iff_lt : a - b < 0 ↔ a < b := !sub_self ▸ !add_lt_add_right_iff + theorem sub_neg_of_lt : a < b → a - b < 0 := iff.mpr !sub_neg_iff_lt + + theorem lt_of_sub_neg : a - b < 0 → a < b := iff.mp !sub_neg_iff_lt + theorem add_le_iff_le_neg_add : a + b ≤ c ↔ b ≤ -a + c := have H: a + b ≤ c ↔ -a + (a + b) ≤ -a + c, from iff.symm (!add_le_add_left_iff), !neg_add_cancel_left ▸ H + theorem add_le_of_le_neg_add : b ≤ -a + c → a + b ≤ c := + iff.mpr !add_le_iff_le_neg_add + + theorem le_neg_add_of_add_le : a + b ≤ c → b ≤ -a + c := + iff.mp !add_le_iff_le_neg_add + theorem add_le_iff_le_sub_left : a + b ≤ c ↔ b ≤ c - a := by rewrite [sub_eq_add_neg, {c+_}add.comm]; apply add_le_iff_le_neg_add + theorem add_le_of_le_sub_left : b ≤ c - a → a + b ≤ c := + iff.mpr !add_le_iff_le_sub_left + + theorem le_sub_left_of_add_le : a + b ≤ c → b ≤ c - a := + iff.mp !add_le_iff_le_sub_left + theorem add_le_iff_le_sub_right : a + b ≤ c ↔ a ≤ c - b := have H: a + b ≤ c ↔ a + b - b ≤ c - b, from iff.symm (!add_le_add_right_iff), !add_neg_cancel_right ▸ H + theorem add_le_of_le_sub_right : a ≤ c - b → a + b ≤ c := + iff.mpr !add_le_iff_le_sub_right + + theorem le_sub_right_of_add_le : a + b ≤ c → a ≤ c - b := + iff.mp !add_le_iff_le_sub_right + theorem le_add_iff_neg_add_le : a ≤ b + c ↔ -b + a ≤ c := assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff), by rewrite neg_add_cancel_left at H; exact H + theorem le_add_of_neg_add_le : -b + a ≤ c → a ≤ b + c := + iff.mpr !le_add_iff_neg_add_le + + theorem neg_add_le_of_le_add : a ≤ b + c → -b + a ≤ c := + iff.mp !le_add_iff_neg_add_le + theorem le_add_iff_sub_left_le : a ≤ b + c ↔ a - b ≤ c := by rewrite [sub_eq_add_neg, {a+_}add.comm]; apply le_add_iff_neg_add_le + theorem le_add_of_sub_left_le : a - b ≤ c → a ≤ b + c := + iff.mpr !le_add_iff_sub_left_le + + theorem sub_left_le_of_le_add : a ≤ b + c → a - b ≤ c := + iff.mp !le_add_iff_sub_left_le + theorem le_add_iff_sub_right_le : a ≤ b + c ↔ a - c ≤ b := assert H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff), by rewrite add_neg_cancel_right at H; exact H + theorem le_add_of_sub_right_le : a - c ≤ b → a ≤ b + c := + iff.mpr !le_add_iff_sub_right_le + + theorem sub_right_le_of_le_add : a ≤ b + c → a - c ≤ b := + iff.mp !le_add_iff_sub_right_le + theorem le_add_iff_neg_add_le_left : a ≤ b + c ↔ -b + a ≤ c := assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff), by rewrite neg_add_cancel_left at H; exact H + theorem le_add_of_neg_add_le_left : -b + a ≤ c → a ≤ b + c := + iff.mpr !le_add_iff_neg_add_le_left + + theorem neg_add_le_left_of_le_add : a ≤ b + c → -b + a ≤ c := + iff.mp !le_add_iff_neg_add_le_left + theorem le_add_iff_neg_add_le_right : a ≤ b + c ↔ -c + a ≤ b := by rewrite add.comm; apply le_add_iff_neg_add_le_left + theorem le_add_of_neg_add_le_right : -c + a ≤ b → a ≤ b + c := + iff.mpr !le_add_iff_neg_add_le_right + + theorem neg_add_le_right_of_le_add : a ≤ b + c → -c + a ≤ b := + iff.mp !le_add_iff_neg_add_le_right + theorem le_add_iff_neg_le_sub_left : c ≤ a + b ↔ -a ≤ b - c := assert H : c ≤ a + b ↔ -a + c ≤ b, from !le_add_iff_neg_add_le, assert H' : -a + c ≤ b ↔ -a ≤ b - c, from !add_le_iff_le_sub_right, iff.trans H H' + theorem le_add_of_neg_le_sub_left : -a ≤ b - c → c ≤ a + b := + iff.mpr !le_add_iff_neg_le_sub_left + + theorem neg_le_sub_left_of_le_add : c ≤ a + b → -a ≤ b - c := + iff.mp !le_add_iff_neg_le_sub_left + theorem le_add_iff_neg_le_sub_right : c ≤ a + b ↔ -b ≤ a - c := by rewrite add.comm; apply le_add_iff_neg_le_sub_left + theorem le_add_of_neg_le_sub_right : -b ≤ a - c → c ≤ a + b := + iff.mpr !le_add_iff_neg_le_sub_right + + theorem neg_le_sub_right_of_le_add : c ≤ a + b → -b ≤ a - c := + iff.mp !le_add_iff_neg_le_sub_right + theorem add_lt_iff_lt_neg_add_left : a + b < c ↔ b < -a + c := assert H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff), begin rewrite neg_add_cancel_left at H, exact H end + theorem add_lt_of_lt_neg_add_left : b < -a + c → a + b < c := + iff.mpr !add_lt_iff_lt_neg_add_left + + theorem lt_neg_add_left_of_add_lt : a + b < c → b < -a + c := + iff.mp !add_lt_iff_lt_neg_add_left + theorem add_lt_iff_lt_neg_add_right : a + b < c ↔ a < -b + c := by rewrite add.comm; apply add_lt_iff_lt_neg_add_left + theorem add_lt_of_lt_neg_add_right : a < -b + c → a + b < c := + iff.mpr !add_lt_iff_lt_neg_add_right + + theorem lt_neg_add_right_of_add_lt : a + b < c → a < -b + c := + iff.mp !add_lt_iff_lt_neg_add_right + theorem add_lt_iff_lt_sub_left : a + b < c ↔ b < c - a := begin rewrite [sub_eq_add_neg, {c+_}add.comm], apply add_lt_iff_lt_neg_add_left end - theorem add_lt_add_iff_lt_sub_right : a + b < c ↔ a < c - b := + theorem add_lt_of_lt_sub_left : b < c - a → a + b < c := + iff.mpr !add_lt_iff_lt_sub_left + + theorem lt_sub_left_of_add_lt : a + b < c → b < c - a := + iff.mp !add_lt_iff_lt_sub_left + + theorem add_lt_iff_lt_sub_right : a + b < c ↔ a < c - b := assert H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff), by rewrite add_neg_cancel_right at H; exact H + theorem add_lt_of_lt_sub_right : a < c - b → a + b < c := + iff.mpr !add_lt_iff_lt_sub_right + + theorem lt_sub_right_of_add_lt : a + b < c → a < c - b := + iff.mp !add_lt_iff_lt_sub_right + theorem lt_add_iff_neg_add_lt_left : a < b + c ↔ -b + a < c := assert H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff), by rewrite neg_add_cancel_left at H; exact H + theorem lt_add_of_neg_add_lt_left : -b + a < c → a < b + c := + iff.mpr !lt_add_iff_neg_add_lt_left + + theorem neg_add_lt_left_of_lt_add : a < b + c → -b + a < c := + iff.mp !lt_add_iff_neg_add_lt_left + theorem lt_add_iff_neg_add_lt_right : a < b + c ↔ -c + a < b := by rewrite add.comm; apply lt_add_iff_neg_add_lt_left + theorem lt_add_of_neg_add_lt_right : -c + a < b → a < b + c := + iff.mpr !lt_add_iff_neg_add_lt_right + + theorem neg_add_lt_right_of_lt_add : a < b + c → -c + a < b := + iff.mp !lt_add_iff_neg_add_lt_right + theorem lt_add_iff_sub_lt_left : a < b + c ↔ a - b < c := by rewrite [sub_eq_add_neg, {a + _}add.comm]; apply lt_add_iff_neg_add_lt_left + theorem lt_add_of_sub_lt_left : a - b < c → a < b + c := + iff.mpr !lt_add_iff_sub_lt_left + + theorem sub_lt_left_of_lt_add : a < b + c → a - b < c := + iff.mp !lt_add_iff_sub_lt_left + theorem lt_add_iff_sub_lt_right : a < b + c ↔ a - c < b := by rewrite add.comm; apply lt_add_iff_sub_lt_left + theorem lt_add_of_sub_lt_right : a - c < b → a < b + c := + iff.mpr !lt_add_iff_sub_lt_right + + theorem sub_lt_right_of_lt_add : a < b + c → a - c < b := + iff.mp !lt_add_iff_sub_lt_right + -- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0 theorem le_iff_le_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a ≤ b ↔ c ≤ d := calc diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index b503bef61..062d3c553 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -570,12 +570,12 @@ theorem floor_succ (x : ℝ) : (floor x) + 1 = floor (x + 1) := apply by_contradiction, intro H, cases int.lt_or_gt_of_ne H with [Hlt, Hgt], - let Hl := floor_largest (iff.mp !int.add_lt_add_iff_lt_sub_right Hlt), + let Hl := floor_largest (iff.mp !int.add_lt_iff_lt_sub_right Hlt), rewrite [of_int_sub at Hl, -of_rat_sub at Hl], - apply (not_le_of_gt (iff.mpr !add_lt_add_iff_lt_sub_right Hl)) !floor_spec, + apply not_le_of_gt (iff.mpr !add_lt_iff_lt_sub_right Hl) !floor_spec, let Hl := floor_largest Hgt, rewrite [of_int_add at Hl, -of_rat_add at Hl], - apply (not_le_of_gt (lt_of_add_lt_add_right Hl)) !floor_spec + apply not_le_of_gt (lt_of_add_lt_add_right Hl) !floor_spec end theorem floor_succ_lt (x : ℝ) : floor (x - 1) < floor x :=