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 α
ι : 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)
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)}ᶜ
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : ι), f i b

Tactic:
apply Measurable.isLUB_of_mem hf A _ _ this

Premises used: Measurable.isLUB_of_mem
-- 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 α
ι : 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
H : BddAbove.{u_1} (α := α) (range fun (y : ι) ↦ f y b)
⊢ IsLUB.{u_1} (α := α) {a : α | ∃ (i : ι), f i b = a} (⨆ (i : ι), f i b)

Tactic:
apply isLUB_ciSup

Premises used: isLUB_ciSup
-- 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 α
ι : 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
⊢ BddAbove.{u_1} (α := α) (range fun (y : ι) ↦ f y b)

Tactic:
simpa
-- 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 α
ι : 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
hs : ¬BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)
⊢ Eq.{u_1 + 1} (α := α) ((fun (b : δ) ↦ (⨆ (i : ι), f i b : α)) b) ((fun (_b : δ) ↦ (sSup ∅ : α)) b)

Tactic:
apply csSup_of_not_bddAbove

Premises used: csSup_of_not_bddAbove
-- 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 α
ι : 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
⊢ ¬BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)

Tactic:
simpa
-- 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 α
ι : Sort u_5
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ (i : ι), f i b) μ

Tactic:
⟨fun b ↦ ⨆ i, (hf i).mk (f i) b, .iSup (fun i ↦ (hf i).measurable_mk), ?_⟩

Premises used: AEMeasurable, iSup, Measurable.iSup, AEMeasurable.mk, And.intro, Exists.intro, AEMeasurable.measurable_mk
-- 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 α
ι : Sort u_5
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
refine : EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ (i : ι), f i b) fun (b : δ) ↦ ⨆ (i : ι), mk (f i) ⋯ b
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ (i : ι), f i b) μ

Tactic:
refine ⟨fun b ↦ ⨆ i, (hf i).mk (f i) b, .iSup (fun i ↦ (hf i).measurable_mk), ?_⟩
-- 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 α
ι : Sort u_5
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
b : δ
hb : ∀ (i : ι), f i b = mk (f i) ⋯ b
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i b) (⨆ (i : ι), mk (f i) ⋯ b)

Tactic:
simp [hb]
-- 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 α
ι : 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
h₁ h₂ :
  ∀ (b : δ) (hb : ∀ (i : ι), f i b = mk (f i) ⋯ b), Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i b) (⨆ (i : ι), mk (f i) ⋯ b)
⊢ EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ (i : ι), f i b) fun (b : δ) ↦ ⨆ (i : ι), mk (f i) ⋯ b

Tactic:
filter_upwards [ae_all_iff.2 (fun i ↦ (hf i).ae_eq_mk)] with b hb using by simp [hb]

Premises used: Iff.mpr, MeasureTheory.ae_all_iff, AEMeasurable.ae_eq_mk
-- 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 α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨅ (i : ι), f i b

Tactic:
.iSup (α := αᵒᵈ) hf

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

Tactic:
.iSup (α := αᵒᵈ) hf

Premises used: iInf, AEMeasurable.iSup, 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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
simp_rw : Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup (range fun (x_1 : (↑s : Type u_5)) ↦ f (↑x_1 : ι) x)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup ((fun (i : ι) ↦ f i x) '' s)

Tactic:
simp_rw [image_eq_range]

Premises used: Set.image_eq_range
-- 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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Countable.{u_5 + 1} (↑s : Type u_5)

Tactic:
have : Countable s := hs.to_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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Countable.{u_5 + 1} (↑s : Type u_5)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup (range fun (x_1 : (↑s : Type u_5)) ↦ f (↑x_1 : ι) x)

Tactic:
.iSup fun i ↦ hf i i.2

Premises used: iSup, Measurable.iSup, Subtype.val, Subtype.property
-- 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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Countable.{u_5 + 1} (↑s : Type u_5)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sSup (range fun (x_1 : (↑s : Type u_5)) ↦ f (↑x_1 : ι) x)

