Tensor Adic Completion Integers To Adic Completion range eq integers

lemma tensorAdicCompletionIntegersToAdicCompletion_range_eq_integers [FiniteDimensional K L] :    Set.range (w.tensorAdicCompletionIntegersToAdicCompletion K L B v) =      adicCompletionIntegers L w.1 := by  ext x  have memrange := (range_baseChange_comp_tensorAdicCompletionTo_eq_pi K L B v)  rw [Set.ext_iff] at memrange  constructor  · rintro ⟨y, rfl⟩    exact (memrange _).mp (Set.mem_range_self y) w trivial  · intro hx    classical    set x' : (w : Extension B v) → adicCompletion L w.val := Pi.single w x with hx'    obtain ⟨y, (hy : _ = x')⟩ : x' ∈ Set.range _ := by      rw [memrange x', Set.mem_pi]      intro w' _      by_cases h : w = w'      · rw [← h, hx', Pi.single_eq_same]        exact hx      · rw [hx', Pi.single_eq_of_ne' h]        exact Subring.zero_mem _    use y    simpa [hx'] using! congr_fun hy w