awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
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.insert x s) : Set γ)), motive f
⊢ 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]

Premises used: Finset.coe_empty, Insert.insert, Set.range_subset_singleton, disjoint_iff_inf_le, OfNat.ofNat, Set.diff_eq_empty, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
generalize₁ : ∀ (s : Finset γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
⊢ 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]

Premises used: MeasureTheory.SimpleFunc.coe_range, Finset.coe_singleton, Finset.coe_empty, Finset.coe_sdiff, Finset.coe_inj, Insert.insert, Set.range_subset_singleton, MeasureTheory.SimpleFunc.range, disjoint_iff_inf_le, OfNat.ofNat, Set.diff_eq_empty, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 : α →ₛ γ
let : P f
⊢ P f

Tactic:
let c : γ := Classical.ofNonempty
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
generalize : ∀ (s : Finset γ) (h : f.range \ {c} = s), P f
⊢ P f

Tactic:
generalize h : f.range \ {c} = s

Premises used: MeasureTheory.SimpleFunc.range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
⊢ 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

Premises used: MeasureTheory.SimpleFunc.coe_range, Finset.coe_singleton, Finset.coe_sdiff, Finset.coe_inj
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 γ)
⊢ (⇑f : (a : α) → γ) = Function.const α c

Tactic:
rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h

Premises used: Finset.coe_empty, Set.range_subset_singleton, Set.diff_eq_empty
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 (SimpleFunc.const α c)

Tactic:
const c
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
h₁ : f = SimpleFunc.const α c
⊢ P f

Tactic:
convert! const c
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
h₁ : ∀ (x : α), Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) x : γ) ((SimpleFunc.const α c : (a : α) → γ) x : γ)
⊢ f = SimpleFunc.const α c

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
x : α
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) x : γ) ((SimpleFunc.const α c : (a : α) → γ) x : γ)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 γ)
⊢ MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})

Tactic:
have mx := f.measurableSet_preimage {x}
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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₁ : range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {c} = (↑s : Set γ)
⊢ P g

Tactic:
apply ih
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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₁ :
  (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 γ)
⊢ range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {c} = (↑s : Set γ)

Tactic:
simp only [g, SimpleFunc.coe_piecewise, range_piecewise]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, Set.range_piecewise
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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}
h₂ : x ∉ (↑s : Set γ)
⊢ (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:
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]

Premises used: Iff.mpr, Set.empty_union, Set.diff_diff_comm, Set.insert_diff_self_of_notMem, Set.union_diff_distrib, Finset.coe_insert, Set.diff_eq_empty, Set.image_compl_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
    (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c})
⊢ Subset (α := Set γ)
    (image.{u_5, u_6} (α := α) (⇑(SimpleFunc.const α c) : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {c}

Tactic:
rw [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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}) univ

Tactic:
Set.subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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₁ : Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c}) univ
⊢ Subset.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
    (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c})

Tactic:
convert! Set.subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
⊢ Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c}) univ

Tactic:
preimage_const_of_mem (mem_singleton _)

Premises used: Set.mem_singleton, Classical.ofNonempty, Set.preimage_const_of_mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
⊢ Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑(SimpleFunc.const α c) : (a : α) → γ) {c}) univ

Tactic:
exact preimage_const_of_mem (mem_singleton _)

Premises used: Set.mem_singleton, Set.preimage_const_of_mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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₁ h₂ h₃ h₄ : x ∉ s
⊢ x ∉ (↑s : Set γ)

Tactic:
rwa [Finset.mem_coe]

Premises used: Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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

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]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 (piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x))

Tactic:
pcw mx.compl Pg (const x)

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
h₁ : f = piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x)
⊢ P f

Tactic:
convert! pcw mx.compl Pg (const x)

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
h₁ :
  ∀ (y : α),
    Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
      ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
⊢ f = piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x)

Tactic:
ext1 y
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 : α
pos :
  ∀ (hy : Membership.mem (γ := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) y),
    Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
      ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
neg :
  ∀ (hy : y ∉ preimage (β := γ) (⇑f : (a : α) → γ) {x}),
    Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
      ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)

Tactic:
by_cases hy : y ∈ f ⁻¹' {x}
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 : α
hy : Membership.mem (γ := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) y
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)

Tactic:
simpa [g, hy]