Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable
    (if h : Multipliable (fun i ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down) then
          ∏ i ∈ Finite.toFinset h, L.support.mulIndicator (fun i ↦ f i) i.down
        else 1
      else if HasProd (fun i ↦ f i) 1 L then 1 else Exists.choose h
    else 1)

Tactic:
split_ifs with hm

Goal state after:
case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ StronglyMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down)

case neg
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : ¬Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ StronglyMeasurable 1

case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : HasProd (fun i ↦ f i) 1 L
⊢ StronglyMeasurable 1

case neg
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ StronglyMeasurable (Exists.choose hm)

case neg
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : ¬Multipliable (fun i ↦ f i) L
⊢ StronglyMeasurable 1