Tensor Adic Completion Integers To range subset closure

lemma tensorAdicCompletionIntegersTo_range_subset_closure [FiniteDimensional K L] :  (tensorAdicCompletionIntegersTo K L B v).range.carrier ⊆    closure (algebraMap B (L ⊗[K] adicCompletion K v)).range := by  rintro _ ⟨s, rfl⟩  induction s with    | zero =>        apply subset_closure        use 0        simp    | add x y hx hy =>        -- The closure of a subgroup is a subgroup        rw [RingHom.map_add]        apply map_mem_closure₂ _ hx hy _        · exact (ModuleTopology.continuousAdd _ _).continuous_add        intro _ ha _ hb        exact add_mem ha hb    | tmul b a' =>        -- Rewrite `tensorAdicCompletionTo (b ⊗ₜ a')` to `b • (1 ⊗ₜ a')`        simp only [RingHom.coe_range, tensorAdicCompletionIntegersTo,          AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.lift_tmul,          AlgHom.coe_comp, AlgHom.coe_restrictScalars', IsScalarTower.coe_toAlgHom',          Function.comp_apply, ValuationSubring.algebraMap_apply,          Algebra.TensorProduct.includeRight_apply]        -- Now, `f : a' ↦ b • (1 ⊗ₜ a')` is continuous        let f (y : ↥(adicCompletionIntegers K v)) : (L ⊗[K] adicCompletion K v) :=          (Algebra.ofId B (L ⊗[K] adicCompletion K v)) b * (1 : L) ⊗ₜ[K] (y : adicCompletion K v)        have hfval : f = fun (y : ↥(adicCompletionIntegers K v)) =>              (y : adicCompletion K v) • (Algebra.ofId B (L ⊗[K] adicCompletion K v)) b := by          ext y          unfold f          rw [Algebra.smul_def]          exact mul_comm _ _        have hcf : ContinuousAt f a' := by          rw [hfval]          fun_prop        -- So, because `A` is dense in `𝒪_v`, `b • (1 ⊗ₜ a') ∈ f '' closure A ⊆ closure f '' A`        have hy : a' ∈ closure (Set.range (algebraMap A _)) := by          apply denseRange_of_integerAlgebraMap        apply mem_closure_image hcf hy        constructor        · exact isClosed_closure        -- Finally, `b • (1 ⊗ₜ a) = (b * a) • (1 ⊗ₜ 1)`, so `f '' A ⊆ algebraMap '' B`        rintro u ⟨_, ⟨a, rfl⟩, rfl⟩        apply subset_closure        use algebraMap A B a * b        unfold f        rw [Algebra.algebraMap_eq_smul_one (A := (adicCompletionIntegers K v)) a,          coe_smul_adicCompletionIntegers, ← TensorProduct.smul_tmul, Algebra.ofId_apply,          Algebra.TensorProduct.algebraMap_apply, RingHom.map_mul, ← Algebra.smul_def]        simp