awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : TopologicalSpace Z
inst_1 : PseudoMetrizableSpace Z
inst_2 : T1Space Z
hg : StronglyMeasurable g
this : MeasurableSpace Z := borel Z
this_1 : BorelSpace Z
⊢ Function.FactorsThrough g f

Tactic:
hg.measurable.factorsThrough

Premises used: MeasureTheory.StronglyMeasurable.measurable, Measurable.factorsThrough
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : TopologicalSpace Z
inst_1 : PseudoMetrizableSpace Z
inst_2 : T1Space Z
hg : StronglyMeasurable g
this : MeasurableSpace Z := borel Z
this_1 : BorelSpace Z
⊢ Function.FactorsThrough g f

Tactic:
exact hg.measurable.factorsThrough

Premises used: MeasureTheory.StronglyMeasurable.measurable, Measurable.factorsThrough
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
z : Z
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (fun (x : X) ↦ z) = h ∘ f

Tactic:
⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩

Premises used: MeasureTheory.stronglyMeasurable_const, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
z : Z
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (fun (x : X) ↦ z) = h ∘ f

Tactic:
exact ⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g₁ g₂ : X → Z
s : Set X
hg₁ : StronglyMeasurable g₁
hg₂ : StronglyMeasurable g₂
hs : MeasurableSet s
h₁ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₁ = h ∘ f
h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f
pcw :
  ∀ (t : Set Y) (ht : MeasurableSet t),
    ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ s.piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f

Tactic:
obtain ⟨t, ht, rfl⟩ := hs

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g₁ g₂ : X → Z
hg₁ : StronglyMeasurable g₁
hg₂ : StronglyMeasurable g₂
h₁ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₁ = h ∘ f
h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f
t : Set Y
ht : MeasurableSet t
pcw :
  ∀ (h₁ : Y → Z) (mh₁ : StronglyMeasurable h₁) (hg₁ : StronglyMeasurable (h₁ ∘ f)),
    ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) g₂ = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f

Tactic:
obtain ⟨h₁, mh₁, rfl⟩ := h₁

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g₂ : X → Z
hg₂ : StronglyMeasurable g₂
h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
pcw :
  ∀ (h₂ : Y → Z) (mh₂ : StronglyMeasurable h₂) (hg₂ : StronglyMeasurable (h₂ ∘ f)),
    ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) g₂ = h ∘ f

Tactic:
obtain ⟨h₂, mh₂, rfl⟩ := h₂

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
h₂ : Y → Z
mh₂ : StronglyMeasurable h₂
hg₂ : StronglyMeasurable (h₂ ∘ f)
rw rw₁ :
  (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) =
    (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f)
⊢ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) = t.piecewise (β := fun (a : Y) ↦ Z) h₁ h₂ ∘ f

Tactic:
rw [piecewise_comp]

Premises used: Set.piecewise_comp
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
h₂ : Y → Z
mh₂ : StronglyMeasurable h₂
hg₂ : StronglyMeasurable (h₂ ∘ f)
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) = h ∘ f

Tactic:
exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
h₂ : Y → Z
mh₂ : StronglyMeasurable h₂
hg₂ : StronglyMeasurable (h₂ ∘ f)
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) = h ∘ f

Tactic:
classical
    exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₁ : ∀ (n : ℕ), ∃ (h : Y → Z), StronglyMeasurable h ∧ g n = h ∘ f
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
lim :
  ∀ (h : (n : ℕ) → Y → Z) (mh : ∀ (n : ℕ), StronglyMeasurable (h n)) (hh : ∀ (n : ℕ), g n = h n ∘ f),
    ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f

Tactic:
choose h mh hh using h₁
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f

Tactic:
⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩

