chore(*): add a few more unique instances (#4511)

* `linear_map.unique_of_left`, `linear_map.unique_of_right`,
  `continuous_linear_map.unique_of_left`,
  `continuous_linear_map.unique_of_right`: if either `M` or `M₂` is a
  `subsingleton`, then both `M →ₗ[R] M₂` and `M →L[R] M₂` are
  `unique`;
* `pi.unique`: if each `β a` is `unique`, then `Π a, β a` is `unique`;
* rename `function.injective.comap_subsingleton` to
  `function.injective.subsingleton`;
* add `unique.mk'` and `function.injective.unique`;
* add a few `simp` lemmas for `default`;
* drop `nonempty_unique_or_exists_ne` and `subsingleton_or_exists_ne`;
* rename `linear_map.coe_inj` to `coe_injective` and `continuous_linear_map.coe_inj` to `coe_fn_injective`,
  make them use `function.injective`.

Motivated by #4407

src/algebra/category/Module/limits.lean

@@ -82,7 +82,7 @@ def limit_cone (F : J ⥤ Module R) : cone F :=
   π :=
   { app := limit_π_linear_map F,
     naturality' := λ j j' f,
-      linear_map.coe_inj ((types.limit_cone (F ⋙ forget _)).π.naturality f) } }
+      linear_map.coe_injective ((types.limit_cone (F ⋙ forget _)).π.naturality f) } }
 
 /--
 Witness that the limit cone in `Module R` is a limit cone.

src/algebra/module/basic.lean

@@ -291,18 +291,19 @@ section
 -- rather than via typeclass resolution.
 variables {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂}
 variables (f g : M →ₗ[R] M₂)
+include semimodule_M semimodule_M₂
 
 @[simp] lemma to_fun_eq_coe : f.to_fun = ⇑f := rfl
 
 theorem is_linear : is_linear_map R f := ⟨f.2, f.3⟩
 
 variables {f g}
 
-theorem coe_inj (h : (f : M → M₂) = g) : f = g :=
-by cases f; cases g; cases h; refl
+theorem coe_injective : injective (λ f : M →ₗ[R] M₂, show M → M₂, from f) :=
+by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr
 
 @[ext] theorem ext (H : ∀ x, f x = g x) : f = g :=
-coe_inj $ funext H
+coe_injective $ funext H
 
 lemma coe_fn_congr : Π {x x' : M}, x = x' → f x = f x'
 | _ _ rfl := rfl
@@ -340,9 +341,9 @@ def to_add_monoid_hom : M →+ M₂ :=
   f (∑ i in t, g i) = (∑ i in t, f (g i)) :=
 f.to_add_monoid_hom.map_sum _ _
 
-theorem to_add_monoid_hom_injective [semimodule R M] [semimodule R M₂] :
+theorem to_add_monoid_hom_injective :
   function.injective (to_add_monoid_hom : (M →ₗ[R] M₂) → (M →+ M₂)) :=
-λ f g h, coe_inj $ funext $ add_monoid_hom.congr_fun h
+λ f g h, ext $ add_monoid_hom.congr_fun h
 
 end
 

src/analysis/calculus/times_cont_diff.lean

@@ -329,8 +329,7 @@ begin
   change (p x 1) (snoc 0 y) = (p x 1) (cons y v),
   unfold_coes,
   congr' with i,
-  have : i = 0 := subsingleton.elim i 0,
-  rw this,
+  rw unique.eq_default i,
   refl
 end
 
@@ -2362,9 +2361,8 @@ begin
   -- `E →L[𝕜] E`
   let O₁ : (E →L[𝕜] E) → (F →L[𝕜] E) := λ f, f.comp (e.symm : (F →L[𝕜] E)),
   let O₂ : (E →L[𝕜] F) → (E →L[𝕜] E) := λ f, (e.symm : (F →L[𝕜] E)).comp f,
-  have : continuous_linear_map.inverse = O₁ ∘ ring.inverse ∘ O₂,
-  { funext f,
-    rw to_ring_inverse e},
+  have : continuous_linear_map.inverse = O₁ ∘ ring.inverse ∘ O₂ :=
+    funext (to_ring_inverse e),
   rw this,
   -- `O₁` and `O₂` are `times_cont_diff`, so we reduce to proving that `ring.inverse` is `times_cont_diff`
   have h₁ : times_cont_diff 𝕜 n O₁,
@@ -2375,9 +2373,8 @@ begin
   -- this works differently depending on whether or not `E` is `nontrivial` (the condition for
   -- `E →L[𝕜] E` to be a `normed_algebra`)
   cases subsingleton_or_nontrivial E with _i _i; resetI,
-  { convert @times_cont_diff_at_const _ _ _ _ _ _ _ _ _ _ (0 :  E →L[𝕜] E),
-    ext,
-    simp },
+  { rw [subsingleton.elim ring.inverse (λ _, (0 : E →L[𝕜] E))],
+    exact times_cont_diff_at_const },
   { convert times_cont_diff_at_ring_inverse 𝕜 (E →L[𝕜] E) 1,
     simp [O₂],
     refl },

src/analysis/normed_space/operator_norm.lean

@@ -566,7 +566,7 @@ have eq : _ := uniformly_extend_of_ind h_e h_dense f.uniform_continuous,
 }
 
 lemma extend_unique (g : G →L[𝕜] F) (H : g.comp e = f) : extend f e h_dense h_e = g :=
