-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem _root_.Measurable.simpleFunc_add
    {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddGroup E] [MeasurableAdd E]
    {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) :
    Measurable ((f : α → E) + g)

Proof state:
case h_add
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
this : ⇑(f + f') + g = (support ⇑f).piecewise (⇑f + g) (⇑f' + g)
⊢ Measurable ((support ⇑f).piecewise (⇑f + g) (⇑f' + g))

Tactic:
exact Measurable.piecewise f.measurableSet_support hf hf'

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
x : α
hx : x ∉ support ⇑f
⊢ (⇑(f + f') + g) x = (support ⇑f).piecewise (⇑f + g) (⇑f' + g) x

Tactic:
simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
  Set.piecewise_eq_of_not_mem _ _ _ hx, _root_.add_left_inj, add_left_eq_self] using hx

Result:
no goals

Proof state:
case h_ind
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
c : E
s : Set α
hs : MeasurableSet s
⊢ Measurable (⇑(piecewise s hs (const α c) (const α 0)) + g)

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
  SimpleFunc.coe_zero]

Result:
case h_ind
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
c : E
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.piecewise (Function.const α c) 0 + g)

Proof state:
case pos
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
x : α
hx : x ∈ support ⇑f
⊢ (⇑(f + f') + g) x = (support ⇑f).piecewise (⇑f + g) (⇑f' + g) x

Tactic:
simpa only [coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
  Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_left_inj, add_right_eq_self]
  using Set.disjoint_left.1 hff' hx

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
x : α
⊢ (⇑(f + f') + g) x = (support ⇑f).piecewise (⇑f + g) (⇑f' + g) x

Tactic:
by_cases hx : x ∈ Function.support f

Result:
case pos
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
x : α
hx : x ∈ support ⇑f
⊢ (⇑(f + f') + g) x = (support ⇑f).piecewise (⇑f + g) (⇑f' + g) x

case neg
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
x : α
hx : x ∉ support ⇑f
⊢ (⇑(f + f') + g) x = (support ⇑f).piecewise (⇑f + g) (⇑f' + g) x

Proof state:
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f : α →ₛ E
⊢ Measurable (⇑f + g)

Tactic:
induction' f using SimpleFunc.induction with c s hs f f' hff' hf hf'

Result:
case h_ind
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
c : E
s : Set α
hs : MeasurableSet s
⊢ Measurable (⇑(piecewise s hs (const α c) (const α 0)) + g)

case h_add
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
⊢ Measurable (⇑(f + f') + g)

Proof state:
case h_ind
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
c : E
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.piecewise (Function.const α c + g) (0 + g))

Tactic:
exact Measurable.piecewise hs (hg.const_add _) (hg.const_add _)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
⊢ ⇑(f + f') + g = (support ⇑f).piecewise (⇑f + g) (⇑f' + g)

Tactic:
ext x

Result:
case h
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
x : α
⊢ (⇑(f + f') + g) x = (support ⇑f).piecewise (⇑f + g) (⇑f' + g) x

Proof state:
case h_add
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
this : ⇑(f + f') + g = (support ⇑f).piecewise (⇑f + g) (⇑f' + g)
⊢ Measurable (⇑(f + f') + g)

Tactic:
rw [this]

Result:
case h_add
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : Measurable (⇑f + g)
hf' : Measurable (⇑f' + g)
this : ⇑(f + f') + g = (support ⇑f).piecewise (⇑f + g) (⇑f' + g)
⊢ Measurable ((support ⇑f).piecewise (⇑f + g) (⇑f' + g))

Proof state:
case h_ind
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
c : E
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.piecewise (Function.const α c) 0 + g)

Tactic:
rw [← s.piecewise_same g, ← piecewise_add]

Result:
case h_ind
α : Type u_1
E : Type u_5
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : AddGroup E
inst✝ : MeasurableAdd E
g : α → E
hg : Measurable g
c : E
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.piecewise (Function.const α c + g) (0 + g))