Finite Adele Ring Aux f g local global

lemma FiniteAdeleRing.Aux.f_g_local_global    (φ : ((FiniteAdeleRing (𝓞 K) K) ⊗[K] B) ≃L[FiniteAdeleRing (𝓞 K) K]      (FiniteAdeleRing (𝓞 K) K) ⊗[K] B) :    g K (f K B φ) = ContinuousAddEquiv.restrictedProductCongrRight    (fun v ↦ e _ _ _ (FiniteAdeleRing.TensorProduct.localcomponentEquiv (𝓞 K) K B v φ))    (FiniteAdeleRing.Aux.almost_always_bijOn _ _ _) := by  ext1 r; ext1 v; ext1 j;  letI b₀ := Module.Free.chooseBasis K B  letI b := Module.Basis.baseChange (FiniteAdeleRing (𝓞 K) K) b₀  letI bLocal := Module.Basis.baseChange (v.adicCompletion K) b₀  let m := LinearMap.toMatrix b b φ.toLinearMap  dsimp [e]  rw [ContinuousAddEquiv.restrictedProductCongrRight_apply]  dsimp  simp only [← basis_eq K B v, map_sum, Finset.sum_apply]  conv_rhs =>    change ∑ c,      (ContinuousLinearEquiv.chooseBasisPiScalarRight' K (adicCompletion K v) B)      (φLocalKvLinear K B v φ (r v c • bLocal c)) j  have basis_repr_eq' {x : adicCompletion K v ⊗[K] B} :      bLocal.repr x      = (ContinuousLinearEquiv.chooseBasisPiScalarRight' K (v.adicCompletion K) B) x :=    basis_repr_eq K B v  have local_repr_eq (i j : Module.Free.ChooseBasisIndex K B) :      ((bLocal.repr (φLocalKvLinear K B v φ (bLocal j))) i) = (m i j) v := by    rw [← LinearMap.toMatrix_apply, localcomponent_matrix]  have hf : m = LinearMap.toMatrix' (f K B φ) := toMatrix_f K B φ  simp only [ ← basis_repr_eq', local_repr_eq, m, hf, g,    ContinuousAddEquiv.trans_apply, map_smul, Finsupp.coe_smul, Pi.smul_apply]  -- Up to here, what we have done is to simplify the RHS `e (localcomponent φ)` in terms of  -- the matrix rep of `φ`, which is the same as the matrix rep of `f φ` by `toMatrix_f` above.  -- What remains is to simplify `g`, i.e. to simplify `ContinuousAddEquiv.restrictedProductPi`.  set ψ := f K B φ  conv_lhs =>    change (ψ.toLinearEquiv.toLinearMap (fun j ↦ map (fun i t ↦ t j)      (Filter.Eventually.of_forall (fun _ _ _ ↦ by simp_all [AddSubgroup.mem_pi])) r) j) v    rw [← Matrix.toLin'_toMatrix' ψ.toLinearEquiv.toLinearMap]  have {f : Module.Free.ChooseBasisIndex K B → FiniteAdeleRing (𝓞 K) K} :      (∑ x, f x) v = ∑ x, f x v :=    -- general lemma    map_sum (RestrictedProduct.evalAddMonoidHom _ _) _ _  simp [-Matrix.toLin'_toMatrix', Matrix.mulVec, dotProduct, this, FiniteAdeleRing,    mul_comm (r v _) _]