awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
x : β
⊢ MeasurableSet.{u_1} (α := α) (preimage (β := β) (⇑f : (a : α) → β) {x})

Tactic:
f.measurableSet_fiber' x

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber'
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α → β
h : ∀ (x : β), MeasurableSet (f ⁻¹' {x})
h' : (range f).Finite
⊢ (⇑{ toFun := f, measurableSet_fiber' := h, finite_range' := h' : α →ₛ β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α → β
h : ∀ (x : β), MeasurableSet (f ⁻¹' {x})
h' : (range f).Finite
x : α
⊢ ({ toFun := f, measurableSet_fiber' := h, finite_range' := h' : α →ₛ β } : (a : α) → β) x = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
b : β
⊢ b ∈ f.range ↔ Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b

Tactic:
Finite.mem_toFinset _

Premises used: Set.Mem, Set.Finite.mem_toFinset, setOf
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
x : α
⊢ Membership.mem (α := β) f.range ((f : (a : α) → β) x : β)

Tactic:
mem_range.2 ⟨x, rfl⟩

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.mem_range, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
⊢ (↑f.range : Set β) = range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
f.finite_range.coe_toFinset

Premises used: MeasureTheory.SimpleFunc.finite_range, setOf, Set.Finite.coe_toFinset
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
x : β
μ : Measure α
H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ x ∈ f.range

Tactic:
let ⟨a, ha⟩ := nonempty_of_measure_ne_zero H
  mem_range.2 ⟨a, ha⟩

Premises used: Iff.mpr, MeasureTheory.nonempty_of_measure_ne_zero, MeasureTheory.SimpleFunc.mem_range, _private.0.MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero.match_1, Membership.mem, Exists.intro, MeasureTheory.SimpleFunc.range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∀ y ∈ f.range, p y) ↔ ∀ (x : α), p ((f : (a : α) → β) x)

Tactic:
simp only [mem_range, Set.forall_mem_range]

Premises used: Set.forall_mem_range, MeasureTheory.SimpleFunc.mem_range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y ∈ f.range, p y) ↔ ∃ (x : α), p ((f : (a : α) → β) x)

Tactic:
simpa only [mem_range, exists_prop] using Set.exists_range_iff

Premises used: MeasureTheory.SimpleFunc.mem_range, exists_prop, Set.exists_range_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
b : β
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {b}) ∅ ↔ b ∉ f.range

Tactic:
preimage_singleton_eq_empty.trans <| not_congr mem_range.symm

Premises used: MeasureTheory.SimpleFunc.mem_range, Set.preimage_singleton_eq_empty, Iff.trans, Iff.symm, not_congr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : Preorder β
inst_3 : IsDirectedOrder β
f : α →ₛ β
⊢ ∃ (C : β), ∀ (x : α), (f : (a : α) → β) x ≤ C

Tactic:
f.range.exists_le.imp fun _ => forall_mem_range.1

Premises used: Exists.imp, Finset.exists_le, MeasureTheory.SimpleFunc.range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
a : α
b : β
⊢ (const α b : (a : α) → β) a = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
b : β
⊢ (⇑(const α b) : (a : α) → β) = Function.const α b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
β : Type u_2
α : Type u_5
inst : MeasurableSpace α
inst_1 : Nonempty α
b : β
⊢ (↑(SimpleFunc.range (const α b)) : Set β) = (↑{b} : Set β)

Tactic:
simp +unfoldPartialApp [Function.const]

Premises used: Function.const
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
β : Type u_2
α : Type u_5
inst : MeasurableSpace α
b : β
⊢ (↑(SimpleFunc.range (const α b)) : Set β) ⊆ (↑{b} : Set β)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst : Nonempty β
⊢ ∀ (x : β), MeasurableSet.{u_5} (α := α) (preimage (β := β) (⇑f : (a : α) → β) {x})

Tactic:
have hf_meas := @SimpleFunc.measurableSet_fiber α _ ⊥ f
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet.{u_5} (α := α) (preimage (β := β) (⇑f : (a : α) → β) {x})
⊢ ∀ (x : β),
    Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) ∅ ∨
      Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) univ

Tactic:
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas

Premises used: MeasurableSpace.measurableSet_bot_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst : Nonempty β
hf_meas :
  ∀ (x : β),
    Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) ∅ ∨
      Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) univ
