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

Author: vihdzp

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