Tactic:
exact .iSup fun i ↦ hf i i.2
-- 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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦ sInf ((fun (i : ι) ↦ f i x) '' s)

Tactic:
.sSup (α := αᵒᵈ) hs hf

Premises used: Measurable.sSup, 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
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
haveI : ∀ (this : Encodable (↑s : Type u_5)), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b

Tactic:
haveI : Encodable s := hs.toEncodable
-- 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)
this : Encodable (↑s : Type u_5)
pos : ∀ (H : ∀ (i : ι), i ∈ s), Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b
neg : ∀ (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

Tactic:
by_cases H : ∀ i, i ∈ s
-- 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)
this : Encodable (↑s : Type u_5)
H : ∀ (i : ι), i ∈ s
⊢ ∀ (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
-- 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)
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)
pos : Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) b
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b

Tactic:
simp only [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
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 : Type u_5)), f (↑i : ι) b

Tactic:
.iSup (fun (i : s) ↦ hf i i.2)

Premises used: Measurable.iSup, Subtype.val, Subtype.property
-- 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)
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 : Type u_5)), f (↑i : ι) b

Tactic:
exact .iSup (fun (i : s) ↦ hf i i.2)
-- 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)
this : Encodable (↑s : Type u_5)
H : ¬∀ (i : ι), i ∈ s
⊢ ∀ (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
-- 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)
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 ∅))
neg : Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ Max.max (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b) (sSup ∅)
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ ⨆ i ∈ s, f i b

Tactic:
simp only [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
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 ∅))
apply : Measurable.{u_4, u_1} (β := α) fun (a : δ) ↦ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) a
⊢ Measurable.{u_4, u_1} (β := α) fun (b : δ) ↦ Max.max (⨆ (i : (↑s : Type u_5)), f (↑i : ι) b) (sSup ∅)

Tactic:
apply Measurable.sup _ measurable_const

Premises used: Measurable.sup, 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
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 (a : δ) ↦ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) a

Tactic:
.iSup (fun (i : s) ↦ hf i i.2)

Premises used: Measurable.iSup, Subtype.val, Subtype.property
-- 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)
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 (a : δ) ↦ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) a

Tactic:
exact .iSup (fun (i : s) ↦ hf i i.2)
-- 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 ∅
i : ι
hi : i ∈ s
⊢ Measurable (g i)

Tactic:
simpa [g, hi] using (hf i hi).measurable_mk

Premises used: AEMeasurable.measurable_mk
-- 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 ∅
⊢ ∀ 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
-- 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 : ∀ i ∈ s, Measurable (g i)
⊢ AEMeasurable.{u_4, u_1} (β := α) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) μ

Tactic:
⟨fun b ↦ ⨆ (i) (_ : i ∈ s), g i b, .biSup s hs this, ?_⟩

Premises used: Measurable.biSup, AEMeasurable, iSup, And.intro, Exists.intro
-- 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 : ∀ i ∈ s, Measurable (g i)
refine : 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) μ

Tactic:
refine ⟨fun b ↦ ⨆ (i) (_ : i ∈ s), g i b, .biSup s hs 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
μ : 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)
i : ι
hi : i ∈ s
⊢ ∀ᵐ (b : δ) ∂μ, f i b = g i b

Tactic:
simpa [g, hi] using (hf i hi).ae_eq_mk

Premises used: AEMeasurable.ae_eq_mk
-- 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 : ∀ i ∈ s, Measurable (g i)
⊢ ∀ 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
-- 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
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)
⊢ EventuallyEq.{u_4, u_1} (β := α) (ae μ) (fun (b : δ) ↦ ⨆ i ∈ s, f i b) fun (b : δ) ↦ ⨆ i ∈ s, g i b

Tactic:
filter_upwards [(ae_ball_iff hs).2 this] with b hb

Premises used: Iff.mpr, MeasureTheory.ae_ball_iff