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
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) ⋯ else fun (_b : δ) ↦ sSup ∅
this_1 : ∀ i ∈ s, Measurable (g i)
this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b
b : δ
hb : ∀ (i : ι) (hi : i ∈ s), f i b = g i b
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (⨆ i ∈ s, g i b)

Tactic:
iSup_congr fun i => iSup_congr (hb i)

Premises used: iSup_congr
-- 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
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) ⋯ else fun (_b : δ) ↦ sSup ∅
this_1 : ∀ i ∈ s, Measurable (g i)
this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b
b : δ
hb : ∀ (i : ι) (hi : i ∈ s), f i b = g i b
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (⨆ i ∈ s, g i b)

Tactic:
exact iSup_congr fun i => iSup_congr (hb i)

Premises used: iSup_congr
-- 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
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
let let₁ let₂ : AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
let₃ :
  let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) ⋯ else fun (_b : δ) ↦ sSup ∅;
  ∀ (this : ∀ i ∈ s, Measurable (g i)), AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
let₄ :
  let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) ⋯ else fun (_b : δ) ↦ sSup ∅;
  ∀ (this : ∀ i ∈ s, Measurable (g i)),
    EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) fun (b : δ) ↦ ⨆ i ∈ s, g i b
let₅ :
  let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) ⋯ else fun (_b : δ) ↦ sSup ∅;
  ∀ (this : ∀ i ∈ s, Measurable (g i)) (this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b),
    EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) fun (b : δ) ↦ ⨆ i ∈ s, g i b
h :
  let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) ⋯ else fun (_b : δ) ↦ sSup ∅;
  ∀ (this : ∀ i ∈ s, Measurable (g i)) (this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b) (b : δ)
    (hb : ∀ (i : ι) (hi : i ∈ s), f i b = g i b), Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (⨆ i ∈ s, g i b)
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ

Tactic:
classical
  let g : ι → δ → α := fun i ↦ if hi : i ∈ s then (hf i hi).mk (f i) else fun _b ↦ sSup ∅
  have : ∀ i ∈ s, Measurable (g i) := by
    intro i hi
    simpa [g, hi] using (hf i hi).measurable_mk
  refine ⟨fun b ↦ ⨆ (i) (_ : i ∈ s), g i b, .biSup s hs this, ?_⟩
  have : ∀ i ∈ s, ∀ᵐ b ∂μ, f i b = g i b :=
    fun i hi ↦ by simpa [g, hi] using (hf i hi).ae_eq_mk
  filter_upwards [(ae_ball_iff hs).2 this] with b hb
  exact iSup_congr fun i => iSup_congr (hb i)
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨅ i ∈ s, f i b

Tactic:
.biSup (α := αᵒᵈ) s hs hf

Premises used: Measurable.biSup, iInf, 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 α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨅ i ∈ s, f i b) μ

Tactic:
.biSup (α := αᵒᵈ) s hs hf

Premises used: iInf, AEMeasurable.biSup, 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 α
ι : 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
⊢ Countable.{max 1 (u_6 + 1)} (Subtype p)

Tactic:
have : Countable (Subtype p) := hv.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 α
ι : 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 : Countable.{max 1 (u_6 + 1)} (Subtype p)
inl :
  ∀ (hp : IsEmpty.{max 1 (u_6 + 1)} (Subtype p)),
    Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
inr :
  ∀ (hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)),
    Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v

Tactic:
rcases isEmpty_or_nonempty (Subtype p) with hp | hp

Premises used: isEmpty_or_nonempty, Subtype
-- 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 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : IsEmpty.{max 1 (u_6 + 1)} (Subtype p)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v

Tactic:
simp [hv.liminf_eq_sSup_iUnion_iInter]