Premises used: Filter.atTop, And.intro, Exists.intro, MeasureTheory.StronglyMeasurable.limUnder, Filter.limUnder
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
lim : i = (fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f

Tactic:
refine ⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
lim : ∀ (x : X), i x = ((fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f) x
⊢ i = (fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
lim : Tendsto (fun (x_1 : ℕ) ↦ h x_1 (f x)) atTop (𝓝 (i x))
⊢ i x = ((fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f) x

Tactic:
rw [Function.comp_apply, Tendsto.limUnder_eq]

Premises used: Function.comp_apply, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ Tendsto (fun (x_1 : ℕ) ↦ h x_1 (f x)) atTop (𝓝 (i x))

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
hg : StronglyMeasurable g
mX : MeasurableSpace X := MeasurableSpace.comap f mY
const : ∀ (z : Z), ∃ (h : Y → Z), StronglyMeasurable h ∧ (fun (x : X) ↦ z) = h ∘ f
pcw :
  ∀ ⦃g₁ g₂ : X → Z⦄ {s : Set X} (hg₁ : StronglyMeasurable g₁) (hg₂ : StronglyMeasurable g₂) (hs : MeasurableSet s)
    (h₁ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₁ = h ∘ f) (h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f),
    ∃ (h : Y → Z), StronglyMeasurable h ∧ s.piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f
lim :
  ∀ ⦃g : ℕ → X → Z⦄ ⦃i : X → Z⦄ (hg : ∀ (n : ℕ), StronglyMeasurable (g n)) (hi : StronglyMeasurable i)
    (h₁ : ∀ (n : ℕ), ∃ (h : Y → Z), StronglyMeasurable h ∧ g n = h ∘ f)
    (h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))), ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ g = h ∘ f

Tactic:
induction g, hg using StronglyMeasurable.induction' with
  | const z => exact ⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩
  | @pcw g₁ g₂ s hg₁ hg₂ hs h₁ h₂ =>
    obtain ⟨t, ht, rfl⟩ := hs
    obtain ⟨h₁, mh₁, rfl⟩ := h₁
    obtain ⟨h₂, mh₂, rfl⟩ := h₂
    classical
    exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
  | @lim g i hg hi h₁ h₂ =>
    choose h mh hh using h₁
    refine ⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
    ext x
    rw [Function.comp_apply, Tendsto.limUnder_eq]
    simp_all

Premises used: MeasureTheory.StronglyMeasurable.induction', Filter.lim, Function.comp_apply, Filter.Tendsto.limUnder_eq, rfl, MeasureTheory.Filtration.const
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : MeasurableSpace Z
inst_2 : StandardBorelSpace Z
hg : Measurable g
this : UpgradedStandardBorel Z := upgradeStandardBorel Z
obtain : ∀ (h : Y → Z) (mh : StronglyMeasurable h) (hh : g = h ∘ f), ∃ (h : Y → Z), Measurable h ∧ g = h ∘ f
⊢ ∃ (h : Y → Z), Measurable h ∧ g = h ∘ f

Tactic:
obtain ⟨h, mh, hh⟩ := hg.stronglyMeasurable.exists_eq_measurable_comp

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.exists_eq_measurable_comp
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : MeasurableSpace Z
inst_2 : StandardBorelSpace Z
hg : Measurable g
this : UpgradedStandardBorel Z := upgradeStandardBorel Z
h : Y → Z
mh : StronglyMeasurable h
hh : g = h ∘ f
⊢ ∃ (h : Y → Z), Measurable h ∧ g = h ∘ f

Tactic:
⟨h, mh.measurable, hh⟩

Premises used: MeasureTheory.StronglyMeasurable.measurable, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : MeasurableSpace Z
inst_2 : StandardBorelSpace Z
hg : Measurable g
this : UpgradedStandardBorel Z := upgradeStandardBorel Z
h : Y → Z
mh : StronglyMeasurable h
hh : g = h ∘ f
⊢ ∃ (h : Y → Z), Measurable h ∧ g = h ∘ f

Tactic:
exact ⟨h, mh.measurable, hh⟩
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
Z : Type u_3
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → MeasurableSpace (X i)
f : ((i : ι) → X i) → Z
inst_1 : Preorder ι
i : ι
inst_2 : MeasurableSpace Z
inst_3 : MeasurableSingletonClass Z
hf : Measurable f
⊢ DependsOn (α := X) f (Iic i)

Tactic:
dependsOn_iff_factorsThrough.2 hf.factorsThrough

Premises used: Iff.mpr, Measurable.factorsThrough, dependsOn_iff_factorsThrough
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
Z : Type u_3
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → MeasurableSpace (X i)
f : ((i : ι) → X i) → Z
inst_1 : Preorder ι
i : ι
inst_2 : TopologicalSpace Z
inst_3 : PseudoMetrizableSpace Z
inst_4 : T1Space Z
hf : StronglyMeasurable f
⊢ DependsOn (α := X) f (Iic i)

Tactic:
dependsOn_iff_factorsThrough.2 hf.factorsThrough

Premises used: Iff.mpr, MeasureTheory.StronglyMeasurable.factorsThrough, dependsOn_iff_factorsThrough
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
Z : Type u_3
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → MeasurableSpace (X i)
f : ((i : ι) → X i) → Z
s : Finset ι
inst_1 : MeasurableSpace Z
inst_2 : MeasurableSingletonClass Z
hf : Measurable f
⊢ DependsOn (α := X) f (↑s : Set ι)

Tactic:
dependsOn_iff_factorsThrough.2 hf.factorsThrough

Premises used: Iff.mpr, Measurable.factorsThrough, dependsOn_iff_factorsThrough
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
Z : Type u_3
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → MeasurableSpace (X i)
f : ((i : ι) → X i) → Z
s : Finset ι
inst_1 : TopologicalSpace Z
inst_2 : PseudoMetrizableSpace Z
inst_3 : T1Space Z
hf : StronglyMeasurable f
⊢ DependsOn (α := X) f (↑s : Set ι)

Tactic:
dependsOn_iff_factorsThrough.2 hf.factorsThrough

Premises used: Iff.mpr, MeasureTheory.StronglyMeasurable.factorsThrough, dependsOn_iff_factorsThrough
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
x : R
⊢ MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊x⌋})

Tactic:
simpa only [Int.preimage_floor_singleton] using measurableSet_Ico

