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)
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}
h₂ : x ∉ (↑s : Set γ)
⊢ (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:
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 : 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.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) (preimage (β := γ) (⇑0 : (a : α) → γ) {0})
⊢ Subset (α := Set γ) (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})) {0}

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 : 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}) 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 : 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₁ : Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑0 : (a : α) → γ) {0}) univ
⊢ Subset.{u_5} (α := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) (preimage (β := γ) (⇑0 : (a : α) → γ) {0})

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 : 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
⊢ Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑0 : (a : α) → γ) {0}) univ

Tactic:
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 : 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
⊢ Eq.{u_5 + 1} (α := Set α) (preimage (β := γ) (⇑0 : (a : α) → γ) {0}) 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 : 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₁ 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 : 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

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]
-- 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)
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 (g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0))

Tactic:
add _ Pg (const x mx)
-- 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)
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 γ)
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)
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 : α) → γ))
⊢ motive f

Tactic:
convert! add _ Pg (const x mx)
-- 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)
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₁ :
  ∀ (y : α),
    Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
      ((g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0) :
            (a : α) → γ)
          y :
        γ)
⊢ f = g + piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)

Tactic:
ext1 y
-- 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)
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 :
        γ)
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 :
        γ)
⊢ 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}
-- 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)
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 : α
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:
simpa [g, hy]
-- 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)
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 : α
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:
simp [g, hy]
-- 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)
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 γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
Pg : motive g
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 : α) → γ))
    ⊥
⊢ 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:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- 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)
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
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
⊢ 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}
-- 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)
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 : α
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:
simp [g, hy]
-- 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)
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 : α
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:
simp [g, hy]