awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ ∀ (y : ℝ≥0∞),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
        (∞ : ℝ≥0∞)
have rw : f.FinMeasSupp μ
Tactic: rw [← finMeasSupp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
⊢ motive f
have generalize : ∀ (s : Finset γ) (h : f.range \ {0} = s), motive f
Tactic: generalize h : f.range \ {0} = s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
s : Finset γ
h : f.range \ {0} = s
⊢ motive f
have h₁ : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)
Tactic: rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑∅ : Set γ)
⊢ motive f
have h₁ : Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)
Tactic: rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)
⊢ motive f
have h₁ : f = piecewise univ sorry (SimpleFunc.const α 0) (SimpleFunc.const α 0)
Tactic: convert! const 0 MeasurableSet.univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)
⊢ f = piecewise univ ⋯ (SimpleFunc.const α 0) (SimpleFunc.const α 0)
have h₁ : ∀ (x : α),
  Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) x : γ)
    ((piecewise univ sorry (SimpleFunc.const α 0) (SimpleFunc.const α 0) : (a : α) → γ) x : γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
⊢ motive f
have insert : ∀ (mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})), motive f
Tactic: have mx := f.measurableSet_preimage {x}
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
⊢ motive g
have h₁ : range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {0} = (↑s : Set γ)
Tactic: apply ih
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
⊢ range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {0} = (↑s : Set γ)
have h₁ : (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) ∪
      image.{u_5, u_6} (α := α) (⇑f : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ) \
    {0} =
  (↑s : Set γ)
Tactic: simp only [g, SimpleFunc.coe_piecewise, range_piecewise]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
⊢ (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) ∪
        image.{u_5, u_6} (α := α) (⇑f : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ) \
      {0} =
    (↑s : Set γ)
have h₁ : Subset (α := Set γ) (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {0}
Tactic: rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert,
        insert_diff_self_of_notMem, diff_eq_empty.mpr, Set.empty_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
h₁ : Subset (α := Set γ) (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {0}
⊢ (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) ∪
        image.{u_5, u_6} (α := α) (⇑f : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ) \
      {0} =
    (↑s : Set γ)
have h₂ : x ∉ (↑s : Set γ)
Tactic: rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert,
        insert_diff_self_of_notMem, diff_eq_empty.mpr, Set.empty_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
⊢ Subset (α := Set γ) (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {0}
have h₁ : Subset.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) (preimage (β := γ) (⇑0 : (a : α) → γ) {0})
Tactic: rw [Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
⊢ Subset.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) (preimage (β := γ) (⇑0 : (a : α) → γ) {0})
have h₁ : Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑0 : (a : α) → γ) {0}) univ
Tactic: convert! Set.subset_univ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
⊢ motive f
have Pg : motive g
Tactic: have Pg : motive g := by
      apply ih
      simp only [g, SimpleFunc.coe_piecewise, range_piecewise]
      rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert,
        insert_diff_self_of_notMem, diff_eq_empty.mpr, Set.empty_union]
      · rw [Set.image_subset_iff]
        convert! Set.subset_univ _
        exact preimage_const_of_mem (mem_singleton _)
      · rwa [Finset.mem_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
⊢ motive f
have h₁ : f = g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)
Tactic: convert! add _ Pg (const x mx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
h₁ : f = g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)
⊢ motive f
have insert : Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ))
  (support.{u_5, u_6} (M := γ)
    (⇑(piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) :
      (a : α) → γ))
Tactic: convert! add _ Pg (const x mx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
⊢ f = g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)
have h₁ : ∀ (y : α),
  Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0) :
          (a : α) → γ)
        y :
      γ)
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
y : α
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0) :
          (a : α) → γ)
        y :
      γ)
have pos : ∀ (hy : Membership.mem (γ := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) y),
  Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0) :
          (a : α) → γ)
        y :
      γ)
Tactic: by_cases hy : y ∈ f ⁻¹' {x}
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
y : α
pos :
  ∀ (hy : Membership.mem (γ := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) y),
    Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
      ((g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0) :
            (a : α) → γ)
          y :
        γ)
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0) :
          (a : α) → γ)
        y :
      γ)
have neg : ∀ (hy : y ∉ preimage (β := γ) (⇑f : (a : α) → γ) {x}),
  Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0) :
          (a : α) → γ)
        y :
      γ)
Tactic: by_cases hy : y ∈ f ⁻¹' {x}
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
⊢ Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ))
    (support.{u_5, u_6} (M := γ)
      (⇑(piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) :
        (a : α) → γ))
have insert : LE.le.{u_5} (α := Set α)
  (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ) ⊓
    support.{u_5, u_6} (M := γ)
      (⇑(piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) :
        (a : α) → γ))
  ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
y : α
⊢ Membership.mem (γ := Set α)
      (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ) ⊓
        support.{u_5, u_6} (M := γ)
          (⇑(piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) :
            (a : α) → γ))
      y →
    Membership.mem (γ := Set α) ⊥ y
have pos : ∀ (hy : Membership.mem (γ := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) y),
  Membership.mem (γ := Set α)
      (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ) ⊓
        support.{u_5, u_6} (M := γ)
          (⇑(piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) :
            (a : α) → γ))
      y →
    Membership.mem (γ := Set α) ⊥ y
Tactic: by_cases hy : y ∈ f ⁻¹' {x}