awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : MeasurableSpace γ := ⊤
this : MeasurableSingletonClass γ
⊢ ∀ (x : γ), MeasurableSet (preimage (β := γ) (Function.extend g (⇑f₁ : (a : α) → γ) (⇑f₂ : (a : β) → γ)) {x})

Tactic:
fun x => hg.measurable_extend f₁.measurable f₂.measurable (measurableSet_singleton _)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.SimpleFunc.measurable, MeasurableEmbedding.measurable_extend
-- 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_1 : MeasurableSpace γ := ⊤
this : MeasurableSingletonClass γ
⊢ ∀ (x : γ), MeasurableSet (preimage (β := γ) (Function.extend g (⇑f₁ : (a : α) → γ) (⇑f₂ : (a : β) → γ)) {x})

Tactic:
exact fun x => hg.measurable_extend f₁.measurable f₂.measurable (measurableSet_singleton _)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.SimpleFunc.measurable, MeasurableEmbedding.measurable_extend
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
x : α
⊢ Eq.{u_3 + 1} (α := γ) ((f₁.extend g hg f₂ : (a : β) → γ) (g x) : γ) ((f₁ : (a : α) → γ) x : γ)

Tactic:
hg.injective.extend_apply _ _ _

Premises used: Function.Injective.extend_apply, dite, Function.extend, MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
y : β
h : ¬∃ (x : α), g x = y
⊢ Eq.{u_3 + 1} (α := γ) ((f₁.extend g hg f₂ : (a : β) → γ) y : γ) ((f₂ : (a : β) → γ) y : γ)

Tactic:
Function.extend_apply' _ _ _ h

Premises used: dite, Function.extend, Function.extend_apply'
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
⊢ Eq (α := α → γ) ((⇑(f₁.extend g hg f₂) : (a : β) → γ) ∘ g) (⇑f₁ : (a : α) → γ)

Tactic:
funext fun _ => extend_apply _ _ _ _

Premises used: funext, MeasureTheory.SimpleFunc.extend_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
⊢ (f₁.extend g hg f₂).comp g ⋯ = f₁

Tactic:
coe_injective <| extend_comp_eq' _ hg _

Premises used: MeasureTheory.SimpleFunc.coe_injective, MeasureTheory.SimpleFunc.extend_comp_eq'
-- 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.seq g : (a : α) → γ) a : γ) ((f : (a : α) → β → γ) a ((g : (a : α) → β) a) : γ)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.inter, Set.preimage, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
rw :
  Eq.{u_1 + 1} (α := Set α) ((⇑(f.pair g) : (a : α) → β × γ) ⁻¹' SProd.sprod (α := Set β) (β := Set γ) {b} {c})
    (preimage (β := β) (⇑f : (a : α) → β) {b} ∩ preimage (β := γ) (⇑g : (a : α) → γ) {c})
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := β × γ) (⇑(f.pair g) : (a : α) → β × γ) {(b, c)})
    (preimage (β := β) (⇑f : (a : α) → β) {b} ∩ preimage (β := γ) (⇑g : (a : α) → γ) {c})

Tactic:
rw [← singleton_prod_singleton]

Premises used: Set.singleton_prod_singleton
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑(f.pair g) : (a : α) → β × γ) ⁻¹' SProd.sprod (α := Set β) (β := Set γ) {b} {c})
    (preimage (β := β) (⇑f : (a : α) → β) {b} ∩ preimage (β := γ) (⇑g : (a : α) → γ) {c})

Tactic:
pair_preimage _ _ _ _

Premises used: MeasureTheory.SimpleFunc.pair_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑(f.pair g) : (a : α) → β × γ) ⁻¹' SProd.sprod (α := Set β) (β := Set γ) {b} {c})
    (preimage (β := β) (⇑f : (a : α) → β) {b} ∩ preimage (β := γ) (⇑g : (a : α) → γ) {c})

Tactic:
exact pair_preimage _ _ _ _

