awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable f

Tactic:
measurable_of_real_prod ?_ ?_ ?_

Premises used: EReal.measurable_of_real_prod
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
refine_1 : Measurable.{0, u_6} (β := β) fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)
refine_2 : Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊥, x)
refine_3 : Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊤, x)
⊢ Measurable f

Tactic:
refine measurable_of_real_prod ?_ ?_ ?_

Premises used: EReal.measurable_of_real_prod
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)

Tactic:
measurable_swap_iff.mp <| measurable_of_real_prod ?_ h_bot_right h_top_right

Premises used: EReal.measurable_of_real_prod, Iff.mp, measurable_swap_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
refine_1 :
  Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦
    ((fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)) ∘ Prod.swap) ((↑p.1 : EReal), p.2)
⊢ Measurable.{0, u_6} (β := β) fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)

Tactic:
refine measurable_swap_iff.mp <| measurable_of_real_prod ?_ h_bot_right h_top_right

Premises used: EReal.measurable_of_real_prod, Iff.mp, measurable_swap_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦
    ((fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)) ∘ Prod.swap) ((↑p.1 : EReal), p.2)

Tactic:
h_real.comp measurable_swap

Premises used: WithBot.some, WithBot, Measurable.comp, EReal, measurable_swap, Real.toEReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦
    ((fun (p : ℝ × EReal) ↦ f ((↑p.1 : EReal), p.2)) ∘ Prod.swap) ((↑p.1 : EReal), p.2)

Tactic:
exact h_real.comp measurable_swap

Premises used: Measurable.comp, measurable_swap
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊥, x)

Tactic:
measurable_of_measurable_real h_bot_left

Premises used: EReal.measurable_of_measurable_real
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊥, x)

Tactic:
exact measurable_of_measurable_real h_bot_left

Premises used: EReal.measurable_of_measurable_real
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊤, x)

Tactic:
measurable_of_measurable_real h_top_left

Premises used: EReal.measurable_of_measurable_real
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable.{0, u_6} (β := β) fun (p : ℝ × ℝ) ↦ f ((↑p.1 : EReal), (↑p.2 : EReal))
h_bot_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊥, (↑r : EReal))
h_top_left : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f (⊤, (↑r : EReal))
h_bot_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊥)
h_top_right : Measurable.{0, u_6} (β := β) fun (r : ℝ) ↦ f ((↑r : EReal), ⊤)
⊢ Measurable.{0, u_6} (β := β) fun (x : EReal) ↦ f (⊤, x)

Tactic:
exact measurable_of_measurable_real h_top_left

Premises used: EReal.measurable_of_measurable_real
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
⊢ Measurable (β := EReal) fun (x : EReal) ↦ c * x

Tactic:
measurable_of_measurable_real ?_

Premises used: EReal.measurable_of_measurable_real
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
refine : Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)
⊢ Measurable (β := EReal) fun (x : EReal) ↦ c * x

Tactic:
refine measurable_of_measurable_real ?_

Premises used: EReal.measurable_of_measurable_real
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
h : ∀ (p : ℝ), ⊥ * (↑p : EReal) = if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥

Tactic:
ext p
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
p : ℝ
pos : ∀ (h1 : p = 0), ⊥ * (↑p : EReal) = 0
pos₁ : ∀ (h1 : ¬p = 0) (h2 : p < 0), ⊥ * (↑p : EReal) = ⊤
neg : ∀ (h1 : ¬p = 0) (h2 : ¬p < 0), ⊥ * (↑p : EReal) = ⊥
⊢ ⊥ * (↑p : EReal) = if p = 0 then 0 else if p < 0 then ⊤ else ⊥

Tactic:
split_ifs with h1 h2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
p : ℝ
h1 : p = 0
⊢ ⊥ * (↑p : EReal) = 0

Tactic:
simp [h1]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : p < 0
pos pos₁ : Eq (α := EReal) ⊤ ⊤
⊢ ⊥ * (↑p : EReal) = ⊤

Tactic:
rw [bot_mul_coe_of_neg h2]

Premises used: EReal.bot_mul_coe_of_neg
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : ¬p < 0
neg : 0 < p
⊢ ⊥ * (↑p : EReal) = ⊥

Tactic:
rw [bot_mul_coe_of_pos]

Premises used: EReal.bot_mul_coe_of_pos
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
p : ℝ
h1 : ¬p = 0
h2 : ¬p < 0
⊢ 0 < p

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

Premises used: Ne.symm, not_lt, Iff.mp, lt_of_le_of_ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
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)

Premises used: Ne.symm, not_lt, Iff.mp, lt_of_le_of_ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
⊢ Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥

Tactic:
have h1 : (fun (p : ℝ) ↦ (⊥ : EReal) * p)
      = fun p ↦ if p = 0 then (0 : EReal) else (if p < 0 then ⊤ else ⊥) := by
    ext p
    split_ifs with h1 h2
    · simp [h1]
    · rw [bot_mul_coe_of_neg h2]
    · rw [bot_mul_coe_of_pos]
      exact lt_of_le_of_ne (not_lt.mp h2) (Ne.symm h1)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥

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

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, Measurable.piecewise, measurable_const, Set.piecewise
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
refine : Measurable (β := EReal) fun (p : ℝ) ↦ if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥

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

Premises used: MeasurableSingletonClass.measurableSet_singleton, Measurable.piecewise, measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ if p < 0 then ⊤ else ⊥

Tactic:
Measurable.piecewise measurableSet_Iio measurable_const measurable_const

