awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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),
    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
⊢ 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 neg : ∀ (hy : y ∉ preimage (β := γ) (⇑f : (a : α) → γ) {x}),
  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}
-- 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 : α →ₛ γ
s : Finset γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)
⊢ motive f
have empty : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑∅ : Set γ)), motive f
Tactic: induction s using Finset.induction generalizing f with
  | empty =>
    rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
    convert! const 0 MeasurableSet.univ
    ext x
    simp [h]
  | insert x s hxs ih =>
    have mx := f.measurableSet_preimage {x}
    let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx 0 f
    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]
    convert! add _ Pg (const x mx)
    · ext1 y
      by_cases hy : y ∈ f ⁻¹' {x}
      · simpa [g, hy]
      · simp [g, hy]
    rw [disjoint_iff_inf_le]
    rintro y
    by_cases hy : y ∈ f ⁻¹' {x} <;> simp [g, hy]
Cleared hypotheses: f, s, 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 : α →ₛ γ
s : Finset γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)
empty : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑∅ : Set γ)), motive f
⊢ motive f
have insert : ∀ (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
Tactic: induction s using Finset.induction generalizing f with
  | empty =>
    rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
    convert! const 0 MeasurableSet.univ
    ext x
    simp [h]
  | insert x s hxs ih =>
    have mx := f.measurableSet_preimage {x}
    let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx 0 f
    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]
    convert! add _ Pg (const x mx)
    · ext1 y
      by_cases hy : y ∈ f ⁻¹' {x}
      · simpa [g, hy]
      · simp [g, hy]
    rw [disjoint_iff_inf_le]
    rintro y
    by_cases hy : y ∈ f ⁻¹' {x} <;> simp [g, hy]
Cleared hypotheses: f, s, 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 : α →ₛ γ
⊢ motive f
have generalize : ∀ (s : Finset γ) (h : f.range \ {0} = s), motive f
Tactic: classical
  generalize h : f.range \ {0} = s
  rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h
  induction s using Finset.induction generalizing f with
  | empty =>
    rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
    convert! const 0 MeasurableSet.univ
    ext x
    simp [h]
  | insert x s hxs ih =>
    have mx := f.measurableSet_preimage {x}
    let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx 0 f
    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]
    convert! add _ Pg (const x mx)
    · ext1 y
      by_cases hy : y ∈ f ⁻¹' {x}
      · simpa [g, hy]
      · simp [g, hy]
    rw [disjoint_iff_inf_le]
    rintro y
    by_cases hy : y ∈ f ⁻¹' {x} <;> simp [g, hy]
-- 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 : α →ₛ γ
generalize : ∀ (s : Finset γ) (h : f.range \ {0} = s), motive f
⊢ motive f
have generalize₁ : ∀ (s : Finset γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
Tactic: classical
  generalize h : f.range \ {0} = s
  rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h
  induction s using Finset.induction generalizing f with
  | empty =>
    rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
    convert! const 0 MeasurableSet.univ
    ext x
    simp [h]
  | insert x s hxs ih =>
    have mx := f.measurableSet_preimage {x}
    let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx 0 f
    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]
    convert! add _ Pg (const x mx)
    · ext1 y
      by_cases hy : y ∈ f ⁻¹' {x}
      · simpa [g, hy]
      · simp [g, hy]
    rw [disjoint_iff_inf_le]
    rintro y
    by_cases hy : y ∈ f ⁻¹' {x} <;> simp [g, hy]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
f : α →ₛ γ
c : γ := Classical.ofNonempty
⊢ P f
have generalize : ∀ (s : Finset γ) (h : f.range \ {c} = s), P f
Tactic: generalize h : f.range \ {c} = s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
f : α →ₛ γ
c : γ := Classical.ofNonempty
s : Finset γ
h : f.range \ {c} = s
⊢ P f
have h₁ : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑∅ : Set γ)
⊢ P f
have h₁ : (⇑f : (a : α) → γ) = Function.const α c
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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
f : α →ₛ γ
h : (⇑f : (a : α) → γ) = Function.const α c
⊢ P f
have h₁ : f = SimpleFunc.const α c
Tactic: convert! const c
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
f : α →ₛ γ
h : (⇑f : (a : α) → γ) = Function.const α c
⊢ f = SimpleFunc.const α c
have h₁ : ∀ (x : α), Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) x : γ) ((SimpleFunc.const α c : (a : α) → γ) x : γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
⊢ P f
have mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
⊢ P g
have h₁ : range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {c} = (↑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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
⊢ range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {c} = (↑s : Set γ)
have h₁ : (image.{u_5, u_6} (α := α) (⇑(SimpleFunc.const α c) : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) ∪
      image.{u_5, u_6} (α := α) (⇑f : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ) \
    {c} =
  (↑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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
⊢ (image.{u_5, u_6} (α := α) (⇑(SimpleFunc.const α c) : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) ∪
        image.{u_5, u_6} (α := α) (⇑f : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ) \
      {c} =
    (↑s : Set γ)
have h₁ : Subset (α := Set γ)
  (image.{u_5, u_6} (α := α) (⇑(SimpleFunc.const α c) : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {c}
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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
h₁ :
  Subset (α := Set γ)
    (image.{u_5, u_6} (α := α) (⇑(SimpleFunc.const α c) : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {c}
⊢ (image.{u_5, u_6} (α := α) (⇑(SimpleFunc.const α c) : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) ∪
        image.{u_5, u_6} (α := α) (⇑f : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ) \
      {c} =
    (↑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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
⊢ Subset (α := Set γ)
    (image.{u_5, u_6} (α := α) (⇑(SimpleFunc.const α c) : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {c}
have h₁ : Subset.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
  (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c})
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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
⊢ Subset.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
    (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c})
have h₁ : Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c}) 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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
⊢ P f
have Pg : P g
Tactic: have Pg : P 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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
Pg : P g
⊢ P f
have h₁ : f = piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ sorry g (SimpleFunc.const α x)
Tactic: convert! pcw mx.compl Pg (const x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
Pg : P g
⊢ f = piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x)
have h₁ : ∀ (y : α),
  Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ sorry g (SimpleFunc.const α x) : (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 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
have pos : ∀ (hy : Membership.mem (γ := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) y),
  Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ sorry g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
Tactic: by_cases hy : y ∈ f ⁻¹' {x}