awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) (∏'[L] (i : ι), f i)
have rw : StronglyMeasurable.{u_4, u_5} (α := X) (β := 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: rw [tprod_def, finprod_def']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := 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)
have 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)),
      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,
          L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
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)),
        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,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := 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)
have 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) →
      StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
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)),
        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,
            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) →
        StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := 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)
have 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 → StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
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)),
        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,
            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) →
        StronglyMeasurable.{u_4, u_5} (α := X) (β := 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 → StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := 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)
have 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 →
      StronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm)
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
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)),
        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,
            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) →
        StronglyMeasurable.{u_4, u_5} (α := X) (β := 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 → StronglyMeasurable.{u_4, u_5} (α := X) (β := 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 →
        StronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := 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)
have neg₂ : ∀ (hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L), StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
have 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)
Tactic: refine Finset.stronglyMeasurable_prod _ (fun _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down)
have pos : StronglyMeasurable (if x.down ∈ L.support then f x.down else 1)
Tactic: rw [Set.mulIndicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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
⊢ StronglyMeasurable (if x.down ∈ L.support then f x.down else 1)
have pos : x.down ∈ L.support → StronglyMeasurable (f x.down)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
⊢ StronglyMeasurable (if x.down ∈ L.support then f x.down else 1)
have neg : x.down ∉ L.support → StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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) μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (∏'[L] (i : ι), f i) μ
have 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)
  μ
Tactic: rw [tprod_def, finprod_def']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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) μ
⊢ 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)
    μ
have 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)
        μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
          μ
⊢ 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)
    μ
have 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 μ
Tactic: split_ifs with hm