awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
have neg : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sSup ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨆ (_ : p), f b
have simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
Tactic: classical
  simp_rw [ciSup_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨆ (_ : p), f b
have pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
Tactic: classical
  simp_rw [ciSup_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨆ (_ : p), f b
have neg : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sSup ∅
Tactic: classical
  simp_rw [ciSup_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨅ (_ : p), f b
have simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
Tactic: simp_rw [ciInf_eq_ite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
have pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
have neg : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sInf ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨅ (_ : p), f b
have simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
Tactic: classical
  simp_rw [ciInf_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨅ (_ : p), f b
have pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
Tactic: classical
  simp_rw [ciInf_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sInf ∅
pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨅ (_ : p), f b
have neg : ∀ (h : ¬p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ sInf ∅
Tactic: classical
  simp_rw [ciInf_eq_ite]
  split_ifs with h
  · exact hf
  · exact 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
have inl : ∀ (hι : IsEmpty ι), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
inl : ∀ (hι : IsEmpty ι), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
have inr : ∀ (hι : Nonempty ι), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
Tactic: rcases isEmpty_or_nonempty ι with hι | 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
have A : MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
Tactic: have A : MeasurableSet {b | BddAbove (range (fun i ↦ f i b))} :=
    measurableSet_bddAbove_range hf
-- 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
have this : Measurable.{u_4, u_1} (β := α) fun (_b : δ) ↦ sSup ∅
Tactic: have : Measurable (fun (_b : δ) ↦ sSup (∅ : Set α)) := 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
this : Measurable.{u_4, u_1} (β := α) fun (_b : δ) ↦ sSup ∅
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
have apply : ∀ (b : δ),
  Membership.mem (γ := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)} b →
    IsLUB.{u_1} (α := α) {a : α | ∃ (i : ι), f i b = a} (⨆ (i : ι), f i b)
Tactic: apply Measurable.isLUB_of_mem hf A _ _ this
-- 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
this : Measurable.{u_4, u_1} (β := α) fun (_b : δ) ↦ sSup ∅
apply :
  ∀ (b : δ),
    Membership.mem (γ := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)} b →
      IsLUB.{u_1} (α := α) {a : α | ∃ (i : ι), f i b = a} (⨆ (i : ι), f i b)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b
have apply₁ : EqOn.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ (i : ι), f i b) (fun (_b : δ) ↦ sSup ∅)
  {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}ᶜ
Tactic: apply Measurable.isLUB_of_mem hf A _ _ this
-- 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
this : Measurable.{u_4, u_1} (β := α) fun (_b : δ) ↦ sSup ∅
b : δ
hb : Membership.mem (γ := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)} b
⊢ IsLUB.{u_1} (α := α) {a : α | ∃ (i : ι), f i b = a} (⨆ (i : ι), f i b)
have H : BddAbove.{u_1} (α := α) (range fun (y : ι) ↦ f y b)
Tactic: apply isLUB_ciSup
-- 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
this : Measurable.{u_4, u_1} (β := α) fun (_b : δ) ↦ sSup ∅
b : δ
hb : Membership.mem (γ := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}ᶜ b
⊢ Eq.{u_1 + 1} (α := α) ((fun (b : δ) ↦ (⨆ (i : ι), f i b : α)) b) ((fun (_b : δ) ↦ (sSup ∅ : α)) b)
have hs : ¬BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)
Tactic: apply csSup_of_not_bddAbove
-- 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 α
ι : Sort u_5
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ (i : ι), f i b) μ
have refine : EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ (i : ι), f i b) fun (b : δ) ↦ ⨆ (i : ι), mk (f i) sorry b
Tactic: refine ⟨fun b ↦ ⨆ i, (hf i).mk (f i) b, .iSup (fun i ↦ (hf i).measurable_mk), ?_⟩
-- 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 α
ι : Sort u_5
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ (i : ι), f i b) fun (b : δ) ↦ ⨆ (i : ι), mk (f i) ⋯ b
have h : ∀ (a : δ),
  Membership.mem (γ := Set δ)
    {x : δ |
      Membership.mem (γ := Set δ) {x : δ | (fun (a : δ) ↦ ∀ (i : ι), f i a = mk (f i) sorry a) x} x →
        Membership.mem (γ := Set δ)
          {x : δ |
            (fun (x : δ) ↦
                Eq.{u_1 + 1} (α := α) ((fun (b : δ) ↦ (⨆ (i : ι), f i b : α)) x)
                  ((fun (b : δ) ↦ (⨆ (i : ι), mk (f i) sorry b : α)) x))
              x}
          x}
    a