⊢ ∃ (c : β), ∀ (x : α), (f : (a : α) → β) x = c

Tactic:
(exists_eq_const_of_preimage_singleton hf_meas).imp fun c hc ↦ congr_fun hc

Premises used: Set.exists_eq_const_of_preimage_singleton, Exists.imp, congr_fun
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst : Nonempty β
hf_meas :
  ∀ (x : β),
    Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) ∅ ∨
      Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) univ
⊢ ∃ (c : β), ∀ (x : α), (f : (a : α) → β) x = c

Tactic:
exact (exists_eq_const_of_preimage_singleton hf_meas).imp fun c hc ↦ congr_fun hc

Premises used: Set.exists_eq_const_of_preimage_singleton, Exists.imp, congr_fun
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
β : Type u_2
α : Type u_5
inst : Nonempty β
f : α →ₛ β
⊢ ∃ (c : β), f = const α c

Tactic:
letI : MeasurableSpace α := ⊥; (simpleFunc_bot f).imp fun _ ↦ ext

Premises used: Exists.imp, MeasureTheory.SimpleFunc.simpleFunc_bot, MeasureTheory.SimpleFunc.ext
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) {a : α | r a ((f : (a : α) → β) a)} a ↔
      Membership.mem (γ := Set α)
        (⋃ (b : β),
          ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
            {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
        a
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})

Tactic:
ext a
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
a : α
this :
  r a ((f : (a : α) → β) a) ↔
    ∃ (i : α), r a ((f : (a : α) → β) i) ∧ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) i : β)
⊢ Membership.mem (γ := Set α) {a : α | r a ((f : (a : α) → β) a)} a ↔
    Membership.mem (γ := Set α)
      (⋃ (b : β),
        ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
          {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
      a

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
a : α
h₁ :
  r a ((f : (a : α) → β) a) ↔
    ∃ (i : α), r a ((f : (a : α) → β) i) ∧ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) i : β)
⊢ Membership.mem (γ := Set α) {a : α | r a ((f : (a : α) → β) a)} a ↔
    Membership.mem (γ := Set α)
      (⋃ (b : β),
        ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
          {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
      a

Tactic:
suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
a : α
⊢ r a ((f : (a : α) → β) a) ↔
    ∃ (i : α), r a ((f : (a : α) → β) i) ∧ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) i : β)

Tactic:
⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩

Premises used: Eq.rec, And.intro, Iff.intro, Exists.intro, _private.0.MeasureTheory.SimpleFunc.measurableSet_cut.match_1, Eq.symm, DFunLike.coe, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
a : α
⊢ r a ((f : (a : α) → β) a) ↔
    ∃ (i : α), r a ((f : (a : α) → β) i) ∧ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) i : β)

Tactic:
exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})

Tactic:
have : { a | r a (f a) } = ⋃ b ∈ range f, { a | r a b } ∩ f ⁻¹' {b} := by
    ext a
    suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
    exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
rw :
  MeasurableSet.{u_1} (α := α)
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
⊢ MeasurableSet.{u_1} (α := α) {a : α | r a ((f : (a : α) → β) a)}

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
⊢ MeasurableSet.{u_1} (α := α)
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})

Tactic:
MeasurableSet.biUnion f.finite_range.countable fun b _ =>
      MeasurableSet.inter (h b) (f.measurableSet_fiber _)

Premises used: MeasureTheory.SimpleFunc.finite_range, MeasureTheory.SimpleFunc.measurableSet_fiber, MeasurableSet.biUnion, Set.Finite.countable, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
⊢ MeasurableSet.{u_1} (α := α)
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})

Tactic:
exact
    MeasurableSet.biUnion f.finite_range.countable fun b _ =>
      MeasurableSet.inter (h b) (f.measurableSet_fiber _)

