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

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := 0, isLt := hlt } :: ns)) { fst := snm, snd := HasName.hd } =
    lookupType ((snm, sτ) :: sch) { fst := snm, snd := hasNameOfNthsHasName HasName.hd }
Tactic:
simp only [Schema.lookupType]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
⊢ sτ = lookupType ((snm, sτ) :: sch) { fst := snm, snd := hasNameOfNthsHasName HasName.hd }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
⊢ sτ = lookupType ((snm, sτ) :: sch) { fst := snm, snd := hasNameOfNthsHasName HasName.hd }
Tactic:
unfold Schema.hasNameOfNthsHasName
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
⊢ sτ =
    lookupType ((snm, sτ) :: sch)
      { fst := snm,
        snd :=
          match snm, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := 0, isLt := hlt }.val
                  (_ : { val := 0, isLt := hlt }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := 0, isLt := hlt }.val
                      (_ : { val := 0, isLt := hlt }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := 0, isLt := hlt }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
⊢ sτ =
    lookupType ((snm, sτ) :: sch)
      { fst := snm,
        snd :=
          match snm, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := 0, isLt := hlt }.val
                  (_ : { val := 0, isLt := hlt }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := 0, isLt := hlt }.val
                      (_ : { val := 0, isLt := hlt }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := 0, isLt := hlt }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }
Tactic:
simp only [Schema.hasNameEqHeadOrTail, Schema.hasNthName, Schema.lookupType]
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
h : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := 0, isLt := hlt } :: ns)) { fst := nm, snd := HasName.tl h } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName (HasName.tl h) }
Tactic:
conv =>
  lhs
  simp only [Schema.nths, Schema.map, Schema.lookupType]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
h : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := h } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName (HasName.tl h) }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
h : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := h } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName (HasName.tl h) }
Tactic:
conv =>
  rhs
  unfold Schema.hasNameOfNthsHasName
  simp only [Schema.hasNameEqHeadOrTail]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
h : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := h } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName h }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
hlt : 0 < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
h : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := h } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName h }
Tactic:
apply lookupType_nths_eq_lookupType
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns)) { fst := nm, snd := hnths } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hnths }
Tactic:
conv =>
  rhs
  unfold Schema.hasNameOfNthsHasName
  simp only [h]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns)) { fst := nm, snd := hnths } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hhnm }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns)) { fst := nm, snd := hnths } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hhnm }
Tactic:
have htoprove : hnths = .tl hhnm :=
  Schema.hasNameEqHeadOrTail_inr _ _ (EqT.ofEq h)
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
htoprove : hnths = HasName.tl hhnm
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns)) { fst := nm, snd := hnths } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hhnm }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
htoprove : hnths = HasName.tl hhnm
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns)) { fst := nm, snd := hnths } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hhnm }
Tactic:
conv =>
  lhs
  simp only [Schema.nths, Schema.map, htoprove, Schema.lookupType]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
htoprove : hnths = HasName.tl hhnm
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := hhnm } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hhnm }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
hhnm : HasName nm (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
h : hasNameEqHeadOrTail hnths = Sum.inr hhnm
htoprove : hnths = HasName.tl hhnm
⊢ lookupType (map (fun n => nth ((snm, sτ) :: sch) n.val (_ : n.val < length ((snm, sτ) :: sch))) ns)
      { fst := nm, snd := hhnm } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hhnm }
Tactic:
apply lookupType_nths_eq_lookupType
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
nm : η
hnths : HasName nm (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
heqt : (nth sch n (_ : Nat.succ n ≤ length sch)).fst ≡ nm
h : hasNameEqHeadOrTail hnths = Sum.inl heqt
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns)) { fst := nm, snd := hnths } =
    lookupType ((snm, sτ) :: sch) { fst := nm, snd := hasNameOfNthsHasName hnths }
Tactic:
cases heqt
State after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hnths } =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName hnths }

State before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hnths } =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName hnths }
Tactic:
have htoprove : hnths = .hd :=
  Schema.hasNameEqHeadOrTail_inl hnths (EqT.ofEq h)
State after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hnths } =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName hnths }

State before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hnths } =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName hnths }
Tactic:
simp only [Schema.nths, Schema.map, Schema.lookupType, htoprove]
State after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName HasName.hd }

State before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName HasName.hd }
Tactic:
unfold Schema.hasNameOfNthsHasName
State after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd :=
          match (nth sch n (_ : Nat.succ n ≤ length sch)).fst, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                  (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                      (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := Nat.succ n, isLt := pf }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }

State before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd :=
          match (nth sch n (_ : Nat.succ n ≤ length sch)).fst, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                  (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                      (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := Nat.succ n, isLt := pf }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }
Tactic:
simp only [Schema.hasNameEqHeadOrTail, Schema.hasNthName, Schema.lookupType]
State after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType sch
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd := hasNthName { val := n, isLt := (_ : n < length sch) } }

State before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType sch
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd := hasNthName { val := n, isLt := (_ : n < length sch) } }
Tactic:
apply Schema.lookup_nth
State after:
no goals