-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
refine_1 :
  ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K)
      ((fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a)
refine_2 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K) a →
      (fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a ∈
        (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range
refine_3 :
  ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    (fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a) =
      a
refine_4 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K) a →
      (fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          ((fun (p : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a) =
        a
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
have refine_5 : ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
  (HPow.hPow (α := ℝ) (β := ℕ) (↑(a.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
      ∫ (x : ℝ) in (↑(a.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(a.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
        HPow.hPow (β := ℕ) x 2 ∂ρ =
    (HPow.hPow (α := ℝ) (β := ℕ)
          (↑(Sigma.snd (β := fun (i : ℕ) ↦ ℕ)
                ((fun (p : (_ : ℕ) × ℕ) ↦
                    (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                      (_ : ℕ) × ℕ))
                  a)) :
            ℝ)
          2)⁻¹ *
      ∫ (x : ℝ) in
        (↑(Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
              ((fun (p : (_ : ℕ) × ℕ) ↦
                  (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                    (_ : ℕ) × ℕ))
                a)) :
          ℝ)..(↑(HAdd.hAdd (α := ℕ)
              (Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
                ((fun (p : (_ : ℕ) × ℕ) ↦
                    (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                      (_ : ℕ) × ℕ))
                  a))
              1) :
          ℝ),
        HPow.hPow (β := ℕ) x 2 ∂ρ
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_