[GOAL]
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m', mapConst := mc' }
[PROOFSTEP]
cases show @m = @m' by funext α β f x; apply H
[GOAL]
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ m = m'
[PROOFSTEP]
funext α β f x
[GOAL]
case h.h.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
f : α → β
x : F α
⊢ m f x = m' f x
[PROOFSTEP]
apply H
[GOAL]
case refl
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m, mapConst := mc' }
[PROOFSTEP]
congr
[GOAL]
case refl.e_mapConst
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ mc = mc'
[PROOFSTEP]
funext α β
[GOAL]
case refl.e_mapConst.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
⊢ mc = mc'
[PROOFSTEP]
have E1 := @map_const _ ⟨@m, @mc⟩ H1
[GOAL]
case refl.e_mapConst.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, mapConst = map ∘ Function.const β
⊢ mc = mc'
[PROOFSTEP]
have E2 := @map_const _ ⟨@m, @mc'⟩ H2
[GOAL]
case refl.e_mapConst.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, mapConst = map ∘ Function.const β
E2 : ∀ {α β : Type u_1}, mapConst = map ∘ Function.const β
⊢ mc = mc'
[PROOFSTEP]
exact E1.trans E2.symm
[GOAL]
γ : Type ?u.2497
⊢ LawfulFunctor (Const γ)
[PROOFSTEP]
constructor
[GOAL]
case map_const
γ : Type ?u.2497
⊢ ∀ {α β : Type ?u.2498}, mapConst = map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case id_map
γ : Type ?u.2497
⊢ ∀ {α : Type ?u.2498} (x : Const γ α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case comp_map
γ : Type ?u.2497
⊢ ∀ {α β γ_1 : Type ?u.2498} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case map_const
γ : Type ?u.2497
α✝ β✝ : Type ?u.2498
⊢ mapConst = map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
case id_map
γ : Type ?u.2497
α✝ : Type ?u.2498
x✝ : Const γ α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case comp_map
γ : Type ?u.2497
α✝ β✝ γ✝ : Type ?u.2498
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const γ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x
[PROOFSTEP]
simp [Comp.map, Functor.map_id]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
x : F (G α)
⊢ mk (mk x) = mk x
[PROOFSTEP]
rfl
  -- porting note: `rfl` wasn't needed in mathlib3
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
g' : α → β
h : β → γ
x : F (G α)
⊢ Comp.map (h ∘ g') (mk x) = Comp.map h (Comp.map g' (mk x))
[PROOFSTEP]
simp [Comp.map, Comp.mk, Functor.map_comp_map, functor_norm]
  -- porting note: `Comp.mk` wasn't needed in mathlib3