Tactic: filter_upwards [ae_all_iff.2 (fun i ↦ (hf i).ae_eq_mk)] with b hb using by simp [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 α
ι : Sort u_5
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (a : δ),
    Membership.mem (γ := Set δ)
      {x : δ |
        Membership.mem (γ := Set δ) {x : δ | (fun (a : δ) ↦ ∀ (i : ι), f i a = mk (f i) ⋯ a) x} x →
          Membership.mem (γ := Set δ)
            {x : δ |
              (fun (x : δ) ↦
                  Eq.{u_1 + 1} (α := α) ((fun (b : δ) ↦ (⨆ (i : ι), f i b : α)) x)
                    ((fun (b : δ) ↦ (⨆ (i : ι), mk (f i) ⋯ b : α)) x))
                x}
            x}
      a
⊢ EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ (i : ι), f i b) fun (b : δ) ↦ ⨆ (i : ι), mk (f i) ⋯ b
have h₁ : ∀ (a : δ), (∀ (i : ι), f i a = mk (f i) sorry a) → Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i a) (⨆ (i : ι), mk (f i) sorry a)
Tactic: filter_upwards [ae_all_iff.2 (fun i ↦ (hf i).ae_eq_mk)] with b hb using by simp [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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup ((fun (i : ι) ↦ f i x) '' s)
have simp_rw : Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup (range fun (x_1 : (↑s : Type u_5)) ↦ f (↑x_1 : ι) x)
Tactic: simp_rw [image_eq_range]
-- 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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup (range fun (x_1 : (↑s : Type u_5)) ↦ f (↑x_1 : ι) x)
have this : Countable.{u_5 + 1} (↑s : Type u_5)
Tactic: have : Countable s := hs.to_subtype
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
have haveI : ∀ (this : Encodable (↑s : Type u_5)), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
Tactic: haveI : Encodable s := hs.toEncodable
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable (↑s : Type u_5)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
have pos : ∀ (H : ∀ (i : ι), i ∈ s), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
Tactic: by_cases H : ∀ i, i ∈ s
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable (↑s : Type u_5)
pos : ∀ (H : ∀ (i : ι), i ∈ s), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
have neg : ∀ (H : ¬∀ (i : ι), i ∈ s), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
Tactic: by_cases H : ∀ i, i ∈ s
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable (↑s : Type u_5)
H : ∀ (i : ι), i ∈ s
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
have this₁ : ∀ (b : δ), Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b)
Tactic: have : ∀ b, ⨆ i ∈ s, f i b = ⨆ (i : s), f i b :=
      fun b ↦ cbiSup_eq_of_forall (f := fun i ↦ f i b) H
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this_1 : Encodable (↑s : Type u_5)
H : ∀ (i : ι), i ∈ s
this : ∀ (b : δ), Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
have pos : Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) b
Tactic: simp only [this]
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable (↑s : Type u_5)
H : ¬∀ (i : ι), i ∈ s
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
have this₁ : ∀ (b : δ), Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (Max.max (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b) (sSup ∅))
Tactic: have : ∀ b, ⨆ i ∈ s, f i b = (⨆ (i : s), f i b) ⊔ sSup ∅ :=
      fun b ↦ cbiSup_eq_of_not_forall (f := fun i ↦ f i b) H
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this_1 : Encodable (↑s : Type u_5)
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (Max.max (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b) (sSup ∅))
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
have neg : Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ Max.max (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b) (sSup ∅)
Tactic: simp only [this]
-- 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this_1 : Encodable (↑s : Type u_5)
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), Eq.{u_1 + 1} (α := α) (⨆ i ∈ s, f i b) (Max.max (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b) (sSup ∅))
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ Max.max (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b) (sSup ∅)
have apply : Measurable.{u_4, u_1} (β := α) fun (a : δ) ↦ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) a
Tactic: apply Measurable.sup _ measurable_const
-- 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
μ : 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 ∅
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
have this : ∀ i ∈ s, Measurable (g i)
Tactic: have : ∀ i ∈ s, Measurable (g i) := by
    intro i hi
    simpa [g, hi] using (hf i hi).measurable_mk
-- 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 : ∀ i ∈ s, Measurable (g i)
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ
have refine : EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) fun (b : δ) ↦ ⨆ i ∈ s, g i b
Tactic: refine ⟨fun b ↦ ⨆ (i) (_ : i ∈ s), g i b, .biSup s hs this, ?_⟩
-- 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
μ : 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 : ∀ 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
have this₁ : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b
Tactic: have : ∀ i ∈ s, ∀ᵐ b ∂μ, f i b = g i b :=
    fun i hi ↦ by simpa [g, hi] using (hf i hi).ae_eq_mk