-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
hf :
  ∀ (x : ℕ+),
    Summable (α := ℝ) fun (y : ↥(↑x : ℕ).divisorsAntidiagonal) ↦
      ‖HPow.hPow (α := 𝕜)
            (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2 :
              𝕜)
            k *
          r ^
            HMul.hMul (α := ℕ)
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).1
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).2‖
⊢ (∀ (x : ℕ+),
      Summable (α := ℝ) fun (y : ↥(↑x : ℕ).divisorsAntidiagonal) ↦
        ‖HPow.hPow (α := 𝕜)
              (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                          (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                      ℕ × ℕ).2 :
                𝕜)
              k *
            r ^
              HMul.hMul (α := ℕ)
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).1
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2‖) ∧
    Summable (α := ℝ) fun (x : ℕ+) ↦
      ∑' (y : ↥(↑x : ℕ).divisorsAntidiagonal),
        ‖HPow.hPow (α := 𝕜)
              (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                          (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                      ℕ × ℕ).2 :
                𝕜)
              k *
            r ^
              HMul.hMul (α := ℕ)
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).1
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2‖
have hf₁ : Summable (α := ℝ) fun (x : ℕ+) ↦
  ∑' (y : ↥(↑x : ℕ).divisorsAntidiagonal),
    ‖HPow.hPow (α := 𝕜)
          (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).2 :
            𝕜)
          k *
        r ^
          HMul.hMul (α := ℕ)
            (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                    (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                ℕ × ℕ).1
            (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                    (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                ℕ × ℕ).2‖
Tactic: constructor