-continuous_linear_map.coe_inj $
+continuous_linear_map.coe_fn_injective $
   uniformly_extend_unique h_e h_dense (continuous_linear_map.ext_iff.1 H) g.continuous
 
 @[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) e h_dense h_e = 0 :=

src/data/equiv/basic.lean

@@ -137,7 +137,7 @@ protected theorem bijective (f : α ≃ β) : bijective f :=
 set.eq_univ_of_forall e.surjective
 
 protected theorem subsingleton (e : α ≃ β) [subsingleton β] : subsingleton α :=
-e.injective.comap_subsingleton
+e.injective.subsingleton
 
 /-- Transfer `decidable_eq` across an equivalence. -/
 protected def decidable_eq (e : α ≃ β) [decidable_eq β] : decidable_eq α :=

src/geometry/euclidean/basic.lean

@@ -474,6 +474,8 @@ lemma eq_of_dist_eq_of_dist_eq_of_mem_of_findim_eq_two {s : affine_subspace ℝ
 begin
   have ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
     inner_vsub_vsub_of_dist_eq_of_dist_eq (by cc) (by cc),
+  have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 :=
+    inner_vsub_vsub_of_dist_eq_of_dist_eq (by cc) (by cc),
   let b : fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁],
   have hb : linear_independent ℝ b,
   { refine linear_independent_of_ne_zero_of_inner_eq_zero _ _,
@@ -504,8 +506,6 @@ begin
     rcases hv' with ⟨t₂, rfl⟩,
     exact ⟨t₁, t₂, hv⟩ },
   rcases hv (p -ᵥ p₁) (vsub_mem_direction hps hp₁s) with ⟨t₁, t₂, hpt⟩,
-  have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 :=
-    inner_vsub_vsub_of_dist_eq_of_dist_eq (by cc) (by cc),
   simp only [hpt, inner_add_right, inner_smul_right, ho, mul_zero, add_zero, mul_eq_zero,
              inner_self_eq_zero, vsub_eq_zero_iff_eq, hc.symm, or_false] at hop,
   rw [hop, zero_smul, zero_add, ←eq_vadd_iff_vsub_eq] at hpt,

src/linear_algebra/basic.lean

@@ -161,6 +161,15 @@ instance : inhabited (M →ₗ[R] M₂) := ⟨0⟩
 
 @[simp] lemma zero_apply (x : M) : (0 : M →ₗ[R] M₂) x = 0 := rfl
 
