golf(*): λ _, default → default (#14608)

src/computability/turing_machine.lean

@@ -302,7 +302,7 @@ structure {u v} pointed_map (Γ : Type u) (Γ' : Type v)
 (f : Γ → Γ') (map_pt' : f default = default)
 
 instance {Γ Γ'} [inhabited Γ] [inhabited Γ'] : inhabited (pointed_map Γ Γ') :=
-⟨⟨λ _, default, rfl⟩⟩
+⟨⟨default, rfl⟩⟩
 
 instance {Γ Γ'} [inhabited Γ] [inhabited Γ'] : has_coe_to_fun (pointed_map Γ Γ') (λ _, Γ → Γ') :=
 ⟨pointed_map.f⟩

src/data/array/lemmas.lean

@@ -12,7 +12,7 @@ namespace d_array
 variables {n : ℕ} {α : fin n → Type u}
 
 instance [∀ i, inhabited (α i)] : inhabited (d_array n α) :=
-⟨⟨λ _, default⟩⟩
+⟨⟨default⟩⟩
 
 end d_array
 

src/data/finset/basic.lean

@@ -2588,7 +2588,7 @@ def sigma_equiv_option_of_inhabited (α : Type u) [inhabited α] [decidable_eq 
   Σ (β : Type u), α ≃ option β :=
 ⟨{x : α // x ≠ default},
 { to_fun := λ (x : α), if h : x = default then none else some ⟨x, h⟩,
-  inv_fun := λ o, option.elim o (default) coe,
+  inv_fun := λ o, option.elim o default coe,
   left_inv := λ x, by { dsimp only, split_ifs; simp [*] },
   right_inv := begin
     rintro (_|⟨x,h⟩),

src/data/holor.lean

@@ -38,7 +38,7 @@ open_locale big_operators
 
 /-- `holor_index ds` is the type of valid index tuples used to identify an entry of a holor
 of dimensions `ds`. -/
-def holor_index (ds : list ℕ) : Type := { is : list ℕ // forall₂ (<) is ds}
+def holor_index (ds : list ℕ) : Type := {is : list ℕ // forall₂ (<) is ds}
 
 namespace holor_index
 variables {ds₁ ds₂ ds₃ : list ℕ}
@@ -80,7 +80,7 @@ lemma drop_drop :
 end holor_index
 
 /-- Holor (indexed collections of tensor coefficients) -/
-def holor (α : Type u) (ds:list ℕ) := holor_index ds → α
+def holor (α : Type u) (ds : list ℕ) := holor_index ds → α
 
 namespace holor
 

src/data/pfunctor/multivariate/basic.lean

@@ -37,7 +37,7 @@ def map {α β : typevec n} (f : α ⟹ β) : P.obj α → P.obj β :=
 λ ⟨a, g⟩, ⟨a, typevec.comp f g⟩
 
 instance : inhabited (mvpfunctor n) :=
-⟨ ⟨default, λ _, default⟩ ⟩
+⟨⟨default, default⟩⟩
 
 instance obj.inhabited {α : typevec n} [inhabited P.A] [Π i, inhabited (α i)] :
   inhabited (P.obj α) :=

src/data/pfunctor/univariate/M.lean

@@ -170,7 +170,7 @@ lemma M.default_consistent [inhabited F.A] :
 | (succ n) := agree.intro _ _ $ λ _, M.default_consistent n
 
 instance M.inhabited [inhabited F.A] : inhabited (M F) :=
-⟨ { approx := λ n, default,
+⟨ { approx := default,
     consistent := M.default_consistent _ } ⟩
 
 instance M_intl.inhabited [inhabited F.A] : inhabited (M_intl F) :=

src/data/pfunctor/univariate/basic.lean

@@ -41,8 +41,7 @@ def obj (α : Type*) := Σ x : P.A, P.B x → α
 def map {α β : Type*} (f : α → β) : P.obj α → P.obj β :=
 λ ⟨a, g⟩, ⟨a, f ∘ g⟩
 
-instance obj.inhabited [inhabited P.A] [inhabited α] : inhabited (P.obj α) :=
-⟨ ⟨ default, λ _, default ⟩ ⟩
+instance obj.inhabited [inhabited P.A] [inhabited α] : inhabited (P.obj α) := ⟨⟨default, default⟩⟩
 instance : functor P.obj := {map := @map P}
 
 protected theorem map_eq {α β : Type*} (f : α → β) (a : P.A) (g : P.B a → α) :
@@ -99,7 +98,7 @@ one part of `x` or is invalid, if `i.1 ≠ x.1` -/
 def Idx := Σ x : P.A, P.B x
 
 instance Idx.inhabited [inhabited P.A] [inhabited (P.B default)] : inhabited P.Idx :=
-⟨ ⟨default, default⟩ ⟩
+⟨⟨default, default⟩⟩
 
 variables {P}
 

src/data/prod/tprod.lean

@@ -57,7 +57,7 @@ protected def mk : ∀ (l : list ι) (f : Π i, α i), tprod α l
 | (i :: is) := λ f, (f i, mk is f)
 
 instance [∀ i, inhabited (α i)] : inhabited (tprod α l) :=
-⟨tprod.mk l (λ _, default)⟩
+⟨tprod.mk l default⟩
 
 @[simp] lemma fst_mk (i : ι) (l : list ι) (f : Π i, α i) : (tprod.mk (i::l) f).1 = f i := rfl
 

src/data/qpf/multivariate/constructions/sigma.lean

@@ -30,10 +30,10 @@ def pi (v : typevec.{u} n) : Type.{u} :=
 Π α : A, F α v
 
 instance sigma.inhabited {α} [inhabited A] [inhabited (F default α)] : inhabited (sigma F α) :=
-⟨ ⟨default, default⟩ ⟩
+⟨⟨default, default⟩⟩
 
 instance pi.inhabited {α} [Π a, inhabited (F a α)] : inhabited (pi F α) :=
-⟨ λ a, default ⟩
+⟨λ a, default⟩
 
 variables [Π α, mvfunctor $ F α]
 

src/data/setoid/partition.lean

@@ -291,9 +291,9 @@ variables {ι α : Type*} {s : ι → set α} (hs : indexed_partition s)
 instance [unique ι] [inhabited α] :
   inhabited (indexed_partition (λ i : ι, (set.univ : set α))) :=
 ⟨{ eq_of_mem := λ x i j hi hj, subsingleton.elim _ _,
-   some := λ i, default,
+   some := default,
    some_mem := set.mem_univ,
-   index := λ a, default,
+   index := default,
    mem_index := set.mem_univ }⟩
 
 attribute [simp] some_mem mem_index

src/data/vector/basic.lean

@@ -23,7 +23,7 @@ infixr `::ᵥ`:67  := vector.cons
 attribute [simp] head_cons tail_cons
 
 instance [inhabited α] : inhabited (vector α n) :=
-⟨of_fn (λ _, default)⟩
+⟨of_fn default⟩
 
 theorem to_list_injective : function.injective (@to_list α n) :=
 subtype.val_injective

src/group_theory/sylow.lean

@@ -626,7 +626,7 @@ begin
   set ps := (fintype.card G).factorization.support,
 
   -- “The” sylow group for p
-  let P : Π p, sylow p G := λ _, default,
+  let P : Π p, sylow p G := default,
 
   have hcomm : pairwise (λ (p₁ p₂ : ps), ∀ (x y : G), x ∈ P p₁ → y ∈ P p₂ → commute x y),
   { rintros ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne,

src/logic/basic.lean

@@ -50,8 +50,8 @@ instance subsingleton.prod {α β : Type*} [subsingleton α] [subsingleton β] :
 
 instance : decidable_eq empty := λa, a.elim
 
-instance sort.inhabited : inhabited (Sort*) := ⟨punit⟩
-instance sort.inhabited' : inhabited (default) := ⟨punit.star⟩
+instance sort.inhabited : inhabited Sort* := ⟨punit⟩
+instance sort.inhabited' : inhabited default := ⟨punit.star⟩
 
 instance psum.inhabited_left {α β} [inhabited α] : inhabited (psum α β) := ⟨psum.inl default⟩
 instance psum.inhabited_right {α β} [inhabited β] : inhabited (psum α β) := ⟨psum.inr default⟩

src/logic/embedding.lean

@@ -286,7 +286,7 @@ This embedding sends each `f : α → γ` to a function `g : β → γ` such tha
 `g y = default` whenever `y ∉ range e`. -/
 noncomputable def arrow_congr_left {α : Sort u} {β : Sort v} {γ : Sort w} [inhabited γ]
   (e : α ↪ β) : (α → γ) ↪ (β → γ) :=
-⟨λ f, extend e f (λ _, default), λ f₁ f₂ h, funext $ λ x,
+⟨λ f, extend e f default, λ f₁ f₂ h, funext $ λ x,
   by simpa only [extend_apply e.injective] using congr_fun h (e x)⟩
 
 /-- Restrict both domain and codomain of an embedding. -/

src/logic/equiv/basic.lean

@@ -2014,8 +2014,8 @@ funext $ λ z, hf.swap_apply _ _ _
 
 /-- If both `α` and `β` are singletons, then `α ≃ β`. -/
 def equiv_of_unique_of_unique [unique α] [unique β] : α ≃ β :=
-{ to_fun := λ _, default,
-  inv_fun := λ _, default,
+{ to_fun := default,
+  inv_fun := default,
   left_inv := λ _, subsingleton.elim _ _,
   right_inv := λ _, subsingleton.elim _ _ }
 

src/logic/unique.lean

@@ -178,7 +178,7 @@ end function
 lemma unique.bijective {A B} [unique A] [unique B] {f : A → B} : function.bijective f :=
 begin
   rw function.bijective_iff_has_inverse,
-  refine ⟨λ x, default, _, _⟩; intro x; simp
+  refine ⟨default, _, _⟩; intro x; simp
 end
 
 namespace option

src/measure_theory/covering/besicovitch.lean

@@ -139,7 +139,7 @@ class has_besicovitch_covering (α : Type*) [metric_space α] : Prop :=
 /-- There is always a satellite configuration with a single point. -/
 instance {α : Type*} {τ : ℝ} [inhabited α] [metric_space α] :
   inhabited (besicovitch.satellite_config α 0 τ) :=
-⟨{ c := λ i, default,
+⟨{ c := default,
   r := λ i, 1,
   rpos := λ i, zero_lt_one,
   h := λ i j hij, (hij (subsingleton.elim i j)).elim,

src/order/jordan_holder.lean

@@ -147,7 +147,7 @@ instance : has_coe_to_fun (composition_series X) (λ x, fin (x.length + 1) → X
 
 instance [inhabited X] : inhabited (composition_series X) :=
 ⟨{ length := 0,
-   series := λ _, default,
+   series := default,
    step' := λ x, x.elim0 }⟩
 
 variables {X}

src/order/omega_complete_partial_order.lean

@@ -97,10 +97,10 @@ variables [preorder α] [preorder β] [preorder γ]
 instance : has_coe_to_fun (chain α) (λ _, ℕ → α) := order_hom.has_coe_to_fun
 
 instance [inhabited α] : inhabited (chain α) :=
-⟨ ⟨ λ _, default, λ _ _ _, le_rfl ⟩ ⟩
+⟨⟨default, λ _ _ _, le_rfl⟩⟩
 
 instance : has_mem α (chain α) :=
-⟨λa (c : ℕ →o α), ∃ i, a = c i⟩
+⟨λ a (c : ℕ →o α), ∃ i, a = c i⟩
 
 variables (c c' : chain α)
 variables (f : α →o β)

src/topology/continuous_function/basic.lean

@@ -96,9 +96,6 @@ protected lemma congr_fun {f g : C(α, β)} (H : f = g) (x : α) : f x = g x :=
 /-- Deprecated. Use `fun_like.congr_arg` instead. -/
 protected lemma congr_arg (f : C(α, β)) {x y : α} (h : x = y) : f x = f y := h ▸ rfl
 
-instance [inhabited β] : inhabited C(α, β) :=
-⟨{ to_fun := λ _, default, }⟩
-
 lemma coe_injective : @function.injective (C(α, β)) (α → β) coe_fn :=
 λ f g h, by cases f; cases g; congr'
 
@@ -132,6 +129,9 @@ def const (b : β) : C(α, β) := ⟨const α b⟩
 
 @[simp] lemma coe_const (b : β) : ⇑(const α b) = function.const α b := rfl
 
+instance [inhabited β] : inhabited C(α, β) :=
+⟨const α default⟩
+
 variables {α}
 
 @[simp] lemma id_apply (a : α) : continuous_map.id α a = a := rfl

src/topology/vector_bundle/basic.lean

@@ -727,7 +727,7 @@ def trivial_topological_vector_bundle_core (ι : Type*) [inhabited ι] :
   topological_vector_bundle_core R B F ι :=
 { base_set := λ ι, univ,
   is_open_base_set := λ i, is_open_univ,
-  index_at := λ x, default,
+  index_at := default,
   mem_base_set_at := λ x, mem_univ x,
   coord_change := λ i j x, continuous_linear_map.id R F,
   coord_change_self := λ i x hx v, rfl,

test/lint_coe_t.lean

@@ -27,7 +27,7 @@ skip
 -- bad, because it introduces a metavariable
 section
 local attribute [instance]
-def int_to_a {α} [inhabited α] : has_coe ℤ α := ⟨λ _, default⟩
+def int_to_a {α} [inhabited α] : has_coe ℤ α := ⟨default⟩
 
 run_cmd do
 decl ← get_decl ``int_to_a,