awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : ¬Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
exact stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
exact stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ StronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm)

Tactic:
stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
exact stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E)
    (∏
      i ∈
        Finite.toFinset (s :=
          Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
      L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)

Tactic:
Finset.stronglyMeasurable_prod _ (fun _ _ ↦ ?_)

Premises used: Finset.stronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
pos :
  ∀
    x ∈
      Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
        h_2,
    StronglyMeasurable.{u_4, u_5} (α := X) (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E)
    (∏
      i ∈
        Finite.toFinset (s :=
          Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
      L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)

Tactic:
refine Finset.stronglyMeasurable_prod _ (fun _ _ ↦ ?_)

Premises used: Finset.stronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
pos : StronglyMeasurable (if x.down ∈ L.support then f x.down else 1)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down)

Tactic:
rw [Set.mulIndicator]

Premises used: Set.mulIndicator
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
pos : x.down ∈ L.support → StronglyMeasurable (f x.down)
neg : x.down ∉ L.support → StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
⊢ StronglyMeasurable (if x.down ∈ L.support then f x.down else 1)

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
h_4 : x.down ∈ L.support
⊢ StronglyMeasurable (f x.down)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
h_4 : x.down ∉ L.support
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
h_4 : x.down ∉ L.support
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
exact stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ ∀ (i : Finset ι), StronglyMeasurable.{u_4, u_5} (α := X) (β := E) (∏ b ∈ i, (fun (i : ι) ↦ f i) b)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ StronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm)

Tactic:
exact stronglyMeasurable_of_tendsto L.filter (by fun_prop) hm.choose_spec

Premises used: Exists.choose_spec, stronglyMeasurable_of_tendsto, SummationFilter.filter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
rw :
  AEStronglyMeasurable.{u_4, u_5} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s :=
                Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down
        else 1
      else
        if HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L then 1
        else Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) h
    else 1)
    μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (∏'[L] (i : ι), f i) μ

Tactic:
rw [tprod_def, finprod_def']

Premises used: finprod_def', tprod_def
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
        AEStronglyMeasurable.{u_4, u_5} (β := E)
          (∏
            i ∈
              Finite.toFinset (s :=
                Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
          μ
neg :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
pos₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
neg₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L →
        AEStronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ
neg₂ : ∀ (hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L), AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s :=
                Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down
        else 1
      else
        if HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L then 1
        else Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) h
    else 1)
    μ

Tactic:
split_ifs with hm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E)
    (∏
      i ∈
        Finite.toFinset (s :=
          Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
      L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
    μ

Tactic:
aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : ¬Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ

Tactic:
aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : ¬Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ

Tactic:
exact aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ

Tactic:
aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ

Tactic:
exact aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ AEStronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ

Tactic:
aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ

Tactic:
aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ

Tactic:
exact aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E)
    (∏
      i ∈
        Finite.toFinset (s :=
          Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
      L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
    μ

Tactic:
Finset.aestronglyMeasurable_prod _ (fun _ _ ↦ ?_)

Premises used: Finset.aestronglyMeasurable_prod