+@[simp] lemma default_def : default (M →ₗ[R] M₂) = 0 := rfl
+
+instance unique_of_left [subsingleton M] : unique (M →ₗ[R] M₂) :=
+{ uniq := λ f, ext $ λ x, by rw [subsingleton.elim x 0, map_zero, map_zero],
+  .. linear_map.inhabited }
+
+instance unique_of_right [subsingleton M₂] : unique (M →ₗ[R] M₂) :=
+coe_injective.unique
+
 /-- The sum of two linear maps is linear. -/
 instance : has_add (M →ₗ[R] M₂) :=
 ⟨λ f g, ⟨λ b, f b + g b, by simp [add_comm, add_left_comm], by simp [smul_add]⟩⟩

src/logic/unique.lean

@@ -16,14 +16,26 @@ In other words, a type that is `inhabited` and a `subsingleton`.
 
 * `unique`: a typeclass that expresses that a type has a unique term.
 
+## Main statements
+
+* `unique.mk'`: an inhabited subsingleton type is `unique`. This can not be an instance because it
+  would lead to loops in typeclass inference.
+
+* `function.surjective.unique`: if the domain of a surjective function is `unique`, then its
+  codomain is `unique` as well.
+
+* `function.injective.subsingleton`: if the codomain of an injective function is `subsingleton`,
+  then its domain is `subsingleton` as well.
+
+* `function.injective.unique`: if the codomain of an injective function is `subsingleton` and its
+  domain is `inhabited`, then its domain is `unique`.
+
 ## Implementation details
 
 The typeclass `unique α` is implemented as a type,
 rather than a `Prop`-valued predicate,
 for good definitional properties of the default term.
 
-There can not be an instance for `inhabited α` + `subsingleton α` to `unique α`
-because it would lead to loops in typeclass inference.
 -/
 
 universes u v w
@@ -74,38 +86,49 @@ lemma exists_iff {p : α → Prop} : Exists p ↔ p (default α) :=
 
 end
 
-protected lemma subsingleton_unique' : ∀ (h₁ h₂ : unique α), h₁ = h₂
+@[ext] protected lemma subsingleton_unique' : ∀ (h₁ h₂ : unique α), h₁ = h₂
 | ⟨⟨x⟩, h⟩ ⟨⟨y⟩, _⟩ := by congr; rw [h x, h y]
 
 instance subsingleton_unique : subsingleton (unique α) :=
 ⟨unique.subsingleton_unique'⟩
 
+/-- Construct `unique` from `inhabited` and `subsingleton`. Making this an instance would create
+a loop in the class inheritance graph. -/
+def mk' (α : Sort u) [h₁ : inhabited α] [subsingleton α] : unique α :=
+{ uniq := λ x, subsingleton.elim _ _, .. h₁ }
+
 end unique
 
+@[simp] lemma pi.default_def {β : Π a : α, Sort v} [Π a, inhabited (β a)] :
+  default (Π a, β a) = λ a, default (β a) :=
+rfl
+
+lemma pi.default_apply {β : Π a : α, Sort v} [Π a, inhabited (β a)] (a : α) :
+  default (Π a, β a) a = default (β a) :=
+rfl
+
+instance pi.unique {β : Π a : α, Sort v} [Π a, unique (β a)] : unique (Π a, β a) :=
+{ uniq := λ f, funext $ λ x, unique.eq_default _,
+  .. pi.inhabited α }
+
 namespace function
 
 variable {f : α → β}
 
 /-- If the domain of a surjective function is a singleton,
 then the codomain is a singleton as well. -/
-def surjective.unique (hf : surjective f) [unique α] : unique β :=
+protected def surjective.unique (hf : surjective f) [unique α] : unique β :=
 { default := f (default _),
   uniq := λ b, let ⟨a, ha⟩ := hf b in ha ▸ congr_arg f (unique.eq_default _) }
 
 /-- If the codomain of an injective function is a subsingleton, then the domain
 is a subsingleton as well. -/
