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

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
⊢ g + ⇑(f + f') = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f')

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
x : α
⊢ (g + ⇑(f + f')) x = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f') x

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
x : α
hx : x ∈ support ⇑f
⊢ (g + ⇑(f + f')) x = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f') x

Tactic:
simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
  Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_right_inj, add_right_eq_self]
  using Set.disjoint_left.1 hff' 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 (s.piecewise (g + Function.const α c) (g + 0))

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

Result:
no goals

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
this : g + ⇑(f + f') = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f')
⊢ Measurable ((support ⇑f).piecewise (g + ⇑f) (g + ⇑f'))

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

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 : α →ₛ E
⊢ Measurable (g + ⇑f)

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 (g + ⇑(piecewise s hs (const α c) (const α 0)))

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
⊢ Measurable (g + ⇑(f + f'))

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 (g + ⇑(piecewise s hs (const α c) (const α 0)))

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 (g + s.piecewise (Function.const α c) 0)

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
this : g + ⇑(f + f') = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f')
⊢ Measurable (g + ⇑(f + f'))

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
this : g + ⇑(f + f') = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f')
⊢ Measurable ((support ⇑f).piecewise (g + ⇑f) (g + ⇑f'))

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
x : α
hx : x ∉ support ⇑f
⊢ (g + ⇑(f + f')) x = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f') 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_right_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 (g + s.piecewise (Function.const α c) 0)

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 (g + Function.const α c) (g + 0))

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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
x : α
⊢ (g + ⇑(f + f')) x = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f') 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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
x : α
hx : x ∈ support ⇑f
⊢ (g + ⇑(f + f')) x = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f') 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 (g + ⇑f)
hf' : Measurable (g + ⇑f')
x : α
hx : x ∉ support ⇑f
⊢ (g + ⇑(f + f')) x = (support ⇑f).piecewise (g + ⇑f) (g + ⇑f') x