awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ Measurable.{u_6, u_7} (α := X) (β := E)
    (∏ i ∈ Finite.toFinset (s := 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.measurable_prod_apply (fun _ _ ↦ ?_) measurable_id

Premises used: measurable_id, Finset.measurable_prod_apply
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
pos :
  ∀ x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
    Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ L.support.mulIndicator (fun (i : ι) ↦ f i) x.down)
⊢ Measurable.{u_6, u_7} (α := X) (β := E)
    (∏ i ∈ Finite.toFinset (s := 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.measurable_prod_apply (fun _ _ ↦ ?_) measurable_id

Premises used: measurable_id, Finset.measurable_prod_apply
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
pos : Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ if x.down ∈ L.support then f x.down else 1)
⊢ Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ L.support.mulIndicator (fun (i : ι) ↦ f i) x.down)

Tactic:
rw [Set.mulIndicator]

Premises used: Set.mulIndicator
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
pos : x.down ∈ L.support → Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ f x.down)
neg : x.down ∉ L.support → Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ 1)
⊢ Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ if x.down ∈ L.support then f x.down else 1)

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
h_4 : x.down ∈ L.support
⊢ Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ f x.down)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
h_4 : x.down ∉ L.support
⊢ Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ 1)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ ∀ (i : Finset ι), Measurable.{u_6, u_7} (α := X) (β := E) (∏ b ∈ i, (fun (i : ι) ↦ f i) b)

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

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

Premises used: measurable_of_tendsto_metrizable', Exists.choose_spec, SummationFilter.filter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
rw :
  AEMeasurable.{u_6, u_7} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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)
    μ
⊢ AEMeasurable.{u_6, u_7} (β := E) (∏'[L] (i : ι), f i) μ

Tactic:
rw [tprod_def, finprod_def']

Premises used: finprod_def', tprod_def
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
        AEMeasurable.{u_6, u_7} (β := E)
          (∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEMeasurable.{u_6, u_7} (β := E) 1 μ
pos₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEMeasurable.{u_6, u_7} (β := E) 1 μ
neg₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L →
        AEMeasurable (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), AEMeasurable.{u_6, u_7} (β := E) 1 μ
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (∏ i ∈ Finite.toFinset (s := 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:
aemeasurable_one

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

Tactic:
aemeasurable_one

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

Tactic:
exact aemeasurable_one

Premises used: aemeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ AEMeasurable.{u_6, u_7} (β := E) 1 μ

Tactic:
aemeasurable_one

Premises used: aemeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ AEMeasurable.{u_6, u_7} (β := E) 1 μ

Tactic:
exact aemeasurable_one

Premises used: aemeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ

Tactic:
aemeasurable_one

Premises used: aemeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ AEMeasurable.{u_6, u_7} (β := E) 1 μ

Tactic:
aemeasurable_one

Premises used: aemeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ AEMeasurable.{u_6, u_7} (β := E) 1 μ

Tactic:
exact aemeasurable_one

Premises used: aemeasurable_one
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (∏ i ∈ Finite.toFinset (s := 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.aemeasurable_prod _ (fun _ _ ↦ ?_)

Premises used: Finset.aemeasurable_prod
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
pos :
  ∀ x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
    AEMeasurable.{u_6, u_7} (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down) μ
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (∏ i ∈ Finite.toFinset (s := 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.aemeasurable_prod _ (fun _ _ ↦ ?_)

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

Tactic:
rw [Set.mulIndicator]

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

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

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

Tactic:
fun_prop