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

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ ∀ (s t : Schema) (c : η) (h : HasName c s),
    lookup s { fst := c, snd := h } = lookup (append s t) { fst := c, snd := hasNameOfAppend h }
Tactic:
intros s t c h
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
h : HasName c s
⊢ lookup s { fst := c, snd := h } = lookup (append s t) { fst := c, snd := hasNameOfAppend h }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
h : HasName c s
⊢ lookup s { fst := c, snd := h } = lookup (append s t) { fst := c, snd := hasNameOfAppend h }
Tactic:
induction h with
| hd =>
  simp only [Schema.hasNameOfAppend]
  rw [Schema.lookup_eq_1, Schema.lookup_eq_1]
| tl h' ih =>
  simp only [Schema.hasNameOfAppend]
  rw [Schema.lookup_eq_2, Schema.lookup_eq_2]
  exact ih
State after:
no goals

State before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    lookup (append ((c✝, τ✝) :: rs✝) t) { fst := c✝, snd := hasNameOfAppend HasName.hd }
Tactic:
simp only [Schema.hasNameOfAppend]
State after:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    lookup (append ((c✝, τ✝) :: rs✝) t) { fst := c✝, snd := HasName.hd }

State before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    lookup (append ((c✝, τ✝) :: rs✝) t) { fst := c✝, snd := HasName.hd }
Tactic:
rw [Schema.lookup_eq_1, Schema.lookup_eq_1]
State after:
no goals

State before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h' } =
    lookup (append (r✝ :: rs✝) t) { fst := c✝, snd := hasNameOfAppend (HasName.tl h') }
Tactic:
simp only [Schema.hasNameOfAppend]
State after:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h' } =
    lookup (append (r✝ :: rs✝) t) { fst := c✝, snd := HasName.tl (hasNameOfAppend h') }

State before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h' } =
    lookup (append (r✝ :: rs✝) t) { fst := c✝, snd := HasName.tl (hasNameOfAppend h') }
Tactic:
rw [Schema.lookup_eq_2, Schema.lookup_eq_2]
State after:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }

State before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
Tactic:
exact ih
State after:
no goals