awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : AddZeroClass β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
ind : ∀ (c : β) ⦃s : Set α⦄ (hs : MeasurableSet s), P (s.indicator fun (x : α) ↦ c) ⋯
add :
  ∀ ⦃f g : α → β⦄ (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hfg : StronglyMeasurable (f + g)),
    Disjoint (support f) (support g) → P f hf → P g hg → P (f + g) hfg
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f_1 : α → β
hf_1 : StronglyMeasurable f_1
s : ℕ → α →ₛ β := hf_1.approx
n : ℕ
f g : α →ₛ β
h_supp :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β))
    (support.{u_1, u_2} (M := β) (⇑g : (a : α) → β))
hf : P (⇑f : (a : α) → β) ⋯
hg : P (⇑g : (a : α) → β) ⋯
⊢ P (⇑(f + g) : (a : α) → β) ⋯

Tactic:
exact add f.stronglyMeasurable g.stronglyMeasurable (f + g).stronglyMeasurable h_supp hf hg

Premises used: HAdd.hAdd, MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : AddZeroClass β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
ind : ∀ (c : β) ⦃s : Set α⦄ (hs : MeasurableSet s), P (s.indicator fun (x : α) ↦ c) ⋯
add :
  ∀ ⦃f g : α → β⦄ (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hfg : StronglyMeasurable (f + g)),
    Disjoint (support f) (support g) → P f hf → P g hg → P (f + g) hfg
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
induction₁ : ∀ (x : α →ₛ β), P (⇑x : (a : α) → β) ⋯
⊢ P (⇑(s n) : (a : α) → β) ⋯

Tactic:
induction s n using SimpleFunc.induction with
  | const c hs => exact ind c hs
  | @add f g h_supp hf hg =>
    exact add f.stronglyMeasurable g.stronglyMeasurable (f + g).stronglyMeasurable h_supp hf hg

Premises used: Function.const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
let : P f hf
⊢ P f hf

Tactic:
let s := hf.approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
⊢ P f hf

Tactic:
lim (fun n ↦ (s n).stronglyMeasurable) hf (fun n ↦ ?_) hf.tendsto_approx

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx, MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
refine : ∀ (n : ℕ), P (⇑(s n) : (a : α) → β) ⋯
⊢ P f hf

Tactic:
refine lim (fun n ↦ (s n).stronglyMeasurable) hf (fun n ↦ ?_) hf.tendsto_approx

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx, MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
change : P (⇑(s n) : (a : α) → β) ⋯
⊢ P (⇑(s n) : (a : α) → β) ⋯

Tactic:
change P (s n) (s n).stronglyMeasurable

Premises used: MeasureTheory.SimpleFunc.stronglyMeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
c : β
⊢ P (⇑(SimpleFunc.const α c) : (a : α) → β) ⋯

Tactic:
const c
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
c : β
⊢ P (⇑(SimpleFunc.const α c) : (a : α) → β) ⋯

Tactic:
exact const c
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f_1 : α → β
hf : StronglyMeasurable f_1
s_1 : ℕ → α →ₛ β := hf.approx
n : ℕ
f g : α →ₛ β
s : Set α
hs : MeasurableSet s
Pf : P (⇑f : (a : α) → β) ⋯
Pg : P (⇑g : (a : α) → β) ⋯
pcw₁ : P (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)) ⋯
⊢ P (⇑(SimpleFunc.piecewise s hs f g) : (a : α) → β) ⋯

Tactic:
simp_rw [SimpleFunc.coe_piecewise]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f_1 : α → β
hf : StronglyMeasurable f_1
s_1 : ℕ → α →ₛ β := hf.approx
n : ℕ
f g : α →ₛ β
s : Set α
hs : MeasurableSet s
Pf : P (⇑f : (a : α) → β) ⋯
Pg : P (⇑g : (a : α) → β) ⋯
⊢ P (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)) ⋯

Tactic:
pcw f.stronglyMeasurable g.stronglyMeasurable hs Pf Pg

Premises used: MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f_1 : α → β
hf : StronglyMeasurable f_1
s_1 : ℕ → α →ₛ β := hf.approx
n : ℕ
f g : α →ₛ β
s : Set α
hs : MeasurableSet s
Pf : P (⇑f : (a : α) → β) ⋯
Pg : P (⇑g : (a : α) → β) ⋯
⊢ P (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)) ⋯

