awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : Zero β
inst_2 : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
x : α
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := γ) ((map g (f.restrict s) : (a : α) → γ) x : γ) (((map g f).restrict s : (a : α) → γ) x : γ)

Tactic:
simp [hs, Set.indicator_comp_of_zero hg]

Premises used: Set.indicator_comp_of_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : Zero β
inst_2 : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
x : α
hs : ¬MeasurableSet s
⊢ Eq.{u_3 + 1} (α := γ) ((map g (f.restrict s) : (a : α) → γ) x : γ) (((map g f).restrict s : (a : α) → γ) x : γ)

Tactic:
simp [restrict_of_not_measurable hs, hg]

Premises used: MeasureTheory.SimpleFunc.restrict_of_not_measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ≥0
s : Set α
⊢ map ofNNReal (f.restrict s) = (map ofNNReal f).restrict s

Tactic:
map_restrict_of_zero ENNReal.coe_zero _ _

Premises used: MeasureTheory.SimpleFunc.map_restrict_of_zero, ENNReal.coe_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ≥0
s : Set α
⊢ map toReal (f.restrict s) = (map toReal f).restrict s

Tactic:
map_restrict_of_zero NNReal.coe_zero _ _

Premises used: NNReal.coe_zero, MeasureTheory.SimpleFunc.map_restrict_of_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f.restrict s : (a : α) → β) a : β) (s.indicator (⇑f : (a : α) → β) a : β)

Tactic:
simp only [f.coe_restrict hs]

Premises used: MeasureTheory.SimpleFunc.coe_restrict
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ (⇑(f.restrict s) : (a : α) → β) ⁻¹' t = s ∩ (⇑f : (a : α) → β) ⁻¹' t

Tactic:
simp [hs, indicator_preimage_of_notMem _ _ ht, inter_comm]

Premises used: Set.inter_comm, Set.indicator_preimage_of_notMem
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
r : β
hr : r ≠ 0
⊢ preimage (β := β) (⇑(f.restrict s) : (a : α) → β) {r} = s ∩ preimage (β := β) (⇑f : (a : α) → β) {r}

Tactic:
f.restrict_preimage hs hr.symm

Premises used: Ne.symm, MeasureTheory.SimpleFunc.restrict_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
rw : r ∈ (↑(f.restrict s).range : Set β) ↔ r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
rw₁ :
  Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑(f.restrict s) : (a : α) → β)) r ↔
    r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
rw₂ :
  Membership.mem (γ := Set β) (range (s.indicator (⇑f : (a : α) → β))) r ↔
    r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
rw₃ rw₄ :
  r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r ↔
    r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r

Tactic:
rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]

Premises used: MeasureTheory.SimpleFunc.coe_range, Set.mem_range_indicator, MeasureTheory.SimpleFunc.coe_restrict, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : MeasurableSet s
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r

Tactic:
simpa [mem_restrict_range hs, h0, -mem_range] using hr

Premises used: MeasureTheory.SimpleFunc.mem_range, MeasureTheory.SimpleFunc.mem_restrict_range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 0) r

Tactic:
rw [restrict_of_not_measurable hs] at hr

Premises used: MeasureTheory.SimpleFunc.restrict_of_not_measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : ¬MeasurableSet s
hr₁ : Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 0) r
⊢ r ≠ 0

Tactic:
rw [restrict_of_not_measurable hs] at hr

Premises used: MeasureTheory.SimpleFunc.restrict_of_not_measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : ¬MeasurableSet s
hr₁ : Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 0) r
h0₁ : r ≠ 0
⊢ ¬MeasurableSet s

Tactic:
rw [restrict_of_not_measurable hs] at hr

Premises used: MeasureTheory.SimpleFunc.restrict_of_not_measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hr : Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 0) r
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r

Tactic:
(h0 <| eq_zero_of_mem_range_zero hr).elim

Premises used: False.elim, MeasureTheory.SimpleFunc.eq_zero_of_mem_range_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hr : Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 0) r
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r

Tactic:
exact (h0 <| eq_zero_of_mem_range_zero hr).elim

Premises used: False.elim, MeasureTheory.SimpleFunc.eq_zero_of_mem_range_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
inst_2 : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : MeasurableSet s
x : α
⊢ LE.le.{u_2} (α := β) ((f.restrict s : (a : α) → β) x : β) ((g.restrict s : (a : α) → β) x : β)

Tactic:
simp only [coe_restrict _ hs, indicator_le_indicator (H x)]

Premises used: MeasureTheory.SimpleFunc.coe_restrict, Set.indicator_le_indicator
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
inst_2 : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : ¬MeasurableSet s
⊢ f.restrict s ≤ g.restrict s

Tactic:
simp only [restrict_of_not_measurable hs, le_refl]

Premises used: le_refl, MeasureTheory.SimpleFunc.restrict_of_not_measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
dsimp :
  Eq.{u_2 + 1} (α := β)
    (((Finset.range n).sup fun (k : ℕ) ↦ restrict (const α (i k)) {a : α | i k ≤ f a} : (a : α) → β) a : β)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0 : β)
⊢ Eq.{u_2 + 1} (α := β) ((approx i f n : (a : α) → β) a : β)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0 : β)

Tactic:
dsimp only [approx]

Premises used: MeasureTheory.SimpleFunc.approx
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
rw :
  Eq.{u_2 + 1} (α := β)
    ((Finset.range n).sup fun (c : ℕ) ↦ (restrict (const α (i c)) {a : α | i c ≤ f a} : (a : α) → β) a)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0)
⊢ Eq.{u_2 + 1} (α := β)
    (((Finset.range n).sup fun (k : ℕ) ↦ restrict (const α (i k)) {a : α | i k ≤ f a} : (a : α) → β) a : β)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0 : β)

Tactic:
rw [finset_sup_apply]

Premises used: MeasureTheory.SimpleFunc.finset_sup_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
e_f :
  Eq.{u_2 + 1} (α := ℕ → β) (fun (c : ℕ) ↦ (restrict (const α (i c)) {a : α | i c ≤ f a} : (a : α) → β) a) fun (k : ℕ) ↦
    if i k ≤ f a then i k else 0
⊢ Eq.{u_2 + 1} (α := β)
    ((Finset.range n).sup fun (c : ℕ) ↦ (restrict (const α (i c)) {a : α | i c ≤ f a} : (a : α) → β) a)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
e_f : ∀ (k : ℕ), (restrict (const α (i k)) {a : α | i k ≤ f a} : (a : α) → β) a = if i k ≤ f a then i k else 0
⊢ Eq.{u_2 + 1} (α := ℕ → β) (fun (c : ℕ) ↦ (restrict (const α (i c)) {a : α | i c ≤ f a} : (a : α) → β) a) fun (k : ℕ) ↦
    if i k ≤ f a then i k else 0

Tactic:
funext k
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
e_f : indicator {a : α | i k ≤ f a} (⇑(const α (i k)) : (a : α) → β) a = if i k ≤ f a then i k else 0
e_f₁ : MeasurableSet.{u_1} (α := α) {a : α | i k ≤ f a}
⊢ (restrict (const α (i k)) {a : α | i k ≤ f a} : (a : α) → β) a = if i k ≤ f a then i k else 0

Tactic:
rw [restrict_apply]

Premises used: MeasureTheory.SimpleFunc.restrict_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ indicator {a : α | i k ≤ f a} (⇑(const α (i k)) : (a : α) → β) a = if i k ≤ f a then i k else 0

Tactic:
simp only [coe_const, mem_setOf_eq, indicator_apply, Function.const_apply]

Premises used: Function.const_apply, Set.indicator_apply, Set.mem_setOf_eq, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet.{u_1} (α := α) {a : α | i k ≤ f a}

Tactic:
hf measurableSet_Ici

Premises used: Set.Mem, setOf, Set.preimage, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet.{u_1} (α := α) {a : α | i k ≤ f a}

Tactic:
exact hf measurableSet_Ici

Premises used: measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
i : ℕ → β
f : α → β
⊢ Monotone (β := α →ₛ β) (approx i f)

Tactic:
fun _ _ h =>
  Finset.sup_mono <| Finset.range_subset_range.2 h

Premises used: Iff.mpr, Monotone, Finset.range_subset_range, Finset.sup_mono
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
inst_3 : Zero β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
inst_6 : MeasurableSpace β
inst_7 : OpensMeasurableSpace β
inst_8 : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
rw :
  Eq.{u_2 + 1} (α := β) ((approx i (f ∘ g) n : (a : α) → β) a : β)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f (g a) then i k else 0 : β)
rw₁ :
  Eq.{u_2 + 1} (α := β) ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ (f ∘ g) a then i k else 0)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f (g a) then i k else 0)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := β) ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f (g a) then i k else 0)
    ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f (g a) then i k else 0)
⊢ Eq.{u_2 + 1} (α := β) ((approx i (f ∘ g) n : (a : α) → β) a : β) ((approx i f n : (a : γ) → β) (g a) : β)

Tactic:
rw [approx_apply _ hf, approx_apply _ (hf.comp hg), Function.comp_apply]

Premises used: Measurable.comp, Function.comp_apply, MeasureTheory.SimpleFunc.approx_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
⊢ Eq.{u_2 + 1} (α := β) (⨆ (n : ℕ), (approx i f n : (a : α) → β) a) (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)

Tactic:
le_antisymm (iSup_le fun n => ?_) (iSup_le fun k => iSup_le fun hk => ?_)

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
refine_1 : ∀ (n : ℕ), LE.le.{u_2} (α := β) ((approx i f n : (a : α) → β) a : β) (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k : β)
refine_2 : ∀ (k : ℕ) (hk : i k ≤ f a), i k ≤ ⨆ (n : ℕ), (approx i f n : (a : α) → β) a
⊢ Eq.{u_2 + 1} (α := β) (⨆ (n : ℕ), (approx i f n : (a : α) → β) a) (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)

Tactic:
refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun k => iSup_le fun hk => ?_)

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n : ℕ
refine_1 :
  LE.le.{u_2} (α := β) ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else ⊥)
    (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)
⊢ LE.le.{u_2} (α := β) ((approx i f n : (a : α) → β) a : β) (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k : β)

Tactic:
rw [approx_apply a hf, h_zero]

Premises used: MeasureTheory.SimpleFunc.approx_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n : ℕ
⊢ LE.le.{u_2} (α := β) ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else ⊥)
    (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)

Tactic:
Finset.sup_le fun k _ => ?_

Premises used: Finset.sup_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n : ℕ
refine_1 : ∀ k ∈ Finset.range n, (if i k ≤ f a then i k else ⊥) ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k
⊢ LE.le.{u_2} (α := β) ((Finset.range n).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else ⊥)
    (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)

Tactic:
refine Finset.sup_le fun k _ => ?_

Premises used: Finset.sup_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n k : ℕ
h : k ∈ Finset.range n
pos : ∀ (h : i k ≤ f a), i k ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k
neg : ∀ (h : ¬i k ≤ f a), LE.le.{u_2} (α := β) ⊥ (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)
⊢ (if i k ≤ f a then i k else ⊥) ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n k : ℕ
h_1 : k ∈ Finset.range n
h : i k ≤ f a
⊢ i k ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k

Tactic:
le_iSup_of_le k (le_iSup (fun _ : i k ≤ f a => i k) h)

Premises used: le_iSup, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n k : ℕ
h_1 : k ∈ Finset.range n
h : i k ≤ f a
⊢ i k ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k

Tactic:
exact le_iSup_of_le k (le_iSup (fun _ : i k ≤ f a => i k) h)

Premises used: le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n k : ℕ
h_1 : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ LE.le.{u_2} (α := β) ⊥ (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
n k : ℕ
h_1 : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ LE.le.{u_2} (α := β) ⊥ (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ ⨆ (n : ℕ), (approx i f n : (a : α) → β) a

Tactic:
le_iSup_of_le (k + 1) ?_

Premises used: HAdd.hAdd, le_iSup_of_le, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
k : ℕ
hk : i k ≤ f a
refine_2 : i k ≤ (approx i f (k + 1) : (a : α) → β) a
⊢ i k ≤ ⨆ (n : ℕ), (approx i f n : (a : α) → β) a

Tactic:
refine le_iSup_of_le (k + 1) ?_

Premises used: HAdd.hAdd, le_iSup_of_le, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
k : ℕ
hk : i k ≤ f a
refine_2 : i k ≤ (Finset.range (k + 1)).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0
⊢ i k ≤ (approx i f (k + 1) : (a : α) → β) a

Tactic:
rw [approx_apply a hf]

Premises used: MeasureTheory.SimpleFunc.approx_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
k : ℕ
hk : i k ≤ f a
⊢ k ∈ Finset.range (k + 1)

Tactic:
have : k ∈ Finset.range (k + 1) := Finset.mem_range.2 (Nat.lt_succ_self _)
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
k : ℕ
hk : i k ≤ f a
this : k ∈ Finset.range (k + 1)
⊢ i k ≤ (Finset.range (k + 1)).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0

Tactic:
le_trans (le_of_eq ?_) (Finset.le_sup this)

Premises used: le_of_eq, Finset.le_sup, le_trans
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
k : ℕ
hk : i k ≤ f a
this : k ∈ Finset.range (k + 1)
refine_2 : i k = if i k ≤ f a then i k else 0
⊢ i k ≤ (Finset.range (k + 1)).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0

Tactic:
refine le_trans (le_of_eq ?_) (Finset.le_sup this)

Premises used: le_of_eq, Finset.le_sup, le_trans
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : CompleteLattice β
inst_3 : OrderClosedTopology β
inst_4 : Zero β
inst_5 : MeasurableSpace β
inst_6 : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : Eq.{u_2 + 1} (α := β) 0 ⊥
k : ℕ
hk : i k ≤ f a
this : k ∈ Finset.range (k + 1)
refine_2 refine_2₁ : i k = i k
⊢ i k = if i k ≤ f a then i k else 0

Tactic:
rw [if_pos hk]

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
q : ℚ
rw : ENNReal.ofReal (↑((some q).getD 0) : ℝ) = (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
⊢ ennrealRatEmbed (Encodable.encode q) = (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)

Tactic:
rw [ennrealRatEmbed, Encodable.encodek]

Premises used: Encodable.encodek, MeasureTheory.SimpleFunc.ennrealRatEmbed
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
q : ℚ
⊢ ENNReal.ofReal (↑((some q).getD 0) : ℝ) = (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)

Tactic:
rfl