[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
f g : LocallyBoundedMap α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
g : LocallyBoundedMap α β
toFun✝ : α → β
comap_cobounded_le'✝ : comap toFun✝ (cobounded β) ≤ cobounded α
h : (fun f => f.toFun) { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ } = (fun f => f.toFun) g
⊢ { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
toFun✝¹ : α → β
comap_cobounded_le'✝¹ : comap toFun✝¹ (cobounded β) ≤ cobounded α
toFun✝ : α → β
comap_cobounded_le'✝ : comap toFun✝ (cobounded β) ≤ cobounded α
h :
  (fun f => f.toFun) { toFun := toFun✝¹, comap_cobounded_le' := comap_cobounded_le'✝¹ } =
    (fun f => f.toFun) { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ }
⊢ { toFun := toFun✝¹, comap_cobounded_le' := comap_cobounded_le'✝¹ } =
    { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
