awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
x : MeasurableSpace α
inst : TopologicalSpace β
p : α → Prop
x_1 : DecidablePred p
hp : MeasurableSet.{u_1} (α := α) {a : α | p a}
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ if p x then f x else g x

Tactic:
StronglyMeasurable.piecewise hp hf hg

Premises used: Set.Mem, MeasureTheory.StronglyMeasurable.piecewise, Set.piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ StronglyMeasurable (Function.extend g f g')

Tactic:
⟨fun n => SimpleFunc.extend (hf.approx n) g hg (hg'.approx n), ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.extend, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
refine :
  ∀ (x : γ),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
      (𝓝 (Function.extend g f g' x))
⊢ StronglyMeasurable (Function.extend g f g')

Tactic:
refine ⟨fun n => SimpleFunc.extend (hf.approx n) g hg (hg'.approx n), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
pos :
  ∀ (hx : ∃ (y : α), g y = x),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
      (𝓝 (Function.extend g f g' x))
neg :
  ∀ (hx : ¬∃ (y : α), g y = x),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
      (𝓝 (Function.extend g f g' x))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))

Tactic:
by_cases hx : ∃ y, g y = x
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ∃ (y : α), g y = x
pos :
  ∀ (y : α),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) (g y)) atTop
      (𝓝 (Function.extend g f g' (g y)))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))

Tactic:
rcases hx with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
y : α
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) (g y)) atTop
    (𝓝 (Function.extend g f g' (g y)))

Tactic:
simpa only [SimpleFunc.extend_apply, hg.injective, Injective.extend_apply] using
      hf.tendsto_approx y

Premises used: Function.Injective.extend_apply, MeasurableEmbedding.injective, MeasureTheory.StronglyMeasurable.tendsto_approx, MeasureTheory.SimpleFunc.extend_apply
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ (y : α), g y = x
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))

Tactic:
simpa only [hx, SimpleFunc.extend_apply', not_false_iff, extend_apply'] using
      hg'.tendsto_approx x

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx, Function.extend_apply', MeasureTheory.SimpleFunc.extend_apply', not_false_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
x : MeasurableSpace α
x_1 : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hne : ∀ (a : γ), Nonempty β
⊢ ∃ (f' : γ → β), StronglyMeasurable f' ∧ f' ∘ g = f

Tactic:
⟨Function.extend g f fun x => Classical.choice (hne x),
    hg.stronglyMeasurable_extend hf (stronglyMeasurable_const' fun _ _ => rfl),
    funext fun _ => hg.injective.extend_apply _ _ _⟩

Premises used: Classical.choice, Function.Injective.extend_apply, MeasurableEmbedding.stronglyMeasurable_extend, funext, Function.extend, MeasurableEmbedding.injective, And.intro, Exists.intro, MeasureTheory.stronglyMeasurable_const', rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
⊢ Nontrivial β

Tactic:
nontriviality β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabit : ∀ (inhabited_h : Inhabited β), StronglyMeasurable f
⊢ StronglyMeasurable f

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
suffices :
  Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default) =
    f
⊢ StronglyMeasurable f

Tactic:
suffices Function.extend Subtype.val (fun x : s ↦ f x)
      (Function.extend (↑) (fun x : t ↦ f x) fun _ ↦ default) = f from
    this ▸ (MeasurableEmbedding.subtype_coe hs).stronglyMeasurable_extend hc <|
      (MeasurableEmbedding.subtype_coe ht).stronglyMeasurable_extend hd stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
h₁ :
  ∀ (x : α),
    Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
        (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
          default)
        x =
      f x
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default) =
    f

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
pos :
  ∀ (hxs : x ∈ s),
    Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
        (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
          default)
        x =
      f x
neg :
  ∀ (hxs : x ∉ s),
    Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
        (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
          default)
        x =
      f x
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x

Tactic:
by_cases hxs : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∈ s
⊢ x ∈ s

Tactic:
hxs
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∈ s
pos :
  ∀ (x : { x : α // x ∈ s }),
    Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
        (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
          default)
        (↑x : α) =
      f (↑x : α)
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x

Tactic:
lift x to s using hxs
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : { x : α // x ∈ s }
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      (↑x : α) =
    f (↑x : α)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∉ s
⊢ x ∈ t

Tactic:
(h trivial).resolve_left hxs

Premises used: trivial, Or.resolve_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∉ s
neg :
  ∀ (x : { x : α // x ∈ t }) (hxs : (↑x : α) ∉ s),
    Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
        (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
          default)
        (↑x : α) =
      f (↑x : α)
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x

Tactic:
lift x to t using (h trivial).resolve_left hxs

Premises used: trivial, Or.resolve_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : { x : α // x ∈ t }
hxs : (↑x : α) ∉ s
neg : ¬∃ (a : { x : α // x ∈ s }), (↑a : α) = (↑x : α)
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      (↑x : α) =
    f (↑x : α)

Tactic:
rw [extend_apply', Subtype.coe_injective.extend_apply]

Premises used: Function.Injective.extend_apply, Subtype.coe_injective, Function.extend_apply'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : { x : α // x ∈ t }
hxs : (↑x : α) ∉ s
⊢ ¬∃ (a : { x : α // x ∈ s }), (↑a : α) = (↑x : α)

Tactic:
fun ⟨y, hy⟩ ↦ hxs <| hy ▸ y.2

Premises used: False, Eq.rec, _private.0.stronglyMeasurable_of_stronglyMeasurable_union_cover.match_1, Not, Subtype.property
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : { x : α // x ∈ t }
hxs : (↑x : α) ∉ s
⊢ ¬∃ (a : { x : α // x ∈ s }), (↑a : α) = (↑x : α)

Tactic:
exact fun ⟨y, hy⟩ ↦ hxs <| hy ▸ y.2
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s : Set α
hs : MeasurableSet s
h₁ : StronglyMeasurable (s.restrict (π := fun (a : α) ↦ β) f)
h₂ : StronglyMeasurable (sᶜ.restrict (π := fun (a : α) ↦ β) f)
⊢ StronglyMeasurable f

Tactic:
stronglyMeasurable_of_stronglyMeasurable_union_cover s sᶜ hs hs.compl (union_compl_self s).ge h₁
    h₂

Premises used: Eq.ge, stronglyMeasurable_of_stronglyMeasurable_union_cover, Compl.compl, Set.union_compl_self, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
hf : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
⊢ StronglyMeasurable (s.indicator f)

Tactic:
hf.piecewise hs stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, Set.indicator, MeasureTheory.StronglyMeasurable.piecewise
-- 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
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 : 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
⊢ 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 : 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
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 : 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 : ℕ
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 : 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 : ℕ
c : β
s_1 : Set α
hs : MeasurableSet s_1
⊢ P (⇑(SimpleFunc.piecewise s_1 hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → β) ⋯

Tactic:
ind c hs

Premises used: Set.indicator, Set.piecewise, ite
-- 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 : ℕ
c : β
s_1 : Set α
hs : MeasurableSet s_1
⊢ P (⇑(SimpleFunc.piecewise s_1 hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → β) ⋯

Tactic:
exact ind c hs
-- 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:
add f.stronglyMeasurable g.stronglyMeasurable (f + g).stronglyMeasurable h_supp hf hg

Premises used: HAdd.hAdd, MeasureTheory.SimpleFunc.stronglyMeasurable