awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∉ m j
⊢ reparam x j = g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)

Tactic:
have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∉ m j
this : reparam x j = g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
⊢ F1 x = F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x

Tactic:
simp only [hF1, this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
⊢ F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x

Tactic:
have : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find (Z x))) x := by
    ext x
    have A : reparam x j = if x ∈ m j then j else g (Nat.find (Z x)) := rfl
    split_ifs with hjx
    · have : reparam x j = j := by rw [A, if_pos hjx]
      simp only [hF1, this]
    · have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
      simp only [hF1, this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
neg :
  Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
⊢ Measurable F1

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
neg :
  Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x

Tactic:
apply Measurable.piecewise (m_meas j) (F0_meas j)

Premises used: Measurable.piecewise
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
apply : ∀ (n : ℕ), MeasurableSet.{u_4} (α := δ) {x : δ | x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k}
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x

Tactic:
apply Measurable.find (fun n ↦ F0_meas (g n)) (fun n ↦ ?_)

Premises used: Measurable.find
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
n : ℕ
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k}

Tactic:
(m_meas (g n)).union mc_meas

Premises used: Set.union, Set.Mem, setOf, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
n : ℕ
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k}

Tactic:
exact (m_meas (g n)).union mc_meas

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
u : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hu : u.HasCountableBasis p s
hs : ∀ (i : ι'), (s i).Countable
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ limsup (fun (i : ι) ↦ f i x) u

Tactic:
.liminf' (α := αᵒᵈ) hf hu hs

Premises used: Filter.limsSup, setOf, Filter.limsup, Measurable.liminf', OrderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
f : ℕ → δ → α
hf : ∀ (i : ℕ), Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ Filter.liminf (fun (i : ℕ) ↦ f i x) atTop

Tactic:
.liminf' hf atTop_countable_basis fun _ => to_countable _

Premises used: Set.Ici, Filter.atTop_countable_basis, Measurable.liminf', Set.to_countable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
f : ℕ → δ → α
hf : ∀ (i : ℕ), Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ Filter.limsup (fun (i : ℕ) ↦ f i x) atTop

Tactic:
.limsup' hf atTop_countable_basis fun _ => to_countable _

Premises used: Set.Ici, Measurable.limsup', Filter.atTop_countable_basis, Set.to_countable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
hd : Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)
h : MeasurableSet (s ∩ f ⁻¹' Ioi 0)
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)

Tactic:
rw [← measure_union]

Premises used: MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' insert 0 (Ioi 0)) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici 0) : ℝ≥0∞)
rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici ⊥) : ℝ≥0∞)
rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' univ) : ℝ≥0∞)
rw₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ univ) : ℝ≥0∞)
rw₇ rw₈ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)

Tactic:
rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]

Premises used: Set.inter_univ, Set.singleton_union, Set.Ioi_insert, Set.preimage_union, Set.preimage_univ, bot_eq_zero, Set.inter_union_distrib_left, Set.Ici_bot
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)

Tactic:
disjoint_singleton_left.mpr self_notMem_Ioi
        |>.preimage f |>.inter_right' s |>.inter_left' s

Premises used: Iff.mpr, Set.disjoint_singleton_left, Disjoint.inter_left', Set.self_notMem_Ioi, Disjoint.inter_right', Disjoint.preimage
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)

Tactic:
exact disjoint_singleton_left.mpr self_notMem_Ioi
        |>.preimage f |>.inter_right' s |>.inter_left' s

Premises used: Iff.mpr, Set.disjoint_singleton_left, Disjoint.inter_left', Set.self_notMem_Ioi, Disjoint.inter_right', Disjoint.preimage
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)

Tactic:
hs.inter (hf measurableSet_Ioi)

Premises used: measurableSet_Ioi, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)

Tactic:
exact hs.inter (hf measurableSet_Ioi)

Premises used: measurableSet_Ioi, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)

Tactic:
have A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0) := by
    rw [← measure_union]
    · rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
    · exact disjoint_singleton_left.mpr self_notMem_Ioi
        |>.preimage f |>.inter_right' s |>.inter_left' s
    · exact hs.inter (hf measurableSet_Ioi)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞} ∪ s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
hd : Disjoint (s ∩ f ⁻¹' {∞}) (s ∩ f ⁻¹' Ioo 0 ∞)
h : MeasurableSet (s ∩ f ⁻¹' Ioo 0 ∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)

Tactic:
rw [← measure_union]

Premises used: MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞} ∪ s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)

Tactic:
rw [← inter_union_distrib_left]

Premises used: Set.inter_union_distrib_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
h : f ⁻¹' Ioi 0 = f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞)) : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
h : ∀ (x : α), x ∈ f ⁻¹' Ioi 0 ↔ x ∈ f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞
⊢ f ⁻¹' Ioi 0 = f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
x : α
⊢ f x = ∞ ∨ f x < ∞

Tactic:
eq_or_lt_of_le le_top

Premises used: eq_or_lt_of_le, le_top