Premises used: MeasureTheory.SimpleFunc.finite_range, MeasureTheory.SimpleFunc.measurableSet_fiber, MeasurableSet.biUnion, Set.Finite.countable, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
s : Set β
⊢ MeasurableSet.{u_1} (α := α) ((⇑f : (a : α) → β) ⁻¹' s)

Tactic:
measurableSet_cut (fun _ b => b ∈ s) f fun b => MeasurableSet.const (b ∈ s)

Premises used: Membership.mem, MeasurableSet.const, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_cut
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α →ₛ β
⊢ Measurable.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
fun s _ =>
  measurableSet_preimage f s

Premises used: Measurable, MeasureTheory.SimpleFunc.measurableSet_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : α →ₛ β
⊢ AEMeasurable.{u_1, u_2} (β := β) (⇑f : (a : α) → β) μ

Tactic:
f.measurable.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.SimpleFunc.measurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
μ : Measure α
s : Finset β
⊢ Eq (α := ℝ≥0∞) (∑ y ∈ s, (μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' (↑s : Set β)) : ℝ≥0∞)

Tactic:
sum_measure_preimage_singleton _ fun _ _ => f.measurableSet_fiber _

Premises used: MeasureTheory.sum_measure_preimage_singleton, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
μ : Measure α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' (↑f.range : Set β)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ y ∈ f.range, (μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]

Premises used: MeasureTheory.SimpleFunc.coe_range, MeasureTheory.SimpleFunc.sum_measure_preimage_singleton, Set.preimage_range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet s
f g : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑(piecewise s hs f g) : (a : α) → β)
    (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: Set.piecewise, rfl, ite
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet s
f g : α →ₛ β
a : α
⊢ Eq.{u_2 + 1} (α := β) ((piecewise s hs f g : (a : α) → β) a : β)
    (if a ∈ s then (f : (a : α) → β) a else (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: Set.piecewise, rfl, ite
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet sᶜ
f g : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑(piecewise sᶜ hs f g) : (a : α) → β) (⇑(piecewise s ⋯ g f) : (a : α) → β)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f g : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑(piecewise univ ⋯ f g) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f g : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑(piecewise ∅ ⋯ f g) : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ piecewise s hs f f = f

Tactic:
coe_injective <| Set.piecewise_same _ _

Premises used: Set.piecewise_same, MeasureTheory.SimpleFunc.coe_injective
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
f : α →ₛ β
⊢ support.{u_1, u_2} (M := β) (⇑(piecewise s hs f (const α 0)) : (a : α) → β) =
    s ∩ support.{u_1, u_2} (M := β) (⇑f : (a : α) → β)

Tactic:
Set.support_indicator

Premises used: Set.support_indicator, Set.indicator, Set.piecewise, ite
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet s
hs_nonempty : s.Nonempty
hs_ne_univ : s ≠ univ
x y : β
⊢ (piecewise s hs (const α x) (const α y)).range = {x, y}

Tactic:
simp only [← Finset.coe_inj, coe_range, coe_piecewise, range_piecewise, coe_const,
    Finset.coe_insert, Finset.coe_singleton, hs_nonempty.image_const,
    (nonempty_compl.2 hs_ne_univ).image_const, singleton_union, Function.const]

Premises used: MeasureTheory.SimpleFunc.coe_range, Iff.mpr, Finset.coe_singleton, MeasureTheory.SimpleFunc.coe_piecewise, Set.Nonempty.image_const, Set.singleton_union, Finset.coe_inj, Function.const, Set.range_piecewise, Finset.coe_insert, MeasureTheory.SimpleFunc.coe_const, Set.nonempty_compl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
f : α →ₛ β
g : β → α → γ
hg : ∀ (b : β), Measurable (g b)
⊢ Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ g ((f : (a : α) → β) a) a

Tactic:
fun s hs =>
  f.measurableSet_cut (fun a b => g b a ∈ s) fun b => hg b hs

Premises used: Set.Mem, Measurable, setOf, Membership.mem, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_cut
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
f : α →ₛ β
g : β → α →ₛ γ
a : α
⊢ Membership.mem (γ := Set γ)
    (⋃ (i : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) i),
        range.{u_3, u_1 + 1} (ι := α) (⇑(g i) : (a : α) → γ))
    ((fun (a : α) ↦ ((g ((f : (a : α) → β) a) : (a : α) → γ) a : γ)) a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : β → α →ₛ γ
a : α
⊢ Eq.{u_3 + 1} (α := γ) ((f.bind g : (a : α) → γ) a : γ) ((g ((f : (a : α) → β) a) : (a : α) → γ) a : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
g : β → γ
f : α →ₛ β
a : α
⊢ (map g f : (a : α) → γ) a = g ((f : (a : α) → β) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
g : β → γ
h : γ → δ
f : α →ₛ β
⊢ map h (map g f) = map (h ∘ g) f

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.bind, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
g : β → γ
f : α →ₛ β
⊢ Eq (α := (a : α) → γ) (⇑(map g f) : (a : α) → γ) (g ∘ (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : DecidableEq γ
g : β → γ
f : α →ₛ β
⊢ (↑(map g f).range : Set γ) = (↑(Finset.image g f.range) : Set γ)

Tactic:
simp only [coe_range, coe_map, Finset.coe_image, range_comp]

Premises used: MeasureTheory.SimpleFunc.coe_range, Set.range_comp, Finset.coe_image, MeasureTheory.SimpleFunc.coe_map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
g : β → γ
b : β
⊢ Eq (α := α →ₛ γ) (map g (const α b)) (const α (g b))

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.const, MeasureTheory.SimpleFunc.bind, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
simp : Eq.{u_1 + 1} (α := Set α) (g ∘ (⇑f : (a : α) → β) ⁻¹' s) ((⇑f : (a : α) → β) ⁻¹' g ⁻¹' s)
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑(map g f) : (a : α) → γ) ⁻¹' s)
    ((⇑f : (a : α) → β) ⁻¹' (↑({b ∈ f.range | g b ∈ s}) : Set β))

Tactic:
simp only [coe_range, sep_mem_eq, coe_map, Finset.coe_filter,
    ← mem_preimage, inter_comm, preimage_inter_range, ← Finset.mem_coe]

Premises used: MeasureTheory.SimpleFunc.coe_range, Finset.coe_filter, Set.preimage_inter_range, MeasureTheory.SimpleFunc.coe_map, Set.sep_mem_eq, Set.inter_comm, Finset.mem_coe, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ Eq.{u_1 + 1} (α := Set α) (g ∘ (⇑f : (a : α) → β) ⁻¹' s) ((⇑f : (a : α) → β) ⁻¹' g ⁻¹' s)

Tactic:
preimage_comp

Premises used: Set.preimage_comp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ Eq.{u_1 + 1} (α := Set α) (g ∘ (⇑f : (a : α) → β) ⁻¹' s) ((⇑f : (a : α) → β) ⁻¹' g ⁻¹' s)

Tactic:
exact preimage_comp

Premises used: Set.preimage_comp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : β → γ
c : γ
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := γ) (⇑(map g f) : (a : α) → γ) {c})
    ((⇑f : (a : α) → β) ⁻¹' (↑({b ∈ f.range | g b = c}) : Set β))

Tactic:
map_preimage _ _ _

Premises used: Set.Mem, setOf, Set.singleton, MeasureTheory.SimpleFunc.map_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β →ₛ γ
g : α → β
hgm : Measurable g
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g hgm) : (a : α) → γ) ((⇑f : (a : β) → γ) ∘ g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β →ₛ γ
g : α → β
hgm : Measurable g
⊢ (↑(f.comp g hgm).range : Set γ) ⊆ (↑f.range : Set γ)

Tactic:
simp only [coe_range, coe_comp, Set.range_comp_subset_range]

Premises used: MeasureTheory.SimpleFunc.coe_range, Set.range_comp_subset_range, MeasureTheory.SimpleFunc.coe_comp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
this : MeasurableSpace γ := ⊤
⊢ MeasurableSingletonClass γ

Tactic:
haveI : MeasurableSingletonClass γ := ⟨fun _ => trivial⟩