Premises used: MeasureTheory.SimpleFunc.pair_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
⊢ map Prod.fst (f.pair 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 α
f : α →ₛ β
g : α →ₛ γ
⊢ map Prod.snd (f.pair g) = g

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.bind, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
H : ∀ (a : α), Eq.{u_2 + 1} (α := β) ((f.bind (const α) : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ f.bind (const α) = f

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

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : One β
⊢ Eq (α := α →ₛ β) (const α 1) 1

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Mul β
f g : α →ₛ β
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Inv β
f : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑f⁻¹ : (a : α) → β) (⇑f : (a : α) → β)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Div β
f g : α →ₛ β
⊢ (⇑(f / g) : (a : α) → β) = HDiv.hDiv (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Max β
f g : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Min β
f g : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑(f ⊓ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Mul β
f g : α →ₛ β
a : α
⊢ (f * g : (a : α) → β) a = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Div β
f g : α →ₛ β
x : α
⊢ (f / g : (a : α) → β) x = HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Inv β
f : α →ₛ β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f⁻¹ : (a : α) → β) x : β) (((f : (a : α) → β) x)⁻¹ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Max β
f g : α →ₛ β
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f ⊔ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Min β
f g : α →ₛ β
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f ⊓ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊓ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty α
inst_2 : One β
x : β
⊢ Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 1) x ↔ Membership.mem (γ := Finset β) {1} x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
h : ∀ (a : β), a ∈ f.range ↔ Membership.mem (γ := Finset β) ∅ a
⊢ f.range = ∅

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
a : β
⊢ a ∈ f.range ↔ Membership.mem (γ := Finset β) ∅ a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
⊢ ∀ {y : β}, Membership.mem (γ := Finset β) (SimpleFunc.range.{u_1, u_2} (α := α) 0) y → y = 0

Tactic:
@(forall_mem_range.2 fun _ => rfl)

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.forall_mem_range, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Mul β
f g : α →ₛ β
⊢ f * g = map (fun (p : β × β) ↦ p.1 * p.2) (f.pair g)

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.seq, MeasureTheory.SimpleFunc.bind, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Max β
f g : α →ₛ β
⊢ f ⊔ g = map (fun (p : β × β) ↦ p.1 ⊔ p.2) (f.pair g)

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.seq, MeasureTheory.SimpleFunc.bind, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Mul β
f : α →ₛ β
b : β
⊢ const α b * f = map (fun (a : β) ↦ b * a) f

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.seq, MeasureTheory.SimpleFunc.bind, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : Mul β
inst_2 : Mul γ
g : β → γ
hg : ∀ (x y : β), g (x * y) = g x * g y
f₁ f₂ : α →ₛ β
⊢ map g (f₁ * f₂) = map g f₁ * map g f₂

Tactic:
ext fun _ => hg _ _

Premises used: MeasureTheory.SimpleFunc.ext, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
K : Type u_5
inst_1 : SMul K β
c : K
f : α →ₛ β
⊢ (⇑(c • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) c (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
K : Type u_5
inst_1 : SMul K β
k : K
f : α →ₛ β
a : α
⊢ (k • f : (a : α) → β) a = HSMul.hSMul (β := β) k ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Monoid β
f : α →ₛ β
n : ℕ
⊢ (⇑(f ^ n) : (a : α) → β) = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Monoid β
n : ℕ
f : α →ₛ β
a : α
⊢ (f ^ n : (a : α) → β) a = HPow.hPow (α := β) ((f : (a : α) → β) a : β) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : DivInvMonoid β
f : α →ₛ β
z : ℤ
⊢ (⇑(f ^ z) : (a : α) → β) = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : DivInvMonoid β
z : ℤ
f : α →ₛ β
a : α
⊢ (f ^ z : (a : α) → β) a = HPow.hPow (α := β) ((f : (a : α) → β) a : β) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
K : Type u_5
inst_1 : SMul K β
k : K
f : α →ₛ β
⊢ k • f = map (fun (x : β) ↦ k • x) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
K : Type u_5
inst_1 : SMul K β
k : K
b : β
⊢ HSMul.hSMul (β := α →ₛ β) k (const α b) = const α (k • b)

Tactic:
ext fun _ ↦ rfl

Premises used: MeasureTheory.SimpleFunc.ext, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : NatCast β
n : ℕ
⊢ Eq (α := (a : α) → β) (⇑(↑n : α →ₛ β) : (a : α) → β) fun (x : α) ↦ (↑n : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : IntCast β
n : ℤ
⊢ Eq (α := (a : α) → β) (⇑(↑n : α →ₛ β) : (a : α) → β) fun (x : α) ↦ (↑n : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
K : Type u_5
inst_1 : CommSemiring K
inst_2 : Semiring β
inst_3 : Algebra K β
k : K
⊢ Eq (α := α →ₛ β) (const α ((algebraMap K β : (a : K) → β) k) : α →ₛ β)
    ((algebraMap K (α →ₛ β) : (a : K) → α →ₛ β) k : α →ₛ β)

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.const, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
K : Type u_5
inst_1 : CommSemiring K
inst_2 : Semiring β
inst_3 : Algebra K β
k : K
x : α
⊢ Eq.{u_2 + 1} (α := β) ((((algebraMap K (α →ₛ β) : (a : K) → α →ₛ β) k : α →ₛ β) : (a : α) → β) x : β)
    ((algebraMap K (α → β) : (a : K) → α → β) k x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Star β
f : α →ₛ β
⊢ Eq (α := (a : α) → β) (⇑(star f) : (a : α) → β) (star (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Preorder β
f g : α →ₛ β
⊢ LE.le (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) ↔ f ≤ g

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Preorder β
f g : α →ₛ β
⊢ LT.lt (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) ↔ f < g

Tactic:
.rfl

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

Tactic:
Iff.rfl

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

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Preorder β
s : Set α
f₁ f₂ g₁ g₂ : α →ₛ β
hs : MeasurableSet s
hf : ∀ a ∈ s, LE.le.{u_2} (α := β) ((f₁ : (a : α) → β) a : β) ((f₂ : (a : α) → β) a : β)
hg : ∀ a ∉ s, LE.le.{u_2} (α := β) ((g₁ : (a : α) → β) a : β) ((g₂ : (a : α) → β) a : β)
⊢ piecewise s hs f₁ g₁ ≤ piecewise s hs f₂ g₂

Tactic:
Set.piecewise_mono hf hg

Premises used: Set.piecewise_mono, Set.piecewise, ite
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)

Tactic:
Finset.induction_on s rfl ?_

Premises used: Finset.induction_on
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
refine :
  ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β) →
        Eq.{u_2 + 1} (α := β) (((insert a_1 s).sup f : (a : α) → β) a : β)
          ((insert a_1 s).sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)
⊢ Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)

Tactic:
refine Finset.induction_on s rfl ?_
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s_1 : Finset γ
a_1 : α
a : γ
s : Finset γ
_ :
  a ∉ s →
    Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a_1 : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β) →
      Eq.{u_2 + 1} (α := β) (((insert a s).sup f : (a : α) → β) a_1 : β)
        ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
⊢ a ∉ s →
    Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a_1 : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β) →
      Eq.{u_2 + 1} (α := β) (((insert a s).sup f : (a : α) → β) a_1 : β)
        ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s_1 : Finset γ
a_1 : α
a : γ
s : Finset γ
h : a ∉ s
ih : Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a_1 : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw :
  Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw₁ :
  Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
    ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw₂ :
  Eq.{u_2 + 1} (α := β) ((f a : (a : α) → β) a_1 ⊔ (s.sup f : (a : α) → β) a_1 : β)
    ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := β) ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
    ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
⊢ Eq.{u_2 + 1} (α := β) (((insert a s).sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)

Tactic:
rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]

Premises used: Finset.sup_insert, MeasureTheory.SimpleFunc.sup_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
refine refine₁ :
  ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ∀ (ih : Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)),
        Eq.{u_2 + 1} (α := β) (((insert a_1 s).sup f : (a : α) → β) a : β)
          ((insert a_1 s).sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)
⊢ Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)

Tactic:
classical
  refine Finset.induction_on s rfl ?_
  intro a s _ ih
  rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]

