feat(data/finsupp): Make finsupp.dom_congr a ≃+ (#4398)

Since this has additional structure, it may as well be part of the type

src/data/finsupp/basic.lean

@@ -1591,18 +1591,20 @@ end
 
 /-- Given `add_comm_monoid β` and `e : α₁ ≃ α₂`, `dom_congr e` is the corresponding `equiv` between
 `α₁ →₀ β` and `α₂ →₀ β`. -/
-protected def dom_congr [add_comm_monoid β] (e : α₁ ≃ α₂) : (α₁ →₀ β) ≃ (α₂ →₀ β) :=
-⟨map_domain e, map_domain e.symm,
-  begin
+protected def dom_congr [add_comm_monoid β] (e : α₁ ≃ α₂) : (α₁ →₀ β) ≃+ (α₂ →₀ β) :=
+{ to_fun := map_domain e,
+  inv_fun := map_domain e.symm,
+  left_inv := begin
     assume v,
     simp only [map_domain_comp.symm, (∘), equiv.symm_apply_apply],
     exact map_domain_id
   end,
-  begin
+  right_inv := begin
     assume v,
     simp only [map_domain_comp.symm, (∘), equiv.apply_symm_apply],
     exact map_domain_id
-  end⟩
+  end,
+  map_add' := λ a b, map_domain_add, }
 
 /-! ### Declarations about sigma types -/
 

src/linear_algebra/basic.lean

@@ -2275,6 +2275,23 @@ def to_linear_equiv (e : M ≃ M₂) (h : is_linear_map R (e : M → M₂)) : M
 
 end equiv
 
+namespace add_equiv
+variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid M₂] [semimodule R M₂]
+
+/-- An additive equivalence whose underlying function preserves `smul` is a linear equivalence. -/
+def to_linear_equiv (e : M ≃+ M₂) (h : ∀ (c : R) x, e (c • x) = c • e x) : M ≃ₗ[R] M₂ :=
+{ map_smul' := h, .. e, }
+
+@[simp] lemma coe_to_linear_equiv (e : M ≃+ M₂) (h : ∀ (c : R) x, e (c • x) = c • e x) :
+  ⇑(e.to_linear_equiv h) = e :=
+rfl
+
+@[simp] lemma coe_to_linear_equiv_symm (e : M ≃+ M₂) (h : ∀ (c : R) x, e (c • x) = c • e x) :
+  ⇑(e.to_linear_equiv h).symm = e.symm :=
+rfl
+
+end add_equiv
+
 namespace linear_map
 
 open submodule

src/linear_algebra/finsupp.lean

@@ -418,15 +418,11 @@ end total
 protected def dom_lcongr
   {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) :
   (α₁ →₀ M) ≃ₗ[R] (α₂ →₀ M) :=
-(finsupp.dom_congr e).to_linear_equiv
-begin
-  change is_linear_map R (lmap_domain M R e : (α₁ →₀ M) →ₗ[R] (α₂ →₀ M)),
-  exact linear_map.is_linear _
-end
+(@finsupp.dom_congr M _ _ _ e).to_linear_equiv (lmap_domain M R e).map_smul
 
 @[simp] theorem dom_lcongr_single {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (i : α₁) (m : M) :
   (finsupp.dom_lcongr e : _ ≃ₗ[R] _) (finsupp.single i m) = finsupp.single (e i) m :=
-by simp [finsupp.dom_lcongr, equiv.to_linear_equiv, finsupp.dom_congr, map_domain_single]
+by simp [finsupp.dom_lcongr, finsupp.dom_congr, map_domain_single]
 
 noncomputable def congr {α' : Type*} (s : set α) (t : set α') (e : s ≃ t) :
   supported M R s ≃ₗ[R] supported M R t :=