chore(order/directed): use implicit args in iffs (#3411)

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: urkud

src/analysis/convex/cone.lean

@@ -350,7 +350,7 @@ begin
     refine ⟨linear_pmap.Sup c c_chain.directed_on, _, λ _, linear_pmap.le_Sup c_chain.directed_on⟩,
     rintros ⟨x, hx⟩ hxs,
     have hdir : directed_on (≤) (linear_pmap.domain '' c),
-      from (directed_on_image _).2 (c_chain.directed_on.mono _ linear_pmap.domain_mono.monotone),
+      from directed_on_image.2 (c_chain.directed_on.mono linear_pmap.domain_mono.monotone),
     rcases (mem_Sup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩,
     have : f ≤ linear_pmap.Sup c c_chain.directed_on, from linear_pmap.le_Sup _ hfc,
     convert ← hcs hfc ⟨x, hfx⟩ hxs,

src/group_theory/subgroup.lean

@@ -490,8 +490,7 @@ lemma mem_Sup_of_directed_on {K : set (subgroup G)} (Kne : K.nonempty)
   x ∈ Sup K ↔ ∃ s ∈ K, x ∈ s :=
 begin
   haveI : nonempty K := Kne.to_subtype,
-  rw [Sup_eq_supr, supr_subtype', mem_supr_of_directed, subtype.exists],
-  exact (directed_on_iff_directed _).1 hK
+  simp only [Sup_eq_supr', mem_supr_of_directed hK.directed_coe, set_coe.exists, subtype.coe_mk]
 end
 
 variables {N : Type*} [group N] {P : Type*} [group P]

src/group_theory/submonoid/membership.lean

@@ -100,8 +100,7 @@ lemma mem_Sup_of_directed_on {S : set (submonoid M)} (Sne : S.nonempty)
   x ∈ Sup S ↔ ∃ s ∈ S, x ∈ s :=
 begin
   haveI : nonempty S := Sne.to_subtype,
-  rw [Sup_eq_supr, supr_subtype', mem_supr_of_directed, subtype.exists],
-  exact (directed_on_iff_directed _).1 hS
+  simp only [Sup_eq_supr', mem_supr_of_directed hS.directed_coe, set_coe.exists, subtype.coe_mk]
 end
 
 @[to_additive]

src/linear_algebra/basic.lean

@@ -728,8 +728,7 @@ theorem mem_Sup_of_directed {s : set (submodule R M)}
   z ∈ Sup s ↔ ∃ y ∈ s, z ∈ y :=
 begin
   haveI : nonempty s := hs.to_subtype,
-  rw [Sup_eq_supr, supr_subtype', mem_supr_of_directed, subtype.exists],
-  exact (directed_on_iff_directed _).1 hdir
+  simp only [Sup_eq_supr', mem_supr_of_directed _ hdir.directed_coe, set_coe.exists, subtype.coe_mk]
 end
 
 section

src/linear_algebra/basis.lean

@@ -373,16 +373,13 @@ lemma linear_independent_sUnion_of_directed {s : set (set M)}
   (h : ∀ a ∈ s, linear_independent R (λ x, x : (a : set M) → M)) :
   linear_independent R (λ x, x : (⋃₀ s) → M) :=
 by rw sUnion_eq_Union; exact
-linear_independent_Union_of_directed
-  ((directed_on_iff_directed _).1 hs) (by simpa using h)
+linear_independent_Union_of_directed hs.directed_coe (by simpa using h)
 
 lemma linear_independent_bUnion_of_directed {η} {s : set η} {t : η → set M}
   (hs : directed_on (t ⁻¹'o (⊆)) s) (h : ∀a∈s, linear_independent R (λ x, x : t a → M)) :
   linear_independent R (λ x, x : (⋃a∈s, t a) → M) :=
 by rw bUnion_eq_Union; exact
-linear_independent_Union_of_directed
-  ((directed_comp _ _ _).2 $ (directed_on_iff_directed _).1 hs)
-  (by simpa using h)
+linear_independent_Union_of_directed (directed_comp.2 $ hs.directed_coe) (by simpa using h)
 
 lemma linear_independent_Union_finite_subtype {ι : Type*} {f : ι → set M}
   (hl : ∀i, linear_independent R (λ x, x : f i → M))

src/linear_algebra/linear_pmap.lean

@@ -287,7 +287,7 @@ private lemma Sup_aux (c : set (linear_pmap R E F)) (hc : directed_on (≤) c) :
 begin
   cases c.eq_empty_or_nonempty with ceq cne, { subst c, simp },
   have hdir : directed_on (≤) (domain '' c),
-    from (directed_on_image _).2 (hc.mono _ domain_mono.monotone),
+    from directed_on_image.2 (hc.mono domain_mono.monotone),
   have P : Π x : Sup (domain '' c), {p : c // (x : E) ∈ p.val.domain },
   { rintros x,
     apply classical.indefinite_description,

src/order/complete_lattice.lean

@@ -806,7 +806,7 @@ lemma infi_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
 (@infi_subtype _ _ _ p (λ x, f x.val x.property)).symm
 
 lemma infi_subtype'' {ι} (s : set ι) (f : ι → α) :
-(⨅ i : s, f i) = ⨅ (t : ι) (H : t ∈ s), f t :=
+  (⨅ i : s, f i) = ⨅ (t : ι) (H : t ∈ s), f t :=
 infi_subtype
 
 lemma is_glb_binfi {s : set β} {f : β → α} : is_glb (f '' s) (⨅ x ∈ s, f x) :=
@@ -818,9 +818,12 @@ le_antisymm
   (supr_le $ assume i, supr_le $ assume : p i, le_supr _ _)
 
 lemma supr_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
-  (⨆ i (h : p i), f i h) = (⨆ x : subtype p, f x.val x.property) :=
+  (⨆ i (h : p i), f i h) = (⨆ x : subtype p, f x x.property) :=
 (@supr_subtype _ _ _ p (λ x, f x.val x.property)).symm
 
+lemma Sup_eq_supr' {s : set α} : Sup s = ⨆ x : s, (x : α) :=
+by rw [Sup_eq_supr, supr_subtype']; refl
+
 lemma is_lub_bsupr {s : set β} {f : β → α} : is_lub (f '' s) (⨆ x ∈ s, f x) :=
 by simpa only [range_comp, subtype.range_coe, supr_subtype'] using @is_lub_supr α s _ (f ∘ coe)
 

src/order/directed.lean

@@ -19,9 +19,13 @@ def directed (f : ι → α) := ∀x y, ∃z, f x ≼ f z ∧ f y ≼ f z
   pair of elements in the set. -/
 def directed_on (s : set α) := ∀ (x ∈ s) (y ∈ s), ∃z ∈ s, x ≼ z ∧ y ≼ z
 
+variables {r}
+
 theorem directed_on_iff_directed {s} : @directed_on α r s ↔ directed r (coe : s → α) :=
 by simp [directed, directed_on]; refine ball_congr (λ x hx, by simp; refl)
 
+alias directed_on_iff_directed ↔ directed_on.directed_coe _
+
 theorem directed_on_image {s} {f : β → α} :
   directed_on r (f '' s) ↔ directed_on (f ⁻¹'o r) s :=
 by simp only [directed_on, set.ball_image_iff, set.bex_image_iff, order.preimage]
@@ -31,19 +35,17 @@ theorem directed_on.mono {s : set α} (h : directed_on r s)
   directed_on r' s :=
 λ x hx y hy, let ⟨z, zs, xz, yz⟩ := h x hx y hy in ⟨z, zs, H xz, H yz⟩
 
-theorem directed_comp {ι} (f : ι → β) (g : β → α) :
+theorem directed_comp {ι} {f : ι → β} {g : β → α} :
   directed r (g ∘ f) ↔ directed (g ⁻¹'o r) f := iff.rfl
 
-variable {r}
-
 theorem directed.mono {s : α → α → Prop} {ι} {f : ι → α}
   (H : ∀ a b, r a b → s a b) (h : directed r f) : directed s f :=
 λ a b, let ⟨c, h₁, h₂⟩ := h a b in ⟨c, H _ _ h₁, H _ _ h₂⟩
 
 theorem directed.mono_comp {ι} {rb : β → β → Prop} {g : α → β} {f : ι → α}
   (hg : ∀ ⦃x y⦄, x ≼ y → rb (g x) (g y)) (hf : directed r f) :
   directed rb (g ∘ f) :=
-(directed_comp rb f g).2 $ hf.mono hg
+directed_comp.2 $ hf.mono hg
 
 /-- A monotone function on a sup-semilattice is directed. -/
 lemma directed_of_sup [semilattice_sup α] {f : α → β} {r : β → β → Prop}

src/ring_theory/subsemiring.lean

@@ -481,8 +481,7 @@ lemma mem_Sup_of_directed_on {S : set (subsemiring R)} (Sne : S.nonempty)
   x ∈ Sup S ↔ ∃ s ∈ S, x ∈ s :=
 begin
   haveI : nonempty S := Sne.to_subtype,
-  rw [Sup_eq_supr, supr_subtype', mem_supr_of_directed, subtype.exists],
-  exact (directed_on_iff_directed _).1 hS
+  simp only [Sup_eq_supr', mem_supr_of_directed hS.directed_coe, set_coe.exists, subtype.coe_mk]
 end
 
 lemma coe_Sup_of_directed_on {S : set (subsemiring R)} (Sne : S.nonempty) (hS : directed_on (≤) S) :

src/topology/algebra/infinite_sum.lean

@@ -440,7 +440,7 @@ theorem rel_supr_sum [complete_lattice β] (m : β → α) (m0 : m ⊥ = 0)
   (s : δ → β) (t : finset δ) :
   R (m (⨆ d ∈ t, s d)) (∑ d in t, m (s d)) :=
 by { cases t.nonempty_encodable, rw [supr_subtype'], convert rel_supr_tsum m m0 R m_supr _,
-     rw [← finset.tsum_subtype], refl, assumption }
+     rw [← finset.tsum_subtype], assumption }
 
 /-- If a function is countably sub-additive then it is binary sub-additive -/
 theorem rel_sup_add [complete_lattice β] (m : β → α) (m0 : m ⊥ = 0)