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

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

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

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

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

State before:
case h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
head✝ : x✝
tail✝ : List x✝
ih : length tail✝ = List.length tail✝
⊢ length tail✝ + 1 = List.length tail✝ + 1
Tactic:
exact congrArg _ ih
State after:
no goals