α : Type u_1
β : Type u_2
γ : Type ?u.9600
δ : Type ?u.9603
δ' : Type ?u.9606
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
⊢ Measurable f
α : Type u_1
β : Type u_2
γ : Type ?u.9600
δ : Type ?u.9603
δ' : Type ?u.9606
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
⊢ Measurable f
nontriviality β
α : Type u_1
β : Type u_2
γ : Type ?u.9600
δ : Type ?u.9603
δ' : Type ?u.9606
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ Measurable f
α : Type u_1
β : Type u_2
γ : Type ?u.9600
δ : Type ?u.9603
δ' : Type ?u.9606
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
⊢ Measurable f
inhabit β
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.9600
δ : Type ?u.9603
δ' : Type ?u.9606
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
inhabited_h : Inhabited β
x✝ : β
⊢ f x✝ = f default
α : Type u_1
β : Type u_2
γ : Type ?u.9600
δ : Type ?u.9603
δ' : Type ?u.9606
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ Measurable f
convert @measurable_const α β ‹_› ‹_› (f default) using 2
no goals
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.9600
δ : Type ?u.9603
δ' : Type ?u.9606
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
inhabited_h : Inhabited β
x✝ : β
⊢ f x✝ = f default
apply hf