awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
this :
  Eq (α := (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) → β)
    (fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
    ((fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1) ∘ Prod.swap)
refine_1 : Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1
⊢ Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2

Tactic:
rw [this, measurable_swap_iff]

Premises used: measurable_swap_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
this :
  Eq (α := (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) → β)
    (fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
    ((fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1) ∘ Prod.swap)
⊢ Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1

Tactic:
measurable_from_prod_countable_left fun j => (h j).measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, measurable_from_prod_countable_left, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
this :
  Eq (α := (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) → β)
    (fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
    ((fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1) ∘ Prod.swap)
⊢ Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1

Tactic:
exact measurable_from_prod_countable_left fun j => (h j).measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
⊢ IsSeparable.{u_6} (α := β) (⋃ (i : ↥(t_sf n).range), range (u (↑i : ι)))

Tactic:
have : IsSeparable (⋃ i : (t_sf n).range, range (u i)) :=
        .iUnion fun i => (h i).isSeparable_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
this : IsSeparable.{u_6} (α := β) (⋃ (i : ↥(t_sf n).range), range (u (↑i : ι)))
refine_2 :
  Subset.{u_6} (α := Set β) (range fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
    (⋃ (i : ↥(t_sf n).range), range (u (↑i : ι)))
⊢ IsSeparable.{u_6} (α := β) (range fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)

Tactic:
apply this.mono

Premises used: TopologicalSpace.IsSeparable.mono
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
this : IsSeparable.{u_6} (α := β) (⋃ (i : ↥(t_sf n).range), range (u (↑i : ι)))
i : ↥(t_sf n).range
x : α
refine_2 : ∃ (i_1 : ↥(t_sf n).range) (y : α), u (↑i_1 : ι) y = u (↑i : ι) x
⊢ Membership.mem (γ := Set β) (⋃ (i : ↥(t_sf n).range), range (u (↑i : ι)))
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) (i, x))

Tactic:
simp only [mem_iUnion, mem_range]

Premises used: Set.mem_range, Set.mem_iUnion
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
this : IsSeparable.{u_6} (α := β) (⋃ (i : ↥(t_sf n).range), range (u (↑i : ι)))
i : ↥(t_sf n).range
x : α
⊢ ∃ (i_1 : ↥(t_sf n).range) (y : α), u (↑i_1 : ι) y = u (↑i : ι) x

Tactic:
⟨i, x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
this : IsSeparable.{u_6} (α := β) (⋃ (i : ↥(t_sf n).range), range (u (↑i : ι)))
i : ↥(t_sf n).range
x : α
⊢ ∃ (i_1 : ↥(t_sf n).range) (y : α), u (↑i_1 : ι) y = u (↑i : ι) x

Tactic:
exact ⟨i, x, rfl⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2

Tactic:
have h_str_meas : StronglyMeasurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd := by
    refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
    · have :
        (fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
          (fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
        rfl
      rw [this, measurable_swap_iff]
      exact measurable_from_prod_countable_left fun j => (h j).measurable
    · have : IsSeparable (⋃ i : (t_sf n).range, range (u i)) :=
        .iUnion fun i => (h i).isSeparable_range
      apply this.mono
      rintro _ ⟨⟨i, x⟩, rfl⟩
      simp only [mem_iUnion, mem_range]
      exact ⟨i, x, rfl⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
⊢ Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))

Tactic:
have :
    (fun p : ι × α => u (t_sf n p.fst) p.snd) =
      (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
        (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
    rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
simp_rw :
  StronglyMeasurable (α := ι × α) (β := β)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ StronglyMeasurable (U n)

Tactic:
simp_rw [U, this]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ StronglyMeasurable (α := ι × α) (β := β)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))

Tactic:
h_str_meas.comp_measurable (Measurable.prodMk ?_ measurable_snd)

Premises used: Measurable.prodMk, MeasureTheory.StronglyMeasurable.comp_measurable, measurable_snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
refine :
  Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
    Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯
⊢ StronglyMeasurable (α := ι × α) (β := β)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))

Tactic:
refine h_str_meas.comp_measurable (Measurable.prodMk ?_ measurable_snd)

Premises used: Measurable.prodMk, MeasureTheory.StronglyMeasurable.comp_measurable, measurable_snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
    Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯

Tactic:
((t_sf n).measurable.comp measurable_fst).subtype_mk

Premises used: Measurable.comp, Measurable.subtype_mk, MeasureTheory.SimpleFunc.measurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
    Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯

Tactic:
exact ((t_sf n).measurable.comp measurable_fst).subtype_mk

Premises used: Measurable.comp, Measurable.subtype_mk, MeasureTheory.SimpleFunc.measurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : Measurable f
⊢ FinStronglyMeasurable f μ

Tactic:
⟨SimpleFunc.eapprox f, measure_support_eapprox_lt_top hf_meas hf,
    SimpleFunc.tendsto_eapprox hf_meas⟩

Premises used: MeasureTheory.measure_support_eapprox_lt_top, MeasureTheory.SimpleFunc.tendsto_eapprox, MeasureTheory.SimpleFunc.eapprox, And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : AEMeasurable f μ
⊢ AEFinStronglyMeasurable f μ

Tactic:
⟨hf_meas.mk f, ENNReal.finStronglyMeasurable_of_measurable ?_ hf_meas.measurable_mk,
    hf_meas.ae_eq_mk⟩

Premises used: ENNReal.finStronglyMeasurable_of_measurable, AEMeasurable.mk, MeasureTheory.AEFinStronglyMeasurable, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : AEMeasurable f μ
refine : ∫⁻ (x : α), AEMeasurable.mk f hf_meas x ∂μ ≠ ∞
⊢ AEFinStronglyMeasurable f μ

Tactic:
refine ⟨hf_meas.mk f, ENNReal.finStronglyMeasurable_of_measurable ?_ hf_meas.measurable_mk,
    hf_meas.ae_eq_mk⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : AEMeasurable f μ
rwa rwa₁ rwa₂ rwa₃ : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ ∫⁻ (x : α), AEMeasurable.mk f hf_meas x ∂μ ≠ ∞

Tactic:
rwa [lintegral_congr_ae hf_meas.ae_eq_mk.symm]

Premises used: MeasureTheory.lintegral_congr_ae, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : MeasurableSpace α
f g : α → E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable.{u_1, u_2} (β := 𝕜) fun (t : α) ↦ ⟪f t, g t⟫

Tactic:
Continuous.comp_stronglyMeasurable continuous_inner (hf.prodMk hg)

Premises used: continuous_inner, Continuous.comp_stronglyMeasurable, MeasureTheory.StronglyMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → 𝕜
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
RCLike.continuous_re.comp_aestronglyMeasurable hf

Premises used: Continuous.comp_aestronglyMeasurable, RCLike.continuous_re
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → 𝕜
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
RCLike.continuous_im.comp_aestronglyMeasurable hf

Premises used: Continuous.comp_aestronglyMeasurable, RCLike.continuous_im
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m x : MeasurableSpace α
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := 𝕜) (fun (x : α) ↦ ⟪f x, g x⟫) μ

Tactic:
continuous_inner.comp_aestronglyMeasurable (hf.prodMk hg)

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.prodMk, continuous_inner
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
c : E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) μ

Tactic:
hf.inner aestronglyMeasurable_const

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.inner