case mk
α : Type u_1
β : Type u_2
γ : Type ?u.9713
δ : Type ?u.9716
inst✝ : MeasurableSpace α
g : α →ₛ β
toFun✝ : α → β
measurableSet_fiber'✝ : ∀ (x : β), MeasurableSet (toFun✝ ⁻¹' {x})
finite_range'✝ : Set.Finite (range toFun✝)
H : ↑{ toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ } = ↑g
⊢ { toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ } = g
α : Type u_1
β : Type u_2
γ : Type ?u.9713
δ : Type ?u.9716
inst✝ : MeasurableSpace α
f g : α →ₛ β
H : ↑f = ↑g
⊢ f = g
cases f
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.9713
δ : Type ?u.9716
inst✝ : MeasurableSpace α
toFun✝¹ : α → β
measurableSet_fiber'✝¹ : ∀ (x : β), MeasurableSet (toFun✝¹ ⁻¹' {x})
finite_range'✝¹ : Set.Finite (range toFun✝¹)
toFun✝ : α → β
measurableSet_fiber'✝ : ∀ (x : β), MeasurableSet (toFun✝ ⁻¹' {x})
finite_range'✝ : Set.Finite (range toFun✝)
H :
  ↑{ toFun := toFun✝¹, measurableSet_fiber' := measurableSet_fiber'✝¹, finite_range' := finite_range'✝¹ } =
    ↑{ toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ }
⊢ { toFun := toFun✝¹, measurableSet_fiber' := measurableSet_fiber'✝¹, finite_range' := finite_range'✝¹ } =
    { toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ }
case mk
α : Type u_1
β : Type u_2
γ : Type ?u.9713
δ : Type ?u.9716
inst✝ : MeasurableSpace α
g : α →ₛ β
toFun✝ : α → β
measurableSet_fiber'✝ : ∀ (x : β), MeasurableSet (toFun✝ ⁻¹' {x})
finite_range'✝ : Set.Finite (range toFun✝)
H : ↑{ toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ } = ↑g
⊢ { toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ } = g
cases g
no goals
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.9713
δ : Type ?u.9716
inst✝ : MeasurableSpace α
toFun✝¹ : α → β
measurableSet_fiber'✝¹ : ∀ (x : β), MeasurableSet (toFun✝¹ ⁻¹' {x})
finite_range'✝¹ : Set.Finite (range toFun✝¹)
toFun✝ : α → β
measurableSet_fiber'✝ : ∀ (x : β), MeasurableSet (toFun✝ ⁻¹' {x})
finite_range'✝ : Set.Finite (range toFun✝)
H :
  ↑{ toFun := toFun✝¹, measurableSet_fiber' := measurableSet_fiber'✝¹, finite_range' := finite_range'✝¹ } =
    ↑{ toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ }
⊢ { toFun := toFun✝¹, measurableSet_fiber' := measurableSet_fiber'✝¹, finite_range' := finite_range'✝¹ } =
    { toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ }
congr