Theorem: List.map_comp (Moncalc/Data/List/Misc.lean)

State before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ ∀ {as : List α}, map (g ∘ f) as = map g (map f as)
Tactic:
intro as
State after:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
as : List α
⊢ map (g ∘ f) as = map g (map f as)

State before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
as : List α
⊢ map (g ∘ f) as = map g (map f as)
Tactic:
induction as
State after:
case nil
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map (g ∘ f) [] = map g (map f [])

case cons
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : map (g ∘ f) tail✝ = map g (map f tail✝)
⊢ map (g ∘ f) (head✝ :: tail✝) = map g (map f (head✝ :: tail✝))

State before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map (g ∘ f) [] = map g (map f [])
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ map (g ∘ f) (a :: as) = map g (map f (a :: as))
Tactic:
case cons a as h_ind =>
  dsimp [map]
  rw [h_ind]
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map (g ∘ f) [] = map g (map f [])
Tactic:
rfl
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ map (g ∘ f) (a :: as) = map g (map f (a :: as))
Tactic:
dsimp [map]
State after:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ g (f a) :: map (g ∘ f) as = g (f a) :: map g (map f as)

State before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ g (f a) :: map (g ∘ f) as = g (f a) :: map g (map f as)
Tactic:
rw [h_ind]
State after:
no goals