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

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
⊢ hasNameEqHeadOrTail h ≡ Sum.inl (EqT.refl nm) → h = HasName.hd
Tactic:
intro eqt
State after:
η : 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

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

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

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

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

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

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