awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inl :
  ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥],
    StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ limUnder ⊥ fun (x_1 : ι) ↦ f x_1 x
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
have inr : ∀ (hl : l.NeBot), StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
Tactic: obtain rfl | hl := eq_or_neBot l
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
have mconv : MeasurableSet conv
Tactic: have mconv : MeasurableSet conv := StronglyMeasurable.measurableSet_exists_tendsto hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
have refine : Tendsto (β := (↑conv : Type u_2) → E) (fun (i : ι) ↦ f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) l
  (𝓝 fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X))
Tactic: refine stronglyMeasurable_of_tendsto l
      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
⊢ Tendsto (β := (↑conv : Type u_2) → E) (fun (i : ι) ↦ f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) l
    (𝓝 fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X))
have refine : ∀ (x : (↑conv : Type u_2)),
  Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
    (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))
Tactic: refine tendsto_pi_nhds.2 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
x : (↑conv : Type u_2)
⊢ Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
    (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))
have obtain : ∀ (c : E) (hc : Tendsto (fun (x_1 : ι) ↦ f x_1 (↑x : X)) l (𝓝 c)),
  Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
    (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))
Tactic: obtain ⟨c, hc⟩ := x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
x : (↑conv : Type u_2)
c : E
hc : Tendsto (fun (x_1 : ι) ↦ f x_1 (↑x : X)) l (𝓝 c)
⊢ Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
    (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))
have rwa : Tendsto (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l (𝓝 c)
Tactic: rwa [hc.limUnder_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
have hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
Tactic: have hconv : StronglyMeasurable (fun x : conv ↦ limUnder l (f · x)) := by
    refine stronglyMeasurable_of_tendsto l
      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_
    refine tendsto_pi_nhds.2 fun x ↦ ?_
    obtain ⟨c, hc⟩ := x.2
    rwa [hc.limUnder_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
⊢ Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
have h : ∀ (x : X),
  Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
have pos : ∀ (hx : x ∈ conv),
  Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
Tactic: by_cases hx : x ∈ conv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
pos :
  ∀ (hx : x ∈ conv),
    Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
      (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
        (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
have neg : ∀ (hx : x ∉ conv),
  Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
Tactic: by_cases hx : x ∈ conv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
hx : x ∈ conv
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
have pos : Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
  (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ conv) x hx) : X))
Tactic: rw [Function.extend_val_apply hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
hx : x ∉ conv
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
have neg : (l.limUnder fun (x_1 : ι) ↦ f x_1 x) = e
Tactic: rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
hx : x ∉ conv
neg : (l.limUnder fun (x_1 : ι) ↦ f x_1 x) = e
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
have neg₁ : Classical.choice hE = e
Tactic: rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
have this : Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
  (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
    (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
Tactic: have : (fun x ↦ limUnder l (f · x)) = ((↑) : conv → X).extend
      (fun x ↦ limUnder l (f · x)) (fun _ ↦ e) := by
    ext x
    by_cases hx : x ∈ conv
    · rw [Function.extend_val_apply hx]
    · rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
this :
  Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
have inr : StronglyMeasurable.{u_2, u_3} (α := X) (β := E)
  (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
    (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
⊢ StronglyMeasurable.{u_4, u_5} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x
have hE : MeasurableSet E
Tactic: have hE : MeasurableSet E := StronglyMeasurable.measurableSet_exists_tendsto (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (hypothesis)
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
⊢ StronglyMeasurable.{u_4, u_5} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x
have h0 : Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
  (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
  fun (x : (↑Eᶜ : Type u_4)) ↦ (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.StronglyMeasurable (goal)
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)
⊢ StronglyMeasurable.{u_4, u_5} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x
have refine : StronglyMeasurable.{u_4, u_5} (α := (↑E : Type u_4)) (β := E_1)
  (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)
Tactic: refine stronglyMeasurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ stronglyMeasurable_const)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)
⊢ StronglyMeasurable.{u_4, u_5} (α := (↑E : Type u_4)) (β := E_1)
    (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)
have refine : ∀ (i : Finset ι),
  StronglyMeasurable.{u_4, u_5} (β := E_1) fun (e : (↑E : Type u_4)) ↦ ∏ b ∈ i, (fun (x : ι) ↦ f x (↑e : X)) b
Tactic: refine stronglyMeasurable_of_tendsto L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ
have choose : ∀ (g : (i : ι) → X → E) (hg_meas : ∀ (i : ι), StronglyMeasurable (g i)) (hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i),
  AEStronglyMeasurable.{u_4, u_5} (β := 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.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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), StronglyMeasurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ
have right : EventuallyEq.{u_4, u_5} (β := 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), StronglyMeasurable.tprod hg_meas
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), StronglyMeasurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
⊢ EventuallyEq.{u_4, u_5} (β := 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_5 + 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.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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), StronglyMeasurable (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_5 + 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_4, u_5} (β := 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_5 + 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