awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_1 : SeminormedAddCommGroup E
inst_2 : SecondCountableTopology E
inst_3 : BorelSpace E
inst_4 : l.IsCountablyGenerated
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
⊢ TendstoInMeasure μ' (X - fun (x : ι) ↦ Z) l 0

Tactic:
simpa [tendstoInMeasure_iff_norm] using h

Premises used: MeasureTheory.tendstoInMeasure_iff_norm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_1 : SeminormedAddCommGroup E
inst_2 : SecondCountableTopology E
inst_3 : BorelSpace E
inst_4 : l.NeBot
inst_5 : l.IsCountablyGenerated
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω') (m := fun (i : ι) ↦ m') (mE := mE) X l Z (fun (x : ι) ↦ μ') μ'

Tactic:
h.tendstoInDistribution_of_aemeasurable hX (h.aemeasurable hX)

Premises used: MeasureTheory.TendstoInMeasure.aemeasurable, MeasureTheory.TendstoInMeasure.tendstoInDistribution_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ ∀ (i : ι), AEMeasurable (X i) μ''

Tactic:
have hX : ∀ i, AEMeasurable (X i) μ'' := hXZ.forall_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'

Tactic:
tendstoInDistribution_of_tendstoInMeasure_sub (X := fun n ω ↦ (X n ω, c))
    (fun n ω ↦ (X n ω, Y n ω)) (fun ω ↦ (Z ω, c)) ?_ ?_ (fun i ↦ (hX i).prodMk (hY_meas i))

Premises used: MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub, setOf, Prod.mk, AEMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
refine_1 :
  TendstoInDistribution (E := E × E') (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
refine_2 :
  TendstoInMeasure μ''
    (HSub.hSub (α := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l 0
⊢ TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'

Tactic:
refine tendstoInDistribution_of_tendstoInMeasure_sub (X := fun n ω ↦ (X n ω, c))
    (fun n ω ↦ (X n ω, Y n ω)) (fun ω ↦ (Z ω, c)) ?_ ?_ (fun i ↦ (hX i).prodMk (hY_meas i))

Premises used: MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub, Prod.mk, AEMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x : E) ↦ (x, c)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ TendstoInDistribution (E := E × E') (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'

Tactic:
exact hXZ.continuous_comp (g := fun x ↦ (x, c)) (by fun_prop)

Premises used: MeasureTheory.TendstoInDistribution.continuous_comp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
this : TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0
⊢ TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0

Tactic:
this
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
this : TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0
h :
  ∀ (n : ι) (ω : Ω''),
    (HSub.hSub (α := ι → Ω'' → E × E') (β := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω))
          (fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) n ω).1 =
      0
⊢ TendstoInMeasure μ''
    (HSub.hSub (α := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l 0

Tactic:
convert! this with n ω
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
this : TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0
n : ι
ω : Ω''
⊢ (HSub.hSub (α := ι → Ω'' → E × E') (β := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω))
        (fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) n ω).1 =
    0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
refine_2 : TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0
⊢ TendstoInMeasure μ''
    (HSub.hSub (α := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l 0

Tactic:
suffices TendstoInMeasure μ'' (fun n ω ↦ ((0 : E), Y n ω - c)) l 0 by
      convert! this with n ω
      simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0

Tactic:
simpa [tendstoInMeasure_iff_norm] using hY

Premises used: MeasureTheory.tendstoInMeasure_iff_norm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
F : Type u_7
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : TopologicalSpace F
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
g : E × E' → F
hg : Continuous[instTopologicalSpaceProd, inst_8] g
inst_11 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ TendstoInDistribution.{u_1, u_7, u_3, u_4} (E := F) (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := inst_9)
    (fun (n : ι) (ω : Ω'') ↦ g (X n ω, Y n ω)) l (fun (ω : Ω') ↦ g (Z ω, c)) (fun (x : ι) ↦ μ'') μ'

Tactic:
TendstoInDistribution.continuous_comp hg ?_

Premises used: MeasureTheory.TendstoInDistribution.continuous_comp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
F : Type u_7
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : TopologicalSpace F
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
g : E × E' → F
hg : Continuous[instTopologicalSpaceProd, inst_8] g
inst_11 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
refine :
  TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
⊢ TendstoInDistribution.{u_1, u_7, u_3, u_4} (E := F) (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := inst_9)
    (fun (n : ι) (ω : Ω'') ↦ g (X n ω, Y n ω)) l (fun (ω : Ω') ↦ g (Z ω, c)) (fun (x : ι) ↦ μ'') μ'

Tactic:
refine TendstoInDistribution.continuous_comp hg ?_

Premises used: MeasureTheory.TendstoInDistribution.continuous_comp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
F : Type u_7
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : TopologicalSpace F
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
g : E × E' → F
hg : Continuous[instTopologicalSpaceProd, inst_8] g
inst_11 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'

Tactic:
hXZ.prodMk_of_tendstoInMeasure_const X Y Z hY_tendsto hY

Premises used: MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
F : Type u_7
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : TopologicalSpace F
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
g : E × E' → F
hg : Continuous[instTopologicalSpaceProd, inst_8] g
inst_11 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'

Tactic:
exact hXZ.prodMk_of_tendstoInMeasure_const X Y Z hY_tendsto hY

Premises used: MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X Y : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
c : E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : E × E) ↦ x.1 + x.2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
pos :
  ∀ (hε_top : ε = ∞),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
neg :
  ∀ (hε_top : ¬ε = ∞),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
by_cases hε_top : ε = ∞
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
⊢ LT.lt (α := ℝ≥0∞) 0 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)

Tactic:
have h1 : Tendsto (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0) := h 1 (by simp) (by simp)
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h1 (fun _ ↦ zero_le) ?_

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
pos :
  LE.le.{u_2} (α := ι → ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) fun (n : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h1 (fun _ ↦ zero_le) ?_

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds