awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
rw₂ :
  Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
    (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₃ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) 0) (s.indicator (⇑f : (a : α) → β))
Tactic: rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
rw₂ :
  Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
    (s.indicator (⇑f : (a : α) → β))
rw₃ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) 0) (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₄ : Eq (α := (a : α) → β) (s.indicator (⇑f : (a : α) → β)) (s.indicator (⇑f : (a : α) → β))
Tactic: rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw : Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
  (s.indicator (⇑f : (a : α) → β))
Tactic: classical
  rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
Tactic: classical
  rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₂ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
  (s.indicator (⇑f : (a : α) → β))
Tactic: classical
  rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
rw₂ :
  Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
    (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₃ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) 0) (s.indicator (⇑f : (a : α) → β))
Tactic: classical
  rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
rw₂ :
  Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
    (s.indicator (⇑f : (a : α) → β))
rw₃ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) 0) (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₄ : Eq (α := (a : α) → β) (s.indicator (⇑f : (a : α) → β)) (s.indicator (⇑f : (a : α) → β))
Tactic: classical
  rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
have rw : r ∈ (↑(f.restrict s).range : Set β) ↔ r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
Tactic: rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
have 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
Tactic: rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
have rw₂ : Membership.mem (γ := Set β) (range (s.indicator (⇑f : (a : α) → β))) r ↔
  r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
Tactic: rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
have rw₃ : r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r ↔
  r = 0 ∧ s ≠ univ ∨ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) r
Tactic: rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
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
have hr₁ : Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 0) r
Tactic: rw [restrict_of_not_measurable hs] at hr
Cleared hypotheses: hr, h0, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ 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 : β)
have 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 : β)
Tactic: dsimp only [approx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ 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 : β)
have 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)
Tactic: rw [finset_sup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ 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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ 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
have e_f : ∀ (k : ℕ), (restrict (const α (i k)) {a : α | i k ≤ f a} : (a : α) → β) a = if i k ≤ f a then i k else 0
Tactic: funext k
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 : ℕ
⊢ (restrict (const α (i k)) {a : α | i k ≤ f a} : (a : α) → β) a = if i k ≤ f a then i k else 0
have e_f : indicator {a : α | i k ≤ f a} (⇑(const α (i k)) : (a : α) → β) a = if i k ≤ f a then i k else 0
Tactic: rw [restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ (restrict (const α (i k)) {a : α | i k ≤ f a} : (a : α) → β) a = if i k ≤ f a then i k else 0
have e_f₁ : MeasurableSet.{u_1} (α := α) {a : α | i k ≤ f a}
Tactic: rw [restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ Eq.{u_2 + 1} (α := β) ((approx i (f ∘ g) n : (a : α) → β) a : β) ((approx i f n : (a : γ) → β) (g a) : β)
have 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 : β)
Tactic: rw [approx_apply _ hf, approx_apply _ (hf.comp hg), Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 : β)
⊢ Eq.{u_2 + 1} (α := β) ((approx i (f ∘ g) n : (a : α) → β) a : β) ((approx i f n : (a : γ) → β) (g a) : β)
have 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)
Tactic: rw [approx_apply _ hf, approx_apply _ (hf.comp hg), Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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)
⊢ Eq.{u_2 + 1} (α := β) ((approx i (f ∘ g) n : (a : α) → β) a : β) ((approx i f n : (a : γ) → β) (g a) : β)
have 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)
Tactic: rw [approx_apply _ hf, approx_apply _ (hf.comp hg), Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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)
have refine_1 : ∀ (n : ℕ), LE.le.{u_2} (α := β) ((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 => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 : β)
⊢ Eq.{u_2 + 1} (α := β) (⨆ (n : ℕ), (approx i f n : (a : α) → β) a) (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)
have refine_2 : ∀ (k : ℕ) (hk : i k ≤ f a), i k ≤ ⨆ (n : ℕ), (approx i f n : (a : α) → β) a
Tactic: refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun k => iSup_le fun hk => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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} (α := β) ((approx i f n : (a : α) → β) a : β) (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k : β)
have 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)
Tactic: rw [approx_apply a hf, h_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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)
have refine_1 : ∀ k ∈ Finset.range n, (if i k ≤ f a then i k else ⊥) ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k
Tactic: refine Finset.sup_le fun k _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ (if i k ≤ f a then i k else ⊥) ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k
have pos : ∀ (h : i k ≤ f a), i k ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ (if i k ≤ f a then i k else ⊥) ≤ ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k
have neg : ∀ (h : ¬i k ≤ f a), LE.le.{u_2} (α := β) ⊥ (⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
have refine_2 : i k ≤ (approx i f (k + 1) : (a : α) → β) a
Tactic: refine le_iSup_of_le (k + 1) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 ≤ (approx i f (k + 1) : (a : α) → β) a
have refine_2 : i k ≤ (Finset.range (k + 1)).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0
Tactic: rw [approx_apply a hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
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 ≤ (Finset.range (k + 1)).sup fun (k : ℕ) ↦ if i k ≤ f a then i k else 0
have this : k ∈ Finset.range (k + 1)
Tactic: have : k ∈ Finset.range (k + 1) := Finset.mem_range.2 (Nat.lt_succ_self _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
have refine_2 : i k = if i k ≤ f a then i k else 0
Tactic: refine le_trans (le_of_eq ?_) (Finset.le_sup this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 = if i k ≤ f a then i k else 0
have refine_2 : i k = i k
Tactic: rw [if_pos hk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
q : ℚ
⊢ ennrealRatEmbed (Encodable.encode q) = (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
have rw : ENNReal.ofReal (↑((some q).getD 0) : ℝ) = (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
Tactic: rw [ennrealRatEmbed, Encodable.encodek]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ LT.lt (α := ℝ≥0∞) (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
have simp : LT.lt (α := ℝ≥0∞)
  ((Finset.range n).sup fun (c : ℕ) ↦
    ((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed c ≤ f a} then
            piecewise {a : α | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0
          else 0 :
          α →ₛ ℝ≥0∞) :
        (a : α) → ℝ≥0∞)
      a)
  ∞
Tactic: simp only [eapprox, approx, finset_sup_apply, restrict]