Premises used: Set.Mem, measurableSet_Iio, Measurable.piecewise, measurable_const, Set.piecewise
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ if p < 0 then ⊤ else ⊥

Tactic:
exact Measurable.piecewise measurableSet_Iio measurable_const measurable_const

Premises used: measurableSet_Iio, Measurable.piecewise, measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥

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
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
bot bot₁ bot₂ bot₃ : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ ⊥ * (↑p : EReal)

Tactic:
rwa [h1]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
c : ℝ
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ (↑c : EReal) * (↑p : EReal)

Tactic:
(measurable_id.const_mul _).coe_real_ereal

Premises used: WithBot.some, measurable_id, EReal.mul, Measurable.const_mul, Measurable.coe_real_ereal, Real.toEReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
c : ℝ
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ (↑c : EReal) * (↑p : EReal)

Tactic:
exact (measurable_id.const_mul _).coe_real_ereal

Premises used: measurable_id, Measurable.const_mul, Measurable.coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
top : Measurable (β := EReal) fun (p : ℝ) ↦ -(⊥ * (↑p : EReal))
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ ⊤ * (↑p : EReal)

Tactic:
simp_rw [← neg_bot, neg_mul]

Premises used: neg_mul, EReal.neg_bot
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
top : Measurable (β := EReal) fun (x : ℝ) ↦ ⊥ * (↑x : EReal)
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ -(⊥ * (↑p : EReal))

Tactic:
apply Measurable.neg

Premises used: Measurable.neg
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 top top₁ top₂ top₃ : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
⊢ Measurable (β := EReal) fun (x : ℝ) ↦ ⊥ * (↑x : EReal)

Tactic:
rwa [h1]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
c : EReal
h1 :
  Eq (α := (p : ℝ) → EReal) (fun (p : ℝ) ↦ ⊥ * (↑p : EReal)) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
h2 : Measurable (β := EReal) fun (p : ℝ) ↦ if p = 0 then 0 else if p < 0 then ⊤ else ⊥
bot : Measurable (β := EReal) fun (p : ℝ) ↦ ⊥ * (↑p : EReal)
coe : ∀ (c : ℝ), Measurable (β := EReal) fun (p : ℝ) ↦ (↑c : EReal) * (↑p : EReal)
top : Measurable (β := EReal) fun (p : ℝ) ↦ ⊤ * (↑p : EReal)
⊢ Measurable (β := EReal) fun (p : ℝ) ↦ c * (↑p : EReal)

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

Premises used: measurable_id, Measurable.neg, Measurable.const_mul, neg_mul, Measurable.coe_real_ereal, EReal.neg_bot
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ MeasurableMul₂ EReal

Tactic:
⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩

Premises used: MeasurableMul₂.mk, EReal.measurable_of_real_real
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
refine_1 :
  Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2
refine_2 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊥, (↑r : EReal)).1 * (⊥, (↑r : EReal)).2
refine_3 : Measurable (β := EReal) fun (r : ℝ) ↦ (⊤, (↑r : EReal)).1 * (⊤, (↑r : EReal)).2
refine_4 : Measurable (β := EReal) fun (r : ℝ) ↦ ((↑r : EReal), ⊥).1 * ((↑r : EReal), ⊥).2
refine_5 : Measurable (β := EReal) fun (r : ℝ) ↦ ((↑r : EReal), ⊤).1 * ((↑r : EReal), ⊤).2
⊢ MeasurableMul₂ EReal

Tactic:
refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2

Tactic:
(measurable_fst.mul measurable_snd).coe_real_ereal

Premises used: WithBot.some, Measurable.mul, measurable_snd, EReal.mul, Measurable.coe_real_ereal, measurable_fst, Real.toEReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (p : ℝ × ℝ) ↦ ((↑p.1 : EReal), (↑p.2 : EReal)).1 * ((↑p.1 : EReal), (↑p.2 : EReal)).2

Tactic:
exact (measurable_fst.mul measurable_snd).coe_real_ereal

Premises used: Measurable.mul, measurable_snd, Measurable.coe_real_ereal, measurable_fst
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ (⊥, (↑r : EReal)).1 * (⊥, (↑r : EReal)).2

Tactic:
(measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ (⊥, (↑r : EReal)).1 * (⊥, (↑r : EReal)).2

Tactic:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ (⊤, (↑r : EReal)).1 * (⊤, (↑r : EReal)).2

Tactic:
(measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: WithBot.some, Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ (⊤, (↑r : EReal)).1 * (⊤, (↑r : EReal)).2

Tactic:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ ⊥ * (↑r : EReal)

Tactic:
(measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ ⊥ * (↑r : EReal)

Tactic:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ ⊤ * (↑r : EReal)

Tactic:
(measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α_1
mα_1 : MeasurableSpace α_1
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable (β := EReal) fun (r : ℝ) ↦ ⊤ * (↑r : EReal)

Tactic:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

Premises used: Measurable.comp, _private.0.EReal.measurable_const_mul, measurable_coe_real_ereal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (n : ℕ), norm_sets n) x ↔ Membership.mem (γ := Set α) univ x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
x : α
h : ∃ (i : ℕ), x ∈ norm_sets i
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), norm_sets n) x ↔ Membership.mem (γ := Set α) univ x

Tactic:
simp only [Set.mem_iUnion, Set.mem_univ, iff_true]

Premises used: Set.mem_iUnion, iff_true, Set.mem_univ
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
x : α
⊢ ∃ (i : ℕ), x ∈ norm_sets i

Tactic:
exists_nat_ge (f x)

Premises used: Set.Mem, setOf, exists_nat_ge