Tactic:
exact pcw f.stronglyMeasurable g.stronglyMeasurable hs Pf Pg

Premises used: MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
induction : ∀ (x : α →ₛ β), P (⇑x : (a : α) → β) ⋯
⊢ P (⇑(s n) : (a : α) → β) ⋯

Tactic:
induction s n with
  | const c => exact const c
  | @pcw f g s hs Pf Pg =>
    simp_rw [SimpleFunc.coe_piecewise]
    exact pcw f.stronglyMeasurable g.stronglyMeasurable hs Pf Pg

Premises used: MeasureTheory.SimpleFunc.coe_piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
β : Type u_5
inst : PseudoMetricSpace β
f g : α → β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (β := ℝ) fun (x : α) ↦ dist (f x) (g x)

Tactic:
continuous_dist.comp_stronglyMeasurable (hf.prodMk hg)

Premises used: continuous_dist, Continuous.comp_stronglyMeasurable, MeasureTheory.StronglyMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
β : Type u_5
inst : PseudoEMetricSpace β
f g : α → β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (x : α) ↦ edist (f x) (g x)

Tactic:
continuous_edist.comp_stronglyMeasurable (hf.prodMk hg)

Premises used: continuous_edist, Continuous.comp_stronglyMeasurable, MeasureTheory.StronglyMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
β : Type u_5
inst : SeminormedAddCommGroup β
f : α → β
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
continuous_norm.comp_stronglyMeasurable hf

Premises used: Continuous.comp_stronglyMeasurable, continuous_norm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
β : Type u_5
inst : SeminormedAddCommGroup β
f : α → β
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := ℝ≥0) fun (x : α) ↦ ‖f x‖₊

Tactic:
continuous_nnnorm.comp_stronglyMeasurable hf

Premises used: Continuous.comp_stronglyMeasurable, continuous_nnnorm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : StronglyMeasurable f
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ‖f x‖ₑ

Tactic:
(continuous_enorm.comp_stronglyMeasurable hf).measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, continuous_enorm, Continuous.comp_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := ℝ≥0) fun (x : α) ↦ (f x).toNNReal

Tactic:
continuous_real_toNNReal.comp_stronglyMeasurable hf

Premises used: Continuous.comp_stronglyMeasurable, continuous_real_toNNReal
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ let this : MeasurableSpace (E × E) := borel (E × E);
  BorelSpace.{u_5} (E × E)

Tactic:
borelize (E × E)

Premises used: Prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace (E × E) := borel (E × E)
this_1 : BorelSpace.{u_5} (E × E)
⊢ MeasurableSet.{u_1} (α := α) {a : α | f a ≤ g a}

Tactic:
(hf.prodMk hg).measurable isClosed_le_prod.measurableSet

Premises used: Set.Mem, MeasureTheory.StronglyMeasurable.measurable, setOf, IsClosed.measurableSet, Set.preimage, MeasureTheory.StronglyMeasurable.prodMk, isClosed_le_prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace (E × E) := borel (E × E)
this_1 : BorelSpace.{u_5} (E × E)
⊢ MeasurableSet.{u_1} (α := α) {a : α | f a ≤ g a}

Tactic:
exact (hf.prodMk hg).measurable isClosed_le_prod.measurableSet

Premises used: MeasureTheory.StronglyMeasurable.measurable, IsClosed.measurableSet, MeasureTheory.StronglyMeasurable.prodMk, isClosed_le_prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet.{u_1} (α := α) {a : α | f a < g a}

Tactic:
simpa only [lt_iff_le_not_ge] using (hf.measurableSet_le hg).inter (hg.measurableSet_le hf).compl

Premises used: lt_iff_le_not_ge, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᶠ[ae μ] g
rwa : MeasurableSet.{u_1} (α := α) {a : α | ¬f a ≤ g a}
⊢ f ≤ᶠ[ae (μ.trim hm)] g

Tactic:
rwa [EventuallyLE, ae_iff, trim_measurableSet_eq hm]

