awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
K : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K
N : ℕ
⊢ MeasurableSet.{u_5} (α := β)
    (⋂ i ∈ u N,
      ⋂ i_1 ∈ u N,
        {x : β |
          Membership.mem (γ := Set (ι × ι))
            (preimage.{u_2, u_3} (β := γ × γ) (fun (p : ι × ι) ↦ (f p.1 x, f p.2 x))
              {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1})
            (i, i_1)})

Tactic:
MeasurableSet.biInter (to_countable (u N)) fun i _ =>
      MeasurableSet.biInter (to_countable (u N)) fun j _ =>
        measurableSet_lt (Measurable.dist (hf i) (hf j)) measurable_const

Premises used: MeasurableSet.biInter, Measurable.dist, Set.to_countable, measurableSet_lt, measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
K : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K
N : ℕ
⊢ MeasurableSet.{u_5} (α := β)
    (⋂ i ∈ u N,
      ⋂ i_1 ∈ u N,
        {x : β |
          Membership.mem (γ := Set (ι × ι))
            (preimage.{u_2, u_3} (β := γ × γ) (fun (p : ι × ι) ↦ (f p.1 x, f p.2 x))
              {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1})
            (i, i_1)})

Tactic:
exact
    MeasurableSet.biInter (to_countable (u N)) fun i _ =>
      MeasurableSet.biInter (to_countable (u N)) fun j _ =>
        measurableSet_lt (Measurable.dist (hf i) (hf j)) measurable_const

Premises used: MeasurableSet.biInter, Measurable.dist, Set.to_countable, measurableSet_lt, measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
⊢ ∀ (i : Finset ι), Measurable.{u_6, u_7} (β := E_1) fun (x : X) ↦ ∏ b ∈ i, (fun (x_1 : ι) ↦ f x_1 x) b

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
⊢ MeasurableSet E

Tactic:
have hE : MeasurableSet E := measurableSet_exists_tendsto (by fun_prop)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
⊢ Eq (α := (a : (↑Eᶜ : Type u_6)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_6)) → E_1)
    fun (x : (↑Eᶜ : Type u_6)) ↦ (1 : E_1)

Tactic:
have h0 : (Eᶜ.restrict fun x => ∏'[L] i, f i x) = fun _ => 1 :=
    funext fun ⟨x, hx⟩ => tprod_eq_one_of_not_multipliable hx
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_6)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_6)) → E_1)
    fun (x : (↑Eᶜ : Type u_6)) ↦ (1 : E_1)
⊢ Measurable.{u_6, u_7} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x

Tactic:
measurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ measurable_const)

Premises used: Eq.rec, measurable_const, Eq.symm, measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_6)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_6)) → E_1)
    fun (x : (↑Eᶜ : Type u_6)) ↦ (1 : E_1)
refine :
  Measurable.{u_6, u_7} (α := (↑E : Type u_6)) (β := E_1)
    (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)
⊢ Measurable.{u_6, u_7} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x

Tactic:
refine measurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ measurable_const)

Premises used: measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_6)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_6)) → E_1)
    fun (x : (↑Eᶜ : Type u_6)) ↦ (1 : E_1)
⊢ Measurable.{u_6, u_7} (α := (↑E : Type u_6)) (β := E_1)
    (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)

Tactic:
measurable_of_tendsto_metrizable' L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)

Premises used: Iff.mpr, measurable_of_tendsto_metrizable', tendsto_pi_nhds, Multipliable.hasProd, SummationFilter.filter, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_6)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_6)) → E_1)
    fun (x : (↑Eᶜ : Type u_6)) ↦ (1 : E_1)
refine :
  ∀ (i : Finset ι), Measurable.{u_6, u_7} (β := E_1) fun (e : (↑E : Type u_6)) ↦ ∏ b ∈ i, (fun (x : ι) ↦ f x (↑e : X)) b
⊢ Measurable.{u_6, u_7} (α := (↑E : Type u_6)) (β := E_1)
    (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)

Tactic:
refine measurable_of_tendsto_metrizable' L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)

