awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
⊢ MeasurableSet.{u_5} (α := β)
    (⋂ (i : ℕ),
      ⋂ (_ : True),
        {x : β |
          ∃ (i_2 : ℕ),
            True ∧
              SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i_2) ((fun (n : ι) ↦ f n x) '' u i_2) ⊆
                {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1}})
have inr : ∀ (K : ℕ),
  Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K →
    MeasurableSet.{u_5} (α := β)
      {x : β |
        ∃ (i : ℕ),
          True ∧
            SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
              {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}
Tactic: refine MeasurableSet.biInter Set.countable_univ fun K _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ MeasurableSet.{u_5} (α := β)
    {x : β |
      ∃ (i : ℕ),
        True ∧
          SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
            {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}
have inr : MeasurableSet.{u_5} (α := β)
  (⋃ (i : ℕ),
    {x : β |
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
        {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}})
Tactic: simp_rw [Set.setOf_exists, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ MeasurableSet.{u_5} (α := β)
    (⋃ (i : ℕ),
      {x : β |
        SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
          {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}})
have inr : ∀ (N : ℕ),
  MeasurableSet.{u_5} (α := β)
    {x : β |
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u N) ((fun (n : ι) ↦ f n x) '' u N) ⊆
        {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}
Tactic: refine MeasurableSet.iUnion fun N => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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} (α := β)
    {x : β |
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u N) ((fun (n : ι) ↦ f n x) '' u N) ⊆
        {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}
have inr : 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: simp_rw [prod_image_image_eq, image_subset_iff, prod_subset_iff, Set.setOf_forall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
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}
⊢ Measurable.{u_6, u_7} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x
have hE : MeasurableSet E
Tactic: have hE : MeasurableSet E := measurableSet_exists_tendsto (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
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
⊢ Measurable.{u_6, u_7} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
have 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)
Tactic: refine measurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ measurable_const)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
have 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
Tactic: refine measurable_of_tendsto_metrizable' L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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) μ
⊢ AEMeasurable.{u_6, u_7} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ
have 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) μ
Tactic: choose g hg_meas hg_eq_f using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ AEMeasurable.{u_6, u_7} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ
have right : EventuallyEq.{u_6, u_7} (β := E) (ae μ) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) fun (x : X) ↦ ∏'[L] (i : ι), g i x
Tactic: use (fun x => ∏'[L] i, g i x), Measurable.tprod hg_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ EventuallyEq.{u_6, u_7} (β := E) (ae μ) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) fun (x : X) ↦ ∏'[L] (i : ι), g i x
have 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
Tactic: filter_upwards [ae_all_iff.mpr hg_eq_f] with x h_eq using tprod_congr h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ EventuallyEq.{u_6, u_7} (β := E) (ae μ) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) fun (x : X) ↦ ∏'[L] (i : ι), g i x
have h₁ : ∀ (a : X), (∀ (i : ι), f i a = g i a) → Eq.{u_7 + 1} (α := E) (∏'[L] (i : ι), f i a) (∏'[L] (i : ι), g i a)
Tactic: filter_upwards [ae_all_iff.mpr hg_eq_f] with x h_eq using tprod_congr h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
⊢ Measurable.{u_6, u_7} (α := X) (β := E) (∏'[L] (i : ι), f i)
have 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)
Tactic: rw [tprod_def, finprod_def']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
⊢ 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)
have 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
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ 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)
have 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
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ 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)
have 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)
Tactic: split_ifs with hm