diff --git a/src/computability/turing_machine.lean b/src/computability/turing_machine.lean index 05d26c6f167ef..0a69783e0f461 100644 --- a/src/computability/turing_machine.lean +++ b/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⟩ diff --git a/src/data/array/lemmas.lean b/src/data/array/lemmas.lean index 7b4821d5496eb..15745bf153213 100644 --- a/src/data/array/lemmas.lean +++ b/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 diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index 01f6663efb3a9..4e782bdae5bcb 100644 --- a/src/data/finset/basic.lean +++ b/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⟩), diff --git a/src/data/holor.lean b/src/data/holor.lean index 35699760c4404..db1692c6234fe 100644 --- a/src/data/holor.lean +++ b/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 diff --git a/src/data/pfunctor/multivariate/basic.lean b/src/data/pfunctor/multivariate/basic.lean index 823037162e2cb..1e0dacfdec7d7 100644 --- a/src/data/pfunctor/multivariate/basic.lean +++ b/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 α) := diff --git a/src/data/pfunctor/univariate/M.lean b/src/data/pfunctor/univariate/M.lean index cdcedad8b350e..0d7980a33d14c 100644 --- a/src/data/pfunctor/univariate/M.lean +++ b/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) := diff --git a/src/data/pfunctor/univariate/basic.lean b/src/data/pfunctor/univariate/basic.lean index fb0e3efaa3844..e4aeca9a721ca 100644 --- a/src/data/pfunctor/univariate/basic.lean +++ b/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} diff --git a/src/data/prod/tprod.lean b/src/data/prod/tprod.lean index a653cb6bcb69c..b89c8772ee701 100644 --- a/src/data/prod/tprod.lean +++ b/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 diff --git a/src/data/qpf/multivariate/constructions/sigma.lean b/src/data/qpf/multivariate/constructions/sigma.lean index 98bc5f1c1ace7..08b97bc1a285a 100644 --- a/src/data/qpf/multivariate/constructions/sigma.lean +++ b/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 α] diff --git a/src/data/setoid/partition.lean b/src/data/setoid/partition.lean index 8cf099452e55e..279e8a17421af 100644 --- a/src/data/setoid/partition.lean +++ b/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 diff --git a/src/data/vector/basic.lean b/src/data/vector/basic.lean index 006431584bc1b..7b15294ea58a4 100644 --- a/src/data/vector/basic.lean +++ b/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 diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean index 2c415b1f35256..e52d4635d128a 100644 --- a/src/group_theory/sylow.lean +++ b/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, diff --git a/src/logic/basic.lean b/src/logic/basic.lean index 9a54d9f8db2ef..70ce2b8cfbd63 100644 --- a/src/logic/basic.lean +++ b/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⟩ diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean index 448c3bfa3a16f..3e0865695a091 100644 --- a/src/logic/embedding.lean +++ b/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. -/ diff --git a/src/logic/equiv/basic.lean b/src/logic/equiv/basic.lean index db7a47806d83d..166212a8a70b7 100644 --- a/src/logic/equiv/basic.lean +++ b/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 _ _ } diff --git a/src/logic/unique.lean b/src/logic/unique.lean index bafbd62abe354..51b2ca6b58b2c 100644 --- a/src/logic/unique.lean +++ b/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 diff --git a/src/measure_theory/covering/besicovitch.lean b/src/measure_theory/covering/besicovitch.lean index a88727f55140d..f7a3932833f7a 100644 --- a/src/measure_theory/covering/besicovitch.lean +++ b/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, diff --git a/src/order/jordan_holder.lean b/src/order/jordan_holder.lean index c6578f9d88bce..0a80954db4fcb 100644 --- a/src/order/jordan_holder.lean +++ b/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} diff --git a/src/order/omega_complete_partial_order.lean b/src/order/omega_complete_partial_order.lean index cbd3fb890ebb2..471392a666fce 100644 --- a/src/order/omega_complete_partial_order.lean +++ b/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 β) diff --git a/src/topology/continuous_function/basic.lean b/src/topology/continuous_function/basic.lean index f724ec9f4acdc..7391a026f0cbb 100644 --- a/src/topology/continuous_function/basic.lean +++ b/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 diff --git a/src/topology/vector_bundle/basic.lean b/src/topology/vector_bundle/basic.lean index ff22ff6da84da..bd60b46499c68 100644 --- a/src/topology/vector_bundle/basic.lean +++ b/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, diff --git a/test/lint_coe_t.lean b/test/lint_coe_t.lean index 49c51e08fb61b..0a809d2f6e350 100644 --- a/test/lint_coe_t.lean +++ b/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,