α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
⊢ ∃ c, f = const α c
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
⊢ ∃ c, f = const α c
letI : MeasurableSpace α := ⊥
case intro
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
⊢ ∃ c, f = const α c
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
⊢ ∃ c, f = const α c
obtain ⟨c, h_eq⟩ := simpleFunc_bot f
case intro
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
⊢ f = const α c
case intro
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
⊢ ∃ c, f = const α c
refine' ⟨c, _⟩
case intro.H
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
x : α
⊢ ↑f x = ↑(const α c) x
case intro
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
⊢ f = const α c
ext1 x
no goals
case intro.H
α✝ : Type ?u.21990
β : Type u_2
γ : Type ?u.21996
δ : Type ?u.21999
inst✝¹ : MeasurableSpace α✝
α : Type u_1
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
x : α
⊢ ↑f x = ↑(const α c) x
rw [h_eq x, SimpleFunc.coe_const, Function.const]