Premises used: Iff.mpr, measurable_of_tendsto_metrizable', tendsto_pi_nhds, SummationFilter.filter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_6
E_1 : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : SecondCountableTopology E_1
inst_5 : MeasurableSpace E_1
inst_6 : BorelSpace E_1
inst_7 : MeasurableMul₂ E_1
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), Measurable (f i)
E : Set X := {x : X | Multipliable.{u_7, u_8} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_6)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_6)) → E_1)
    fun (x : (↑Eᶜ : Type u_6)) ↦ (1 : E_1)
⊢ ∀ (i : Finset ι), Measurable.{u_6, u_7} (β := E_1) fun (e : (↑E : Type u_6)) ↦ ∏ b ∈ i, (fun (x : ι) ↦ f x (↑e : X)) 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : MeasurableMul₂ E
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
choose :
  ∀ (g : (i : ι) → X → E) (hg_meas : ∀ (i : ι), Measurable (g i)) (hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i),
    AEMeasurable.{u_6, u_7} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ
⊢ AEMeasurable.{u_6, u_7} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ

Tactic:
choose g hg_meas hg_eq_f using h
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : MeasurableMul₂ E
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), Measurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
right : EventuallyEq.{u_6, u_7} (β := E) (ae μ) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) fun (x : X) ↦ ∏'[L] (i : ι), g i x
⊢ AEMeasurable.{u_6, u_7} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ

Tactic:
use (fun x => ∏'[L] i, g i x), Measurable.tprod hg_meas

Premises used: tprod, Measurable.tprod
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : MeasurableMul₂ E
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), Measurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
x : X
h_eq : ∀ (i : ι), f i x = g i x
⊢ Eq.{u_7 + 1} (α := E) (∏'[L] (i : ι), f i x) (∏'[L] (i : ι), g i x)

Tactic:
tprod_congr h_eq

Premises used: tprod_congr
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : MeasurableMul₂ E
inst_8 : Countable ι
L : SummationFilter ι
inst_9 : L.NeBot
inst_10 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), Measurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ ∀ (i : ι), f i a = g i a) x} x →
          Membership.mem (γ := Set X)
            {x : X |
              (fun (x : X) ↦
                  Eq.{u_7 + 1} (α := E) ((fun (x : X) ↦ (∏'[L] (i : ι), f i x : E)) x)
                    ((fun (x : X) ↦ (∏'[L] (i : ι), g i x : E)) x))
                x}
            x}
      a
h₁ h₂ : ∀ (x : X) (h_eq : ∀ (i : ι), f i x = g i x), Eq.{u_7 + 1} (α := E) (∏'[L] (i : ι), f i x) (∏'[L] (i : ι), g i x)
⊢ EventuallyEq.{u_6, u_7} (β := E) (ae μ) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) fun (x : X) ↦ ∏'[L] (i : ι), g i x

Tactic:
filter_upwards [ae_all_iff.mpr hg_eq_f] with x h_eq using tprod_congr h_eq

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- 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)
rw :
  Measurable.{u_6, u_7} (α := X) (β := 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)
⊢ Measurable.{u_6, u_7} (α := X) (β := 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
f : ι → X → E
h : ∀ (i : ι), Measurable (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)),
        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,
            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) →
        Measurable.{u_6, u_7} (α := X) (β := 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 → Measurable.{u_6, u_7} (α := X) (β := 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 →
        Measurable (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), Measurable.{u_6, u_7} (α := X) (β := E) 1
⊢ Measurable.{u_6, u_7} (α := X) (β := 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
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:
measurable_one

Premises used: measurable_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
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) 1

Tactic:
measurable_one

Premises used: measurable_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
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) 1

Tactic:
exact measurable_one

Premises used: measurable_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
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.{u_6, u_7} (α := X) (β := E) 1

Tactic:
measurable_one

Premises used: measurable_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
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.{u_6, u_7} (α := X) (β := E) 1

Tactic:
exact measurable_one

Premises used: measurable_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
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:
measurable_one

Premises used: measurable_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
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ Measurable.{u_6, u_7} (α := X) (β := E) 1

Tactic:
measurable_one

Premises used: measurable_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
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
⊢ Measurable.{u_6, u_7} (α := X) (β := E) 1

Tactic:
exact measurable_one

Premises used: measurable_one