-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ)
S : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ ∑ i ∈ range n, Y i
hS : S = fun (n : ℕ) ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun (n : ℕ) ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 :
  ∀ (K : ℕ),
    ∑ j ∈ range K,
        (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ ≤
      HMul.hMul (α := ℝ) 2 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
C : ℝ :=
  HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 *
    HMul.hMul (α := ℝ) 2 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
N : ℕ
refine_1 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (u a)) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range (u (N - 1))).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ {i ∈ range N | a < u i})
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
refine_2 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range (u (N - 1))).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ {i ∈ range N | a < u i}) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (u a))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
refine_3 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (u a)) 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_4 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range (u (N - 1))).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ {i ∈ range N | a < u i}) 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 : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (u a)) a →
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(u (a.fst (β := fun (i : ℕ) ↦ ℕ))) : ℝ) 2)⁻¹ *
          variance (mΩ := MeasureSpace.toMeasurableSpace) (Y (a.snd (β := fun (i : ℕ) ↦ ℕ))) ℙ =
        (HPow.hPow (α := ℝ) (β := ℕ)
              (↑(u
                    (Sigma.snd (β := fun (i : ℕ) ↦ ℕ)
                      ((fun (p : (_ : ℕ) × ℕ) ↦
                          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ))
                              (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                            (_ : ℕ) × ℕ))
                        a))) :
                ℝ)
              2)⁻¹ *
          variance (mΩ := MeasureSpace.toMeasurableSpace)
            (Y
              (Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
                ((fun (p : (_ : ℕ) × ℕ) ↦
                    (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                      (_ : ℕ) × ℕ))
                  a)))
            ℙ
⊢ Eq (α := ℝ)
    (∑ x ∈ (range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (u a),
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(u (x.fst (β := fun (i : ℕ) ↦ ℕ))) : ℝ) 2)⁻¹ *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y (x.snd (β := fun (i : ℕ) ↦ ℕ))) ℙ)
    (∑ x ∈ (range (u (N - 1))).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ {i ∈ range N | a < u i},
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(u (x.snd (β := fun (i : ℕ) ↦ ℕ))) : ℝ) 2)⁻¹ *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y (x.fst (β := fun (i : ℕ) ↦ ℕ))) ℙ)

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

Premises used: Finset.sum_nbij'