-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
private lemma measurable_const_mul (c : EReal) : Measurable fun (x : EReal) ↦ c * x

Proof state:
c : EReal
⊢ (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥

Tactic:
ext p

Result:
case h
c : EReal
p : ℝ
⊢ ⊥ * ↑p = if p = 0 then 0 else if p < 0 then ⊤ else ⊥

Proof state:
case h_top
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => -(⊥ * ↑p)

Tactic:
apply Measurable.neg

Result:
case h_top.hf
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun x => ⊥ * ↑x

Proof state:
c : EReal
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => if p < 0 then ⊤ else ⊥

Tactic:
exact Measurable.piecewise measurableSet_Iio measurable_const measurable_const

Result:
no goals

Proof state:
case pos
c : EReal
p : ℝ
h1 : p = 0
⊢ ⊥ * ↑p = 0

Tactic:
simp [h1]

Result:
no goals

Proof state:
case h_top
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => ⊤ * ↑p

Tactic:
simp_rw [← neg_bot, neg_mul]

Result:
case h_top
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => -(⊥ * ↑p)

Proof state:
case neg
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : ¬p < 0
⊢ 0 < p

Tactic:
exact lt_of_le_of_ne (not_lt.mp h2) (Ne.symm h1)

Result:
no goals

Proof state:
c : EReal
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => c * ↑p

Tactic:
have h2 : Measurable fun (p : ℝ) ↦ if p = 0 then (0 : EReal) else if p < 0 then ⊤ else ⊥ := by
  refine Measurable.piecewise (measurableSet_singleton _) measurable_const ?_
  exact Measurable.piecewise measurableSet_Iio measurable_const measurable_const

Result:
c : EReal
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => c * ↑p

Proof state:
c : EReal
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => c * ↑p

Tactic:
induction c with
| h_bot => rwa [h1]
| h_real c => exact (measurable_id.const_mul _).coe_real_ereal
| h_top =>
  simp_rw [← neg_bot, neg_mul]
  apply Measurable.neg
  rwa [h1]

Result:
no goals

Proof state:
case h_bot
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => ⊥ * ↑p

Tactic:
rwa [h1]

Result:
no goals

Proof state:
case h
c : EReal
p : ℝ
⊢ ⊥ * ↑p = if p = 0 then 0 else if p < 0 then ⊤ else ⊥

Tactic:
split_ifs with h1 h2

Result:
case pos
c : EReal
p : ℝ
h1 : p = 0
⊢ ⊥ * ↑p = 0

case pos
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : p < 0
⊢ ⊥ * ↑p = ⊤

case neg
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : ¬p < 0
⊢ ⊥ * ↑p = ⊥

Proof state:
case pos
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : p < 0
⊢ ⊥ * ↑p = ⊤

Tactic:
rw [bot_mul_coe_of_neg h2]

Result:
no goals

Proof state:
c : EReal
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥

Tactic:
refine Measurable.piecewise (measurableSet_singleton _) measurable_const ?_

Result:
c : EReal
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun p => if p < 0 then ⊤ else ⊥

Proof state:
case h_top.hf
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable fun x => ⊥ * ↑x

Tactic:
rwa [h1]

Result:
no goals

Proof state:
case neg
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : ¬p < 0
⊢ ⊥ * ↑p = ⊥

Tactic:
rw [bot_mul_coe_of_pos]

Result:
case neg
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : ¬p < 0
⊢ 0 < p

Proof state:
case h_real
h1 : (fun p => ⊥ * ↑p) = fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable fun p => if p = 0 then 0 else if p < 0 then ⊤ else ⊥
c : ℝ
⊢ Measurable fun p => ↑c * ↑p

Tactic:
exact (measurable_id.const_mul _).coe_real_ereal

Result:
no goals

Proof state:
c : EReal
⊢ Measurable fun x => c * x

Tactic:
refine measurable_of_measurable_real ?_

Result:
c : EReal
⊢ Measurable fun p => c * ↑p