-- Module: Mathlib.Probability.StrongLaw
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
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 ∂ρ
⊢ 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 ∂ρ)

Tactic:
refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_

Premises used: Finset.sum_nbij'