Premises used: MeasureTheory.ae_iff, MeasureTheory.trim_measurableSet_eq, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᶠ[ae μ] g
⊢ MeasurableSet.{u_1} (α := α) {a : α | ¬f a ≤ g a}

Tactic:
(hf.measurableSet_le hg).compl

Premises used: Set.Mem, setOf, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᶠ[ae μ] g
⊢ MeasurableSet.{u_1} (α := α) {a : α | ¬f a ≤ g a}

Tactic:
exact (hf.measurableSet_le hg).compl

Premises used: MeasureTheory.StronglyMeasurable.measurableSet_le, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ f ≤ᶠ[ae (μ.trim hm)] g ↔ f ≤ᶠ[ae μ] g

Tactic:
⟨ae_le_of_ae_le_trim, ae_le_trim_of_stronglyMeasurable hm hf hg⟩

Premises used: MeasureTheory.ae_le_of_ae_le_trim, Iff.intro, MeasureTheory.StronglyMeasurable.ae_le_trim_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ let this : MeasurableSpace (E × E) := borel (E × E);
  BorelSpace.{u_5} (E × E)

Tactic:
borelize (E × E)

Premises used: Prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace (E × E) := borel (E × E)
this_1 : BorelSpace.{u_5} (E × E)
⊢ MeasurableSet.{u_1} (α := α) {a : α | f a = g a}

Tactic:
(hf.prodMk hg).measurable isClosed_diagonal.measurableSet

Premises used: Set.Mem, MeasureTheory.StronglyMeasurable.measurable, setOf, IsClosed.measurableSet, isClosed_diagonal, Set.diagonal, Set.preimage, MeasureTheory.StronglyMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace (E × E) := borel (E × E)
this_1 : BorelSpace.{u_5} (E × E)
⊢ MeasurableSet.{u_1} (α := α) {a : α | f a = g a}

Tactic:
exact (hf.prodMk hg).measurable isClosed_diagonal.measurableSet

Premises used: MeasureTheory.StronglyMeasurable.measurable, IsClosed.measurableSet, isClosed_diagonal, MeasureTheory.StronglyMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
rwa : MeasurableSet.{u_1} (α := α) {a : α | ¬f a = g a}
⊢ f =ᶠ[ae (μ.trim hm)] g

Tactic:
rwa [EventuallyEq, ae_iff, trim_measurableSet_eq hm]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_iff, MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ MeasurableSet.{u_1} (α := α) {a : α | ¬f a = g a}

Tactic:
(hf.measurableSet_eq_fun hg).compl

Premises used: Set.Mem, setOf, MeasurableSet.compl, MeasureTheory.StronglyMeasurable.measurableSet_eq_fun
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ MeasurableSet.{u_1} (α := α) {a : α | ¬f a = g a}

Tactic:
exact (hf.measurableSet_eq_fun hg).compl

Premises used: MeasurableSet.compl, MeasureTheory.StronglyMeasurable.measurableSet_eq_fun
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ f =ᶠ[ae (μ.trim hm)] g ↔ f =ᶠ[ae μ] g

Tactic:
⟨ae_eq_of_ae_eq_trim, ae_eq_trim_of_stronglyMeasurable hm hf hg⟩

Premises used: MeasureTheory.ae_eq_of_ae_eq_trim, Iff.intro, MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
x : α
hx : x ∈ s
n : ℕ
rw : Eq.{u_2 + 1} (α := β) (s.indicator (⇑(hf.approx n) : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
rw₁ rw₂ : Eq.{u_2 + 1} (α := β) ((hf.approx n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
⊢ Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)

Tactic:
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]

Premises used: Set.indicator_of_mem, MeasureTheory.SimpleFunc.coe_restrict
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
⊢ ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)

Tactic:
have hg_eq : ∀ x ∈ s, ∀ n, g_seq_s n x = hf.approx n x := by
    intro x hx n
    rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
x : α
hx : x ∉ s
n : ℕ
rw : Eq.{u_2 + 1} (α := β) (s.indicator (⇑(hf.approx n) : (a : α) → β) x) 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := β) 0 0
⊢ Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)

Tactic:
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_notMem hx]

Premises used: MeasureTheory.SimpleFunc.coe_restrict, Set.indicator_of_notMem