chore(algebra/ordered_group): use implicit args, add add_eq_coe (#4853

)

* Use implicit arguments in various `iff` lemmas about `with_top`.
* Add `add_eq_coe`.
* Rewrite `with_top.ordered_add_comm_monoid` moving `begin .. end` blocks inside the structure.

This way we don't depend on the fact that `refine` doesn't introduce any `id`s and it's easier to see right away which block proves which statement.

src/algebra/ordered_group.lean

@@ -379,6 +379,25 @@ instance [add_semigroup α] : add_semigroup (with_top α) :=
 @[norm_cast]
 lemma coe_bit1 [has_add α] [has_one α] {a : α} : ((bit1 a : α) : with_top α) = bit1 a := rfl
 
+@[simp] lemma add_top [has_add α] : ∀{a : with_top α}, a + ⊤ = ⊤
+| none := rfl
+| (some a) := rfl
+
+@[simp] lemma top_add [has_add α] {a : with_top α} : ⊤ + a = ⊤ := rfl
+
+lemma add_eq_top [has_add α] {a b : with_top α} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
+by {cases a; cases b; simp [none_eq_top, some_eq_coe, ←with_top.coe_add, ←with_zero.coe_add]}
+
+lemma add_lt_top [has_add α] [partial_order α] {a b : with_top α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
+by simp [lt_top_iff_ne_top, add_eq_top, not_or_distrib]
+
+lemma add_eq_coe [has_add α] : ∀ {a b : with_top α} {c : α},
+  a + b = c ↔ ∃ (a' b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
+| none b c := by simp [none_eq_top]
+| (some a) none c := by simp [none_eq_top]
+| (some a) (some b) c :=
+    by simp only [some_eq_coe, ← coe_add, coe_eq_coe, exists_and_distrib_left, exists_eq_left]
+
 instance [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
 { ..@additive.add_comm_semigroup _ $
     @with_zero.comm_semigroup (multiplicative α) _ }
@@ -396,28 +415,24 @@ instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
     @with_zero.comm_monoid_with_zero (multiplicative α) _ }
 
 instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_top α) :=
-begin
-  suffices, refine {
-    add_le_add_left := this,
-    ..with_top.partial_order,
-    ..with_top.add_comm_monoid, ..},
-  { intros a b c h,
-    have h' := h,
-    rw lt_iff_le_not_le at h' ⊢,
-    refine ⟨λ c h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
-    cases h₂, cases a with a,
-    { exact (not_le_of_lt h).elim le_top },
-    cases b with b,
-    { exact (not_le_of_lt h).elim le_top },
-    { exact ⟨_, rfl, le_of_lt (lt_of_add_lt_add_left $
-        with_top.some_lt_some.1 h)⟩ } },
-  { intros a b h c ca h₂,
-    cases c with c, {cases h₂},
-    cases b with b; cases h₂,
-    cases a with a, {cases le_antisymm h le_top },
-    simp at h,
-    exact ⟨_, rfl, add_le_add_left h _⟩, }
-end
+{ add_le_add_left :=
+    begin
+      rintros a b h (_|c), { simp [none_eq_top] },
+      rcases b with (_|b), { simp [none_eq_top] },
+      rcases le_coe_iff.1 h with ⟨a, rfl, h⟩,
+      simp only [some_eq_coe, ← coe_add, coe_le_coe] at h ⊢,
+      exact add_le_add_left h c
+    end,
+  lt_of_add_lt_add_left :=
+    begin
+      intros a b c h,
+      rcases lt_iff_exists_coe.1 h with ⟨ab, hab, hlt⟩,
+      rcases add_eq_coe.1 hab with ⟨a, b, rfl, rfl, rfl⟩,
+      rw coe_lt_iff,
+      rintro c rfl,
+      exact lt_of_add_lt_add_left (coe_lt_coe.1 hlt)
+    end,
+  ..with_top.partial_order, ..with_top.add_comm_monoid }
 
 /-- Coercion from `α` to `with_top α` as an `add_monoid_hom`. -/
 def coe_add_hom [add_monoid α] : α →+ with_top α :=
@@ -432,18 +447,6 @@ coe_lt_top 0
   (0 : with_top α) < a ↔ 0 < a :=
 coe_lt_coe
 
-@[simp] lemma add_top [ordered_add_comm_monoid α] : ∀{a : with_top α}, a + ⊤ = ⊤
-| none := rfl
-| (some a) := rfl
-
-@[simp] lemma top_add [ordered_add_comm_monoid α] {a : with_top α} : ⊤ + a = ⊤ := rfl
-
-lemma add_eq_top [ordered_add_comm_monoid α] (a b : with_top α) : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
-by {cases a; cases b; simp [none_eq_top, some_eq_coe, ←with_top.coe_add, ←with_zero.coe_add]}
-
-lemma add_lt_top [ordered_add_comm_monoid α] (a b : with_top α) : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
-by simp [lt_top_iff_ne_top, add_eq_top, not_or_distrib]
-
 end with_top
 
 namespace with_bot

src/data/real/ennreal.lean

@@ -261,8 +261,8 @@ def of_nnreal_hom : ℝ≥0 →+* ennreal :=
 @[simp, norm_cast] lemma coe_pow (n : ℕ) : (↑(r^n) : ennreal) = r^n :=
 of_nnreal_hom.map_pow r n
 
-lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top _ _
-lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top _ _
+lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top
+lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top
 
 lemma to_nnreal_add {r₁ r₂ : ennreal} (h₁ : r₁ < ⊤) (h₂ : r₂ < ⊤) :
   (r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal :=
@@ -362,10 +362,14 @@ lemma zero_lt_coe_iff : 0 < (↑p : ennreal) ↔ 0 < p := coe_lt_coe
 @[simp] lemma top_ne_nat (n : nat) : (⊤ : ennreal) ≠ n := with_top.top_ne_nat n
 @[simp] lemma one_lt_top : 1 < ∞ := coe_lt_top
 
-lemma le_coe_iff : a ≤ ↑r ↔ (∃p:ℝ≥0, a = p ∧ p ≤ r) := with_top.le_coe_iff r a
-lemma coe_le_iff : ↑r ≤ a ↔ (∀p:ℝ≥0, a = p → r ≤ p) := with_top.coe_le_iff r a
+lemma le_coe_iff : a ≤ ↑r ↔ (∃p:ℝ≥0, a = p ∧ p ≤ r) := with_top.le_coe_iff
+lemma coe_le_iff : ↑r ≤ a ↔ (∀p:ℝ≥0, a = p → r ≤ p) := with_top.coe_le_iff
 
-lemma lt_iff_exists_coe : a < b ↔ (∃p:ℝ≥0, a = p ∧ ↑p < b) := with_top.lt_iff_exists_coe a b
+lemma lt_iff_exists_coe : a < b ↔ (∃p:ℝ≥0, a = p ∧ ↑p < b) := with_top.lt_iff_exists_coe
+
+@[simp, norm_cast] lemma coe_finset_sup {s : finset α} {f : α → ℝ≥0} :
+  ↑(s.sup f) = s.sup (λ x, (f x : ennreal)) :=
+finset.comp_sup_eq_sup_comp_of_is_total _ coe_mono rfl
 
 lemma pow_le_pow {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
 begin

src/order/bounded_lattice.lean

@@ -694,15 +694,15 @@ theorem le_coe [partial_order α] {a b : α} :
   (@has_le.le (with_top α) _ o b ↔ a ≤ b)
 | _ rfl := coe_le_coe
 
-theorem le_coe_iff [partial_order α] (b : α) : ∀(x : with_top α), x ≤ b ↔ (∃a:α, x = a ∧ a ≤ b)
+theorem le_coe_iff [partial_order α] {b : α} : ∀{x : with_top α}, x ≤ b ↔ (∃a:α, x = a ∧ a ≤ b)
 | (some a) := by simp [some_eq_coe, coe_eq_coe]
 | none     := by simp [none_eq_top]
 
-theorem coe_le_iff [partial_order α] (a : α) : ∀(x : with_top α), ↑a ≤ x ↔ (∀b:α, x = ↑b → a ≤ b)
+theorem coe_le_iff [partial_order α] {a : α} : ∀{x : with_top α}, ↑a ≤ x ↔ (∀b:α, x = ↑b → a ≤ b)
 | (some b) := by simp [some_eq_coe, coe_eq_coe]
 | none     := by simp [none_eq_top]
 
-theorem lt_iff_exists_coe [partial_order α] : ∀(a b : with_top α), a < b ↔ (∃p:α, a = p ∧ ↑p < b)
+theorem lt_iff_exists_coe [partial_order α] : ∀{a b : with_top α}, a < b ↔ (∃p:α, a = p ∧ ↑p < b)
 | (some a) b := by simp [some_eq_coe, coe_eq_coe]
 | none     b := by simp [none_eq_top]
 
@@ -711,6 +711,10 @@ lemma coe_lt_coe [partial_order α] {a b : α} : (a : with_top α) < b ↔ a < b
 
 lemma coe_lt_top [partial_order α] (a : α) : (a : with_top α) < ⊤ := some_lt_none
 
+theorem coe_lt_iff [partial_order α] {a : α} : ∀{x : with_top α}, ↑a < x ↔ (∀b:α, x = ↑b → a < b)
+| (some b) := by simp [some_eq_coe, coe_eq_coe, coe_lt_coe]
+| none     := by simp [none_eq_top, coe_lt_top]
+
 lemma not_top_le_coe [partial_order α] (a : α) : ¬ (⊤:with_top α) ≤ ↑a :=
 assume h, (lt_irrefl ⊤ (lt_of_le_of_lt h (coe_lt_top a))).elim
 
@@ -813,7 +817,7 @@ instance densely_ordered [partial_order α] [densely_ordered α] [no_top_order 
 lemma lt_iff_exists_coe_btwn [partial_order α] [densely_ordered α] [no_top_order α]
   {a b : with_top α} :
   (a < b) ↔ (∃ x : α, a < ↑x ∧ ↑x < b) :=
-⟨λ h, let ⟨y, hy⟩ := exists_between h, ⟨x, hx⟩ := (lt_iff_exists_coe _ _).1 hy.2 in ⟨x, hx.1 ▸ hy⟩,
+⟨λ h, let ⟨y, hy⟩ := exists_between h, ⟨x, hx⟩ := lt_iff_exists_coe.1 hy.2 in ⟨x, hx.1 ▸ hy⟩,
  λ ⟨x, hx⟩, lt_trans hx.1 hx.2⟩
 
 end with_top

src/order/conditionally_complete_lattice.lean

@@ -593,15 +593,15 @@ begin
   cases s.eq_empty_or_nonempty with hs hs,
   { rw [hs, cSup_empty], simp only [set.mem_empty_eq, supr_bot, supr_false], refl },
   apply le_antisymm,
-  { refine ((coe_le_iff _ _).2 $ assume b hb, cSup_le hs $ assume a has, coe_le_coe.1 $ hb ▸ _),
+  { refine (coe_le_iff.2 $ assume b hb, cSup_le hs $ assume a has, coe_le_coe.1 $ hb ▸ _),
     exact (le_supr_of_le a $ le_supr_of_le has $ _root_.le_refl _) },
   { exact (supr_le $ assume a, supr_le $ assume ha, coe_le_coe.2 $ le_cSup hb ha) }
 end
 
 lemma coe_Inf {s : set α} (hs : s.nonempty) : (↑(Inf s) : with_top α) = (⨅a∈s, ↑a) :=
 let ⟨x, hx⟩ := hs in
 have (⨅a∈s, ↑a : with_top α) ≤ x, from infi_le_of_le x $ infi_le_of_le hx $ _root_.le_refl _,
-let ⟨r, r_eq, hr⟩ := (le_coe_iff _ _).1 this in
+let ⟨r, r_eq, hr⟩ := le_coe_iff.1 this in
 le_antisymm
   (le_infi $ assume a, le_infi $ assume ha, coe_le_coe.2 $ cInf_le (order_bot.bdd_below s) ha)
   begin

src/topology/metric_space/basic.lean

@@ -1142,9 +1142,7 @@ begin
     ennreal.to_real (sup univ (λ (b : β), edist (x b) (y b))),
   { assume x y,
     have : sup univ (λ (b : β), edist (x b) (y b)) = ↑(sup univ (λ (b : β), nndist (x b) (y b))),
-    { simp [edist_nndist],
-      refine eq.symm (comp_sup_eq_sup_comp_of_is_total _ _ _),
-      exact (assume x y h, ennreal.coe_le_coe.2 h), refl },
+    { simp [edist_nndist] },
     rw this,
     refl }
 end