Premises used: measurableSet_Ico, Int.preimage_floor_singleton
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
α : Type u_1
R : Type u_2
inst : MeasurableSpace α
inst_1 : Ring R
inst_2 : LinearOrder R
inst_3 : FloorRing R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
inst_6 : MeasurableSpace R
inst_7 : OpensMeasurableSpace R
f : α → R
hf : Measurable f
⊢ Measurable (β := ℤ) fun (x : α) ↦ ⌊f x⌋

Tactic:
Int.measurable_floor.comp hf

Premises used: Measurable.comp, Int.measurable_floor
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
x : R
⊢ MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈x⌉})

Tactic:
simpa only [Int.preimage_ceil_singleton] using measurableSet_Ioc

Premises used: Int.preimage_ceil_singleton, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
α : Type u_1
R : Type u_2
inst : MeasurableSpace α
inst_1 : Ring R
inst_2 : LinearOrder R
inst_3 : FloorRing R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
inst_6 : MeasurableSpace R
inst_7 : OpensMeasurableSpace R
f : α → R
hf : Measurable f
⊢ Measurable (β := ℤ) fun (x : α) ↦ ⌈f x⌉

Tactic:
Int.measurable_ceil.comp hf

Premises used: Measurable.comp, Int.measurable_ceil
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
rw : MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1))
⊢ MeasurableSet (Int.fract ⁻¹' s)

Tactic:
rw [Int.preimage_fract]

Premises used: Int.preimage_fract
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1))

Tactic:
MeasurableSet.iUnion fun z => measurable_id.sub_const _ (hs.inter measurableSet_Ico)

Premises used: Int.cast, measurable_id, measurableSet_Ico, Measurable.sub_const, MeasurableSet.iUnion, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1))

Tactic:
exact MeasurableSet.iUnion fun z => measurable_id.sub_const _ (hs.inter measurableSet_Ico)

Premises used: measurable_id, measurableSet_Ico, Measurable.sub_const, MeasurableSet.iUnion, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
α : Type u_1
R : Type u_2
inst : MeasurableSpace α
inst_1 : Ring R
inst_2 : LinearOrder R
inst_3 : FloorRing R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
inst_6 : MeasurableSpace R
inst_7 : IsStrictOrderedRing R
inst_8 : BorelSpace R
f : α → R
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := R) fun (x : α) ↦ Int.fract (f x)

Tactic:
measurable_fract.comp hf

Premises used: Measurable.comp, Int.fract, measurable_fract
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
simp : MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x + (↑m : R)) ⁻¹' s ∩ Ico 0 1)
⊢ MeasurableSet (Int.fract '' s)

Tactic:
simp only [Int.image_fract, sub_eq_add_neg, image_add_right']

Premises used: sub_eq_add_neg, Int.image_fract, Set.image_add_right'
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x + (↑m : R)) ⁻¹' s ∩ Ico 0 1)

Tactic:
MeasurableSet.iUnion fun m => (measurable_add_const _ hs).inter measurableSet_Ico

Premises used: Int.cast, measurableSet_Ico, MeasurableSet.iUnion, MeasurableAdd.measurable_add_const, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x + (↑m : R)) ⁻¹' s ∩ Ico 0 1)

Tactic:
exact MeasurableSet.iUnion fun m => (measurable_add_const _ hs).inter measurableSet_Ico

Premises used: measurableSet_Ico, MeasurableSet.iUnion, MeasurableAdd.measurable_add_const, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
inst_7 : IsStrictOrderedRing R
n : R
inl : ∀ (h : ⌊n⌋₊ = 0), MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})
inr : ∀ (h : ⌊n⌋₊ ≠ 0), MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})
⊢ MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})

Tactic:
rcases eq_or_ne ⌊n⌋₊ 0 with h | h

Premises used: Nat.floor, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
inst_7 : IsStrictOrderedRing R
n : R
h : ⌊n⌋₊ = 0
⊢ MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})

Tactic:
simp [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]

Premises used: Nat.preimage_floor_of_ne_zero, Nat.floor_eq_zero
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
inst_7 : IsStrictOrderedRing R
n : R
h : ⌊n⌋₊ ≠ 0
⊢ MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})

Tactic:
simp [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]

Premises used: Nat.preimage_floor_of_ne_zero, Nat.floor_eq_zero
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
α : Type u_1
R : Type u_2
inst : MeasurableSpace α
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
inst_6 : MeasurableSpace R
inst_7 : OpensMeasurableSpace R
f : α → R
inst_8 : IsStrictOrderedRing R
hf : Measurable f
⊢ Measurable (β := ℕ) fun (x : α) ↦ ⌊f x⌋₊

Tactic:
Nat.measurable_floor.comp hf

Premises used: Nat.measurable_floor, Measurable.comp
-- Module: Mathlib.MeasureTheory.Function.Floor
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
n : R
inl : ∀ (h : ⌈n⌉₊ = 0), MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})
inr : ∀ (h : ⌈n⌉₊ ≠ 0), MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})
⊢ MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})

Tactic:
rcases eq_or_ne ⌈n⌉₊ 0 with h | h

Premises used: Nat.ceil, eq_or_ne, OfNat.ofNat