internlm/Lean-Github huggingface dataset:
Theorem: Schema.hasNameEqHeadOrTail_inl
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
eqt : hasNameEqHeadOrTail h ≡ Sum.inl (EqT.refl nm)
⊢ h = HasName.hd
Tactic:
simp only [hasNameEqHeadOrTail] at eqt
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
eqt :
  (match nm, hs, h with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ h = HasName.hd
Theorem: Schema.hasNameEqHeadOrTail_inl
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
eqt :
  (match nm, hs, h with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ h = HasName.hd
Tactic:
cases h
Proof state after:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
eqt :
  (match nm, hs, HasName.hd with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.hd = HasName.hd

case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.tl a✝ = HasName.hd
Theorem: Schema.hasNameEqHeadOrTail_inl
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
eqt :
  (match nm, hs, HasName.hd with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.hd = HasName.hd

case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.tl a✝ = HasName.hd
Tactic:
. rfl
Proof state after:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.tl a✝ = HasName.hd
Theorem: Schema.hasNameEqHeadOrTail_inl
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.tl a✝ = HasName.hd
Tactic:
. contradiction
Proof state after:
no goals
Theorem: Schema.hasNameEqHeadOrTail_inl
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
eqt :
  (match nm, hs, HasName.hd with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.hd = HasName.hd
Tactic:
rfl
Proof state after:
no goals
Theorem: Schema.hasNameEqHeadOrTail_inl
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(nm), x, HasName.hd => Sum.inl (EqT.refl nm)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inl (EqT.refl nm)
⊢ HasName.tl a✝ = HasName.hd
Tactic:
contradiction
Proof state after:
no goals
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h✝ : Header
hs : List Header
h : HasName nm (h✝ :: hs)
htl : HasName nm hs
⊢ hasNameEqHeadOrTail h ≡ Sum.inr htl → h = HasName.tl htl
Tactic:
intro eqt
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h✝ : Header
hs : List Header
h : HasName nm (h✝ :: hs)
htl : HasName nm hs
eqt : hasNameEqHeadOrTail h ≡ Sum.inr htl
⊢ h = HasName.tl htl
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h✝ : Header
hs : List Header
h : HasName nm (h✝ :: hs)
htl : HasName nm hs
eqt : hasNameEqHeadOrTail h ≡ Sum.inr htl
⊢ h = HasName.tl htl
Tactic:
simp only [hasNameEqHeadOrTail] at eqt
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h✝ : Header
hs : List Header
h : HasName nm (h✝ :: hs)
htl : HasName nm hs
eqt :
  (match nm, hs, h with
    | .(h✝.fst), x, HasName.hd => Sum.inl (EqT.refl h✝.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ h = HasName.tl htl
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h✝ : Header
hs : List Header
h : HasName nm (h✝ :: hs)
htl : HasName nm hs
eqt :
  (match nm, hs, h with
    | .(h✝.fst), x, HasName.hd => Sum.inl (EqT.refl h✝.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ h = HasName.tl htl
Tactic:
cases h
Proof state after:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
hs : List Header
htl : HasName nm hs
τ✝ : Type u_2
eqt :
  (match nm, hs, HasName.hd with
    | .((nm, τ✝).fst), x, HasName.hd => Sum.inl (EqT.refl (nm, τ✝).fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.hd = HasName.tl htl

case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(h.fst), x, HasName.hd => Sum.inl (EqT.refl h.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
hs : List Header
htl : HasName nm hs
τ✝ : Type u_2
eqt :
  (match nm, hs, HasName.hd with
    | .((nm, τ✝).fst), x, HasName.hd => Sum.inl (EqT.refl (nm, τ✝).fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.hd = HasName.tl htl

case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(h.fst), x, HasName.hd => Sum.inl (EqT.refl h.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
Tactic:
. contradiction
Proof state after:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(h.fst), x, HasName.hd => Sum.inl (EqT.refl h.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(h.fst), x, HasName.hd => Sum.inl (EqT.refl h.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
Tactic:
. simp only at eqt
  cases eqt
  rfl
Proof state after:
no goals
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
hs : List Header
htl : HasName nm hs
τ✝ : Type u_2
eqt :
  (match nm, hs, HasName.hd with
    | .((nm, τ✝).fst), x, HasName.hd => Sum.inl (EqT.refl (nm, τ✝).fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.hd = HasName.tl htl
Tactic:
contradiction
Proof state after:
no goals
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt :
  (match nm, hs, HasName.tl a✝ with
    | .(h.fst), x, HasName.hd => Sum.inl (EqT.refl h.fst)
    | x, x_1, HasName.tl htl => Sum.inr htl) ≡
    Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
Tactic:
simp only at eqt
Proof state after:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt : Sum.inr a✝ ≡ Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl a✝ : HasName nm hs
eqt : Sum.inr a✝ ≡ Sum.inr htl
⊢ HasName.tl a✝ = HasName.tl htl
Tactic:
cases eqt
Proof state after:
case tl.refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl : HasName nm hs
⊢ HasName.tl htl = HasName.tl htl
Theorem: Schema.hasNameEqHeadOrTail_inr
Proof state before:
case tl.refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
h : Header
hs : List Header
htl : HasName nm hs
⊢ HasName.tl htl = HasName.tl htl
Tactic:
rfl
Proof state after:
no goals
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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]
Proof 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 }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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
Proof 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 }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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]
Proof state after:
no goals
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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]
Proof 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) }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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]
Proof 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 }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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
Proof state after:
no goals
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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]
Proof 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 }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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)
Proof 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 }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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]
Proof 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 }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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
Proof state after:
no goals
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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
Proof 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 }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof 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)
Proof 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 }