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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals