case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.39044
δ : Type ?u.39047
l : Filter α
f✝ g h : α → β
x✝ : Germ l β
f : α → β
⊢ map id (Quot.mk Setoid.r f) = id (Quot.mk Setoid.r f)
α : Type u_1
β : Type u_2
γ : Type ?u.39044
δ : Type ?u.39047
l : Filter α
f g h : α → β
⊢ map id = id
ext ⟨f⟩
no goals
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.39044
δ : Type ?u.39047
l : Filter α
f✝ g h : α → β
x✝ : Germ l β
f : α → β
⊢ map id (Quot.mk Setoid.r f) = id (Quot.mk Setoid.r f)
rfl