awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) fun (b : δ) ↦ ⨆ i ∈ s, g i b
have h : ∀ (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: filter_upwards [(ae_ball_iff hs).2 this] with b hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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) μ
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
have let₃ : let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) sorry else fun (_b : δ) ↦ sSup ∅;
∀ (this : ∀ i ∈ s, Measurable (g i)), 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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) μ
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
have let₄ : let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) sorry 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
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
have let₅ : let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) sorry 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
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
have h : let g : ι → δ → α := fun (i : ι) ↦ if hi : i ∈ s then mk (f i) sorry 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)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have this : Countable.{max 1 (u_6 + 1)} (Subtype p)
Tactic: have : Countable (Subtype p) := hv.countable
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have 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
Tactic: rcases isEmpty_or_nonempty (Subtype p) with hp | hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have 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
Tactic: rcases isEmpty_or_nonempty (Subtype p) with hp | hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have pos : ∀ (H : ∃ (j : Subtype p), s (↑j : ι') = ∅),
  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 = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have neg : ∀ (H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅),
  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 = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 : ι') = ∅
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have 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
Tactic: simp_rw [hv.liminf_eq_ite, if_pos H, measurable_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have pos₁ : Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup univ
Tactic: simp_rw [hv.liminf_eq_ite, if_pos H, measurable_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 : ι') = ∅
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ liminf (fun (x_1 : ι) ↦ f x_1 x) v
have 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
Tactic: simp_rw [hv.liminf_eq_ite, if_neg H]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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 : ι') = ∅
⊢ 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
have this₁ : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
Tactic: have : ∀ i, Countable (s i) := fun i ↦ countable_coe_iff.2 (hs i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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)}
⊢ 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
have m_meas : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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}
have rw : MeasurableSet.{u_4} (α := δ) (⋂ (i : Subtype p), {x : δ | x ∉ m i})
Tactic: rw [setOf_forall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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)
⊢ 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
have mc_meas : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
have 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
Tactic: refine measurable_const.piecewise mc_meas <| .iSup fun j ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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
⊢ 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
have F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
Tactic: have F0_meas : ∀ j, Measurable (F0 j) := fun j ↦ .iInf (fun (i : s j) ↦ hf i)