-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
ixy : ι
left_1 : Membership.mem (γ := Finset ι) univ ixy
hixy_def :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)
hna' : IsNonarchimedean (R := ℝ) (α := K) (⇑(NormedField.toMulRingNorm K) : (a : K) → ℝ)
k : ι
hk :
  Norm.norm.{u_1} (E := K)
      (∑ x_1 : ι,
        HMul.hMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) x_1 : K)
          (∑ x : ι,
              HMul.hMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) x : K)
                ((((B.repr : (a : L) → ι →₀ K)
                          (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) x_1 : L) ((B : (a : ι) → L) x : L)) :
                        ι →₀ K) :
                      (a : ι) → K)
                    ixy :
                  K) :
            K)) ≤
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) k : K) *
      Norm.norm.{u_1} (E := K)
        (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) x : K)
            ((((B.repr : (a : L) → ι →₀ K)
                      (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) k : L) ((B : (a : ι) → L) x : L)) :
                    ι →₀ K) :
                  (a : ι) → K)
                ixy :
              K))
obtain :
  ∀ (k_1 : ι) (hk0 : Finset.Nonempty.{u_3} (α := ι) univ → Membership.mem (γ := Finset ι) univ k_1)
    (hk :
      LE.le (α := ℝ)
        ((NormedField.toMulRingNorm K : (a : K) → ℝ)
            (∑ i : ι,
              HSMul.hSMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
                ((((B.repr : (a : L) → ι →₀ K)
                          (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) k : L) ((B : (a : ι) → L) i : L)) :
                        ι →₀ K) :
                      (a : ι) → K)
                    ixy :
                  K)) :
          ℝ)
        ((NormedField.toMulRingNorm K : (a : K) → ℝ)
            (HSMul.hSMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) k_1 : K)
              ((((B.repr : (a : L) → ι →₀ K)
                        (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) k : L) ((B : (a : ι) → L) k_1 : L)) :
                      ι →₀ K) :
                    (a : ι) → K)
                  ixy :
                K)) :
          ℝ)),
    ∃ (k' : ι),
      Norm.norm.{u_1} (E := K)
          (∑ j : ι,
            HSMul.hSMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
              ((((B.repr : (a : L) → ι →₀ K)
                        (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) k : L) ((B : (a : ι) → L) j : L)) :
                      ι →₀ K) :
                    (a : ι) → K)
                  ixy :
                K)) ≤
        ‖HSMul.hSMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) k' : K)
            ((((B.repr : (a : L) → ι →₀ K)
                      (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) k : L) ((B : (a : ι) → L) k' : L)) :
                    ι →₀ K) :
                  (a : ι) → K)
                ixy :
              K)‖
⊢ ∃ (k' : ι),
    Norm.norm.{u_1} (E := K)
        (∑ j : ι,
          HSMul.hSMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
            ((((B.repr : (a : L) → ι →₀ K)
                      (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) k : L) ((B : (a : ι) → L) j : L)) :
                    ι →₀ K) :
                  (a : ι) → K)
                ixy :
              K)) ≤
      ‖HSMul.hSMul (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) k' : K)
          ((((B.repr : (a : L) → ι →₀ K)
                    (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) k : L) ((B : (a : ι) → L) k' : L)) :
                  ι →₀ K) :
                (a : ι) → K)
              ixy :
            K)‖

Tactic:
obtain ⟨k, hk0, hk⟩ := IsNonarchimedean.finset_image_add hna'
        (fun i ↦ B.repr y i • B.repr (B k * B i) ixy) (univ : Finset ι)

Premises used: HMul.hMul, Finset.univ, IsNonarchimedean.finset_image_add, Module.Basis.repr, HSMul.hSMul, DFunLike.coe