[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ map e.symm (map e x) = x
[PROOFSTEP]
convert (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm
[GOAL]
case h.e'_3
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ x = map (e.trans e.symm) x
[PROOFSTEP]
simp
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ map e (map e.symm y) = y
[PROOFSTEP]
convert (congr_fun (EquivFunctor.map_trans' e.symm e) y).symm
[GOAL]
case h.e'_3
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ y = map (e.symm.trans e) y
[PROOFSTEP]
simp
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α✝ β : Type u₀
e : α✝ ≃ β
α : Type u₀
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
[PROOFSTEP]
simp [EquivFunctor.mapEquiv]
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α✝ β : Type u₀
e : α✝ ≃ β
α : Type u₀
⊢ { toFun := id, invFun := id, left_inv := (_ : LeftInverse id id), right_inv := (_ : Function.RightInverse id id) } =
    Equiv.refl (f α)
[PROOFSTEP]
rfl
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
γ : Type u₀
ab : α ≃ β
bc : β ≃ γ
x : f α
⊢ ↑((mapEquiv f ab).trans (mapEquiv f bc)) x = ↑(mapEquiv f (ab.trans bc)) x
[PROOFSTEP]
simp [mapEquiv, map_trans']
[GOAL]
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
⊢ (fun {α β} e => Functor.map ↑e) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
x✝ : f α
⊢ (fun {α β} e => Functor.map ↑e) (Equiv.refl α) x✝ = id x✝
[PROOFSTEP]
apply LawfulFunctor.id_map
[GOAL]
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
⊢ (fun {α β} e => Functor.map ↑e) (k.trans h) = (fun {α β} e => Functor.map ↑e) h ∘ (fun {α β} e => Functor.map ↑e) k
[PROOFSTEP]
ext x
[GOAL]
case h
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
x : f α
⊢ (fun {α β} e => Functor.map ↑e) (k.trans h) x =
    ((fun {α β} e => Functor.map ↑e) h ∘ (fun {α β} e => Functor.map ↑e) k) x
[PROOFSTEP]
apply LawfulFunctor.comp_map k h x
[GOAL]
f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (↑e₁ x) = pure (↑e₂ x)
[PROOFSTEP]
simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x)
