-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
lemma measurable_of_real_real {f : EReal × EReal → β}
    (h_real : Measurable fun p : ℝ × ℝ ↦ f (p.1, p.2))
    (h_bot_left : Measurable fun r : ℝ ↦ f (⊥, r))
    (h_top_left : Measurable fun r : ℝ ↦ f (⊤, r))
    (h_bot_right : Measurable fun r : ℝ ↦ f (r, ⊥))
    (h_top_right : Measurable fun r : ℝ ↦ f (r, ⊤)) :
    Measurable f

Proof state:
case refine_1
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun p => ((fun p => f (↑p.1, p.2)) ∘ Prod.swap) (↑p.1, p.2)

Tactic:
exact h_real.comp measurable_swap

Result:
no goals

Proof state:
case refine_1
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun p => f (↑p.1, p.2)

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

Result:
case refine_1
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun p => ((fun p => f (↑p.1, p.2)) ∘ Prod.swap) (↑p.1, p.2)

Proof state:
case refine_3
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun x => f (⊤, x)

Tactic:
exact measurable_of_measurable_real h_top_left

Result:
no goals

Proof state:
case refine_2
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun x => f (⊥, x)

Tactic:
exact measurable_of_measurable_real h_bot_left

Result:
no goals

Proof state:
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable f

Tactic:
refine measurable_of_real_prod ?_ ?_ ?_

Result:
case refine_1
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun p => f (↑p.1, p.2)

case refine_2
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun x => f (⊥, x)

case refine_3
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p => f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r => f (⊥, ↑r)
h_top_left : Measurable fun r => f (⊤, ↑r)
h_bot_right : Measurable fun r => f (↑r, ⊥)
h_top_right : Measurable fun r => f (↑r, ⊤)
⊢ Measurable fun x => f (⊤, x)