feat(linear_algebra/finsupp): adjust apply lemma for `finsupp.dom_lco…

…ngr` (#7549)

This is a split-off dependency from #7496.





Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

src/linear_algebra/basis.lean

@@ -250,7 +250,7 @@ funext (b.reindex_apply e)
 @[simp] lemma coe_reindex_repr : ((b.reindex e).repr x : ι' → R) = b.repr x ∘ e.symm :=
 funext $ λ i',
 show (finsupp.dom_lcongr e : _ ≃ₗ[R] _) (b.repr x) i' = _,
-from finsupp.dom_lcongr_apply _ _ _
+by simp
 
 @[simp] lemma reindex_repr (i' : ι') : (b.reindex e).repr x i' = b.repr x (e.symm i') :=
 by rw coe_reindex_repr

src/linear_algebra/finsupp.lean

@@ -550,10 +550,10 @@ protected def dom_lcongr {α₁ α₂ : Type*} (e : α₁ ≃ α₂) :
   (α₁ →₀ M) ≃ₗ[R] (α₂ →₀ M) :=
 (finsupp.dom_congr e : (α₁ →₀ M) ≃+ (α₂ →₀ M)).to_linear_equiv (lmap_domain M R e).map_smul
 
-lemma dom_lcongr_apply {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (v : α₁ →₀ M) (i : α₂) :
-  (finsupp.dom_lcongr e : _ ≃ₗ[R] _) v i = v (e.symm i) :=
-by { conv_lhs { rw ← e.apply_symm_apply i },
-     exact finsupp.map_domain_apply e.injective v (e.symm i) }
+@[simp]
+lemma dom_lcongr_apply {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (v : α₁ →₀ M) :
+  (finsupp.dom_lcongr e : _ ≃ₗ[R] _) v = finsupp.dom_congr e v :=
+rfl
 
 @[simp]
 lemma dom_lcongr_refl : finsupp.dom_lcongr (equiv.refl α) = linear_equiv.refl R (α →₀ M) :=