Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down) μ

pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : ¬HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable 1 μ

pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable 1 μ

pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ

pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : ¬Multipliable (fun i ↦ f i) L
⊢ AEMeasurable 1 μ

Tactic:
any_goals exact aemeasurable_one

Goal state after:
case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down) μ

case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