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

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ ∀ (sch : Schema) (nm : η), HasName nm sch → nm ∈ map Prod.fst sch
Tactic:
intro sch nm h
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
h : HasName nm sch
⊢ nm ∈ map Prod.fst sch

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
h : HasName nm sch
⊢ nm ∈ map Prod.fst sch
Tactic:
induction h with
| hd =>
  apply List.Mem.head
| tl _ ih =>
  apply List.Mem.tail
  apply ih
State after:
no goals

State before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ c✝ ∈ map Prod.fst ((c✝, τ✝) :: rs✝)
Tactic:
apply List.Mem.head
State after:
no goals

State before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
a✝ : HasName c✝ rs✝
ih : c✝ ∈ map Prod.fst rs✝
⊢ c✝ ∈ map Prod.fst (r✝ :: rs✝)
Tactic:
apply List.Mem.tail
State after:
case tl.a
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
a✝ : HasName c✝ rs✝
ih : c✝ ∈ map Prod.fst rs✝
⊢ List.Mem c✝ (map Prod.fst rs✝)

State before:
case tl.a
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
a✝ : HasName c✝ rs✝
ih : c✝ ∈ map Prod.fst rs✝
⊢ List.Mem c✝ (map Prod.fst rs✝)
Tactic:
apply ih
State after:
no goals