Theorem: Schema.map_eq_List_map (Table/SchemaFunctions.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ @map = @List.map
Tactic:
funext _ _ _ xs
State after:
case h.h.h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
xs : List x✝²
⊢ map x✝ xs = List.map x✝ xs

State before:
case h.h.h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
xs : List x✝²
⊢ map x✝ xs = List.map x✝ xs
Tactic:
induction xs with
| nil => rfl
| cons _ _ ih =>
  simp only [map, List.map]
  exact congrArg _ ih
State after:
no goals

State before:
case h.h.h.h.nil
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
⊢ map x✝ [] = List.map x✝ []
Tactic:
rfl
State after:
no goals

State before:
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ map x✝ (head✝ :: tail✝) = List.map x✝ (head✝ :: tail✝)
Tactic:
simp only [map, List.map]
State after:
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ x✝ head✝ :: map x✝ tail✝ = x✝ head✝ :: List.map x✝ tail✝

State before:
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ x✝ head✝ :: map x✝ tail✝ = x✝ head✝ :: List.map x✝ tail✝
Tactic:
exact congrArg _ ih
State after:
no goals