Premises used: Finset.sup_insert, MeasureTheory.SimpleFunc.sup_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : ¬MeasurableSet s
⊢ f.restrict s = 0

Tactic:
dif_neg hs

Premises used: dif_neg, MeasureTheory.SimpleFunc.restrict
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
rw₂ :
  Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
    (s.indicator (⇑f : (a : α) → β))
rw₃ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) 0) (s.indicator (⇑f : (a : α) → β))
rw₄ rw₅ : Eq (α := (a : α) → β) (s.indicator (⇑f : (a : α) → β)) (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))

Tactic:
rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, dif_pos, MeasureTheory.SimpleFunc.restrict, Set.piecewise_eq_indicator
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
rw₂ :
  Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
    (s.indicator (⇑f : (a : α) → β))
rw₃ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) 0) (s.indicator (⇑f : (a : α) → β))
rw₄ rw₅ : Eq (α := (a : α) → β) (s.indicator (⇑f : (a : α) → β)) (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))

Tactic:
classical
  rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, dif_pos, MeasureTheory.SimpleFunc.restrict, Set.piecewise_eq_indicator
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
⊢ f.restrict univ = f

Tactic:
simp [restrict]

Premises used: MeasureTheory.SimpleFunc.restrict
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
⊢ f.restrict ∅ = 0

Tactic:
simp [restrict]

Premises used: MeasureTheory.SimpleFunc.restrict