{Ω : Type u_1} →
  {ι : Type u_2} →
    {E : Type u_3} →
      {m : MeasurableSpace Ω} →
        {mE : MeasurableSpace E} →
          [inst : TopologicalSpace E] →
            [inst_1 : OpensMeasurableSpace E] →
              {X : ι → Ω → E} →
                {l : Filter ι} →
                  {Z : Ω → E} →
                    {μ : MeasureTheory.Measure Ω} →
                      [inst_2 : MeasureTheory.IsProbabilityMeasure μ] →
                        {motive : MeasureTheory.TendstoInDistribution X l Z μ → Sort u} →
                          ((forall_aemeasurable : ∀ (i : ι), AEMeasurable (X i) μ) →
                              (aemeasurable_limit : AEMeasurable Z μ) →
                                (tendsto :
                                    Filter.Tendsto (fun n => ⟨MeasureTheory.Measure.map (X n) μ, ⋯⟩) l
                                      (nhds ⟨MeasureTheory.Measure.map Z μ, ⋯⟩)) →
                                  motive ⋯) →
                            (t : MeasureTheory.TendstoInDistribution X l Z μ) → motive t