-lemma injective.comap_subsingleton (hf : injective f) [subsingleton β] :
+protected lemma injective.subsingleton (hf : injective f) [subsingleton β] :
   subsingleton α :=
 ⟨λ x y, hf $ subsingleton.elim _ _⟩
 
-end function
-
-lemma nonempty_unique_or_exists_ne (x : α) : nonempty (unique α) ∨ ∃ y, y ≠ x :=
-classical.by_cases or.inr
-  (λ h, or.inl ⟨{ default := x,
-    uniq := λ y, classical.by_contradiction $ λ hy, h ⟨y, hy⟩ }⟩)
+/-- If `α` is inhabited and admits an injective map to a subsingleton type, then `α` is `unique`. -/
+protected def injective.unique [inhabited α] [subsingleton β] (hf : injective f) : unique α :=
+@unique.mk' _ _ hf.subsingleton
 
-lemma subsingleton_or_exists_ne (x : α) : subsingleton α ∨ ∃ y, y ≠ x :=
-(nonempty_unique_or_exists_ne x).elim
-  (λ ⟨h⟩, or.inl $ @unique.subsingleton _ h)
-  or.inr
+end function

src/ring_theory/derivation.lean

@@ -58,7 +58,7 @@ lemma coe_fn_coe (f : derivation R A M) :
   ⇑(f : A →ₗ[R] M) = f := rfl
 
 lemma coe_injective (H : ⇑D1 = D2) : D1 = D2 :=
-by { cases D1, cases D2, congr', exact linear_map.coe_inj H }
+by { cases D1, cases D2, congr', exact linear_map.coe_injective H }
 
 @[ext] theorem ext (H : ∀ a, D1 a = D2 a) : D1 = D2 :=
 coe_injective $ funext H

src/topology/algebra/module.lean

@@ -217,11 +217,11 @@ protected lemma continuous (f : M →L[R] M₂) : continuous f := f.2
 theorem coe_injective : function.injective (coe : (M →L[R] M₂) → (M →ₗ[R] M₂)) :=
 by { intros f g H, cases f, cases g, congr' 1, exact H }
 
-theorem coe_inj ⦃f g : M →L[R] M₂⦄ (H : (f : M → M₂) = g) : f = g :=
-coe_injective $ linear_map.coe_inj H
+theorem coe_fn_injective : function.injective (λ f : M →L[R] M₂, show M → M₂, from f) :=
+linear_map.coe_injective.comp coe_injective
 
 @[ext] theorem ext {f g : M →L[R] M₂} (h : ∀ x, f x = g x) : f = g :=
-coe_inj $ funext h
+coe_fn_injective $ funext h
 
 theorem ext_iff {f g : M →L[R] M₂} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, by rw h, by ext⟩
@@ -242,13 +242,20 @@ lemma map_sum {ι : Type*} (s : finset ι) (g : ι → M) :
 instance: has_zero (M →L[R] M₂) := ⟨⟨0, continuous_const⟩⟩
 instance : inhabited (M →L[R] M₂) := ⟨0⟩
 
+@[simp] lemma default_def : default (M →L[R] M₂) = 0 := rfl
 @[simp] lemma zero_apply : (0 : M →L[R] M₂) x = 0 := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : M →L[R] M₂) : M →ₗ[R] M₂) = 0 := rfl
 /- no simp attribute on the next line as simp does not always simplify `0 x` to `0`
 when `0` is the zero function, while it does for the zero continuous linear map,
 and this is the most important property we care about. -/
 @[norm_cast] lemma coe_zero' : ((0 : M →L[R] M₂) : M → M₂) = 0 := rfl
 
+instance unique_of_left [subsingleton M] : unique (M →L[R] M₂) :=
+coe_injective.unique
+
+instance unique_of_right [subsingleton M₂] : unique (M →L[R] M₂) :=
+coe_injective.unique
+
 section
 
 variables (R M)