awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ
refine_1 : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
have refine_2 : IsSeparable.{u_6} (α := β) (range fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
Tactic: refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : ℕ
⊢ Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
have 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)
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
have refine_1 : Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1
Tactic: rw [this, measurable_swap_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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} (α := β) (range fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ι)))
⊢ IsSeparable.{u_6} (α := β) (range fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
have 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 : ι)))
Tactic: apply this.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α
⊢ 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))
have refine_2 : ∃ (i_1 : ↥(t_sf n).range) (y : α), u (↑i_1 : ι) y = u (↑i : ι) x
Tactic: simp only [mem_iUnion, mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 (U n)
have h_str_meas : 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
⊢ StronglyMeasurable (U n)
have 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) sorry, 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (U n)
have 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) sorry, p.2))
Tactic: simp_rw [U, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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))
have refine : Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
  Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) sorry
Tactic: refine h_str_meas.comp_measurable (Measurable.prodMk ?_ measurable_snd)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : AEMeasurable f μ
⊢ AEFinStronglyMeasurable f μ
have refine : ∫⁻ (x : α), AEMeasurable.mk f hf_meas x ∂μ ≠ ∞
Tactic: refine ⟨hf_meas.mk f, ENNReal.finStronglyMeasurable_of_measurable ?_ hf_meas.measurable_mk,
    hf_meas.ae_eq_mk⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace γ
β : Type u_4
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb
have rw : AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μa)
Tactic: rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace γ
β : Type u_4
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
rw : AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μa)
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb
have rw₁ : AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable (g ∘ f) μa
Tactic: rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have mp : AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
  AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
mp :
  AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
    AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have mpr : AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ →
  AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
Tactic: have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have mp : EventuallyEq.{u_1, u_4} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
Tactic: refine ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.stronglyMeasurable.smul g'meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
have mp : ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
  Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
Tactic: apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
have mp₁ : ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
  Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
Tactic: apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have hg'₁ : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
Tactic: rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
Cleared hypotheses: hg', A
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have mp : ∀ᵐ (x : α) ∂μ,
  Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
Tactic: rw [ae_restrict_iff' A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
      Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have h : ∀ (a : α) (ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a) (h'a : f a ≠ 0), (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
Tactic: filter_upwards [hg'] with a ha h'a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
have this : (↑(f a) : ℝ≥0∞) ≠ 0
Tactic: have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h'a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : (↑(f a) : ℝ≥0∞) ≠ 0
⊢ (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
have h : (↑(f a) : ℝ) • g' a = (↑(f a) : ℝ) • g' a
Tactic: rw [ha this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have h : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ x), (↑(f x) : ℝ) • g x = (↑(f x) : ℝ) • g' x
Tactic: filter_upwards [ae_restrict_mem A.compl] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ x
⊢ (↑(f x) : ℝ) • g x = (↑(f x) : ℝ) • g' x
have hx₁ : f x = 0
Tactic: simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
Cleared hypotheses: hx