Tensor Adic Completion Integers To is Clopen range

lemma tensorAdicCompletionIntegersTo_isClopen_range    [IsIntegralClosure B A L] [FiniteDimensional K L] :    IsClopen (SetLike.coe (tensorAdicCompletionIntegersTo K L B v).range) := by  -- `B ⊗[A] 𝒪_v` is a subgroup of `L ⊗[K] K_v`, so we can show it's closed  -- by showing that it's open. **TODO** split into IsOpen + IsClosed lemmas?  have : SeparatelyContinuousAdd (L ⊗[K] v.adicCompletion K) :=    instSeparatelyContinuousAddOfContinuousAdd  rw [← Subalgebra.coe_toSubring, ← Subring.coe_toAddSubgroup]  refine OpenAddSubgroup.isClopen ⟨_, ?_⟩  -- Further, we can show `B ⊗[A] 𝒪_v` is open by showing that it contains an  -- open neighbourhood of 0.  apply AddSubgroup.isOpen_of_zero_mem_interior  rw [mem_interior, Subring.coe_toAddSubgroup, Subalgebra.coe_toSubring]  -- Take a basis `b` of `L` over `K` with elements in `B` and use it to  -- get a basis `b'` of `L ⊗[K] K_v` over `K_v`.  obtain ⟨ι, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L  let b' : Module.Basis ι (adicCompletion K v) (L ⊗[K] (adicCompletion K v)) := by    classical    exact b.rightBaseChange L  -- Use the basis to get a continuous equivalence from `L ⊗[K] K_v` to `ι → K_v`.  let equiv : L ⊗[K] (adicCompletion K v) ≃L[v.adicCompletion K] (ι → adicCompletion K v) :=    IsModuleTopology.continuousLinearEquiv (b'.equivFun)  -- Use the preimage of `∏ 𝒪_v` as the open neighbourhood.  use equiv.symm '' (Set.pi Set.univ (fun _ => SetLike.coe (adicCompletionIntegers K v)))  refine ⟨?_, ?_, by simp⟩  · intro t ⟨g, hg, ht⟩    -- We have `t = equiv g = ∑ i, b i ⊗ g i`, since `g in ∏ 𝒪_v` and    -- `b i ∈ (algebraMap B L).range`, this is `tensorAdicCompletionTo`    -- of some element of `B ⊗[A] 𝒪_v`    have hf : ∀ (i : ι), ∃ (w : B), (algebraMap B L w) = (b i) := by      intro i      apply IsIntegralClosure.isIntegral_iff.mp (hb i)    choose f hf_prop using hf    let b : B ⊗[A] ↥(adicCompletionIntegers K v) := ∑ (i : ι), (f i) ⊗ₜ ⟨g i, hg i trivial⟩    use b    rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, map_sum, ← ht]    unfold equiv    rw [IsModuleTopology.continuousLinearEquiv_symm_apply, Module.Basis.equivFun_symm_apply]    apply Finset.sum_congr rfl    intro x    simp only [Finset.univ_eq_attach, Finset.mem_attach, tensorAdicCompletionIntegersTo_tmul,      hf_prop, Module.Basis.rightBaseChange_apply, Algebra.smul_def,      TensorProduct.RightActions.algebraMap_eval, Algebra.TensorProduct.tmul_mul_tmul, one_mul,      mul_one, imp_self, b']  · rw [ContinuousLinearEquiv.image_symm_eq_preimage]    apply IsOpen.preimage equiv.continuous    apply isOpen_set_pi Set.finite_univ    rintro i -    exact Valued.isOpen_valuationSubring (v.adicCompletion K)