Premises used: Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, Filter.HasCountableBasis.toHasBasis
-- 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 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
pos :
  ∀ (H : ∃ (j : Subtype p), s (↑j : ι') = ∅),
    Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
neg :
  ∀ (H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅),
    Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v

Tactic:
by_cases H : ∃ (j : Subtype p), s j = ∅

Premises used: Subtype
-- 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 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ∃ (j : Subtype p), s (↑j : ι') = ∅
pos :
  Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x) then
        sSup ∅
      else
        ⨆ (j : Subtype p),
          ⨅ (i : (↑(s (↑(liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (x_1 : ι) ↦ f x_1 x) s p j) : ι')) : Type u_5)),
            f (↑i : ι) x
pos₁ : Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup univ
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v

Tactic:
simp_rw [hv.liminf_eq_ite, if_pos H, measurable_const]

Premises used: Filter.HasBasis.liminf_eq_ite, if_pos, measurable_const, Filter.HasCountableBasis.toHasBasis
-- 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 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
neg :
  Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x) then
      sSup ∅
    else
      ⨆ (j : Subtype p),
        ⨅ (i : (↑(s (↑(liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (x_1 : ι) ↦ f x_1 x) s p j) : ι')) : Type u_5)),
          f (↑i : ι) x
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v

Tactic:
simp_rw [hv.liminf_eq_ite, if_neg H]

Premises used: Filter.HasBasis.liminf_eq_ite, if_neg, Filter.HasCountableBasis.toHasBasis
-- 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 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
⊢ ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)

Tactic:
have : ∀ i, Countable (s i) := fun i ↦ countable_coe_iff.2 (hs i)
-- 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)}
⊢ ∀ (j : Subtype p), MeasurableSet (m j)

Tactic:
have m_meas : ∀ j, MeasurableSet (m j) :=
    fun j ↦ measurableSet_bddBelow_range (fun (i : s j) ↦ hf i)
-- 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)
rw : MeasurableSet.{u_4} (α := δ) (⋂ (i : Subtype p), {x : δ | x ∉ m i})
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}

Tactic:
rw [setOf_forall]

Premises used: Set.setOf_forall
-- 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)
⊢ MeasurableSet.{u_4} (α := δ) (⋂ (i : Subtype p), {x : δ | x ∉ m i})

Tactic:
MeasurableSet.iInter (fun j ↦ (m_meas j).compl)

Premises used: MeasurableSet.compl, MeasurableSet.iInter
-- 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)
⊢ MeasurableSet.{u_4} (α := δ) (⋂ (i : Subtype p), {x : δ | x ∉ m i})

Tactic:
exact MeasurableSet.iInter (fun j ↦ (m_meas j).compl)

Premises used: MeasurableSet.compl, MeasurableSet.iInter
-- 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)
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}

Tactic:
have mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j} := by
    rw [setOf_forall]
    exact MeasurableSet.iInter (fun j ↦ (m_meas j).compl)
-- 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}
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x) then
      sSup ∅
    else
      ⨆ (j : Subtype p),
        ⨅ (i : (↑(s (↑(liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (x_1 : ι) ↦ f x_1 x) s p j) : ι')) : Type u_5)),
          f (↑i : ι) x

Tactic:
measurable_const.piecewise mc_meas <| .iSup fun j ↦ ?_

Premises used: Set.Mem, Measurable.piecewise, Measurable.iSup, measurable_const, Set.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 : ∀ (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}
neg :
  ∀ (j : Subtype p),
    Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
      ⨅ (i : (↑(s (↑(liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (x_1 : ι) ↦ f x_1 x) s p j) : ι')) : Type u_5)),
        f (↑i : ι) x
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x) then
      sSup ∅
    else
      ⨆ (j : Subtype p),
        ⨅ (i : (↑(s (↑(liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (x_1 : ι) ↦ f x_1 x) s p j) : ι')) : Type u_5)),
          f (↑i : ι) x

Tactic:
refine measurable_const.piecewise mc_meas <| .iSup fun j ↦ ?_

Premises used: Measurable.piecewise, measurable_const
-- 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
⊢ ∀ (j : Subtype p), Measurable (F0 j)

Tactic:
have F0_meas : ∀ j, Measurable (F0 j) := fun j ↦ .iInf (fun (i : s j) ↦ hf i)
-- 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)
neg :
  let F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x;
  ∀ (hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x), Measurable F1
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    ⨅ (i : (↑(s (↑(liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (x_1 : ι) ↦ f x_1 x) s p j) : ι')) : Type u_5)),
      f (↑i : ι) x

Tactic:
set F1 : δ → α := fun x ↦ F0 (reparam x j) x with hF1
-- 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) ⋯
x : δ
pos : ∀ (H : ∃ (k : Subtype p), x ∈ m k), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
neg : ∀ (H : ∀ (k : Subtype p), x ∉ m k), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
⊢ ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
by_cases! H : ∃ k, x ∈ m k