Theorem: dropColumn_spec2_unique (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ Schema.Unique sch →
    ∀ (t : Table sch) (c : η) (hc : Schema.HasName c sch), header (dropColumn t c) = List.removeAllEq (header t) [c]
Tactic:
intro hsch t c hc
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ header (dropColumn t c) = List.removeAllEq (header t) [c]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ header (dropColumn t c) = List.removeAllEq (header t) [c]
Tactic:
simp only [List.removeAllEq, header]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)
Tactic:
unfold Schema.Unique at hsch
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : List.Unique (Schema.names sch)
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : List.Unique (Schema.names sch)
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)
Tactic:
induction hc with
| @hd nm s' τ =>
  simp only [List.filter, List.notElem, List.elem]
  cases hsch with | cons hnmem hu =>
  simp only at hnmem
  have : (decide (nm ∉ [nm])) = false :=
    by simp only [decide_not, List.mem_singleton_iff, decide_True,
                  decide_False, not]
  rw [this]
  simp only
  simp only [Schema.names, List.map]
  have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
          = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
  rw [this]
  rw [List.removeAllEq_singleton_nonelem_eq]
  exact hnmem
| @tl hdr nm s' h ih =>
  simp only [Schema.names, List.map]
  cases hdr with | mk nm₁ τ₁ =>
  cases Decidable.em (nm₁ = nm) with
  | inl heq =>
    rw [heq] at hsch
    cases hsch with | cons hnmem hu =>
    simp only at hnmem
    have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
    contradiction
  | inr hneq =>
    rw [←List.removeAllEq]
    rw [List.removeAllEq_singleton_hd_neq]
    . congr
      apply ih
      . cases hsch; assumption
      . exact Table.mk []
    . exact hneq
State after:
no goals

State before:
case hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names ((nm, τ) :: s'))
Tactic:
simp only [List.filter, List.notElem, List.elem]
State after:
case hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')

State before:
case hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
cases hsch with | cons hnmem hu =>
simp only at hnmem
have : (decide (nm ∉ [nm])) = false :=
  by simp only [decide_not, List.mem_singleton_iff, decide_True,
                decide_False, not]
rw [this]
simp only
simp only [Schema.names, List.map]
have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
        = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
rw [this]
rw [List.removeAllEq_singleton_nonelem_eq]
exact hnmem
State after:
no goals

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬(nm, τ).fst ∈ List.map Prod.fst s'
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
simp only at hnmem
State after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
have : (decide (nm ∉ [nm])) = false :=
  by simp only [decide_not, List.mem_singleton_iff, decide_True,
                decide_False, not]
State after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
rw [this]
State after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match false with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match false with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
simp only
State after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
simp only [Schema.names, List.map]
State after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
        = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
State after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
rw [this]
State after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) = List.removeAllEq (List.map Prod.fst s') [nm]

State before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) = List.removeAllEq (List.map Prod.fst s') [nm]
Tactic:
rw [List.removeAllEq_singleton_nonelem_eq]
State after:
case hd.cons.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ ¬nm ∈ List.map Prod.fst s'

State before:
case hd.cons.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ ¬nm ∈ List.map Prod.fst s'
Tactic:
exact hnmem
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (decide ¬nm ∈ [nm]) = false
Tactic:
simp only [decide_not, List.mem_singleton_iff, decide_True,
           decide_False, not]
State after:
no goals

State before:
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ Schema.names (Schema.removeName (hdr :: s') (Schema.HasName.tl h)) =
    List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names (hdr :: s'))
Tactic:
simp only [Schema.names, List.map]
State after:
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ hdr.fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) (hdr.fst :: List.map Prod.fst s')

State before:
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ hdr.fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) (hdr.fst :: List.map Prod.fst s')
Tactic:
cases hdr with | mk nm₁ τ₁ =>
cases Decidable.em (nm₁ = nm) with
| inl heq =>
  rw [heq] at hsch
  cases hsch with | cons hnmem hu =>
  simp only at hnmem
  have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
  contradiction
| inr hneq =>
  rw [←List.removeAllEq]
  rw [List.removeAllEq_singleton_hd_neq]
  . congr
    apply ih
    . cases hsch; assumption
    . exact Table.mk []
  . exact hneq
State after:
no goals

State before:
case tl.mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
cases Decidable.em (nm₁ = nm) with
| inl heq =>
  rw [heq] at hsch
  cases hsch with | cons hnmem hu =>
  simp only at hnmem
  have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
  contradiction
| inr hneq =>
  rw [←List.removeAllEq]
  rw [List.removeAllEq_singleton_hd_neq]
  . congr
    apply ih
    . cases hsch; assumption
    . exact Table.mk []
  . exact hneq
State after:
no goals

State before:
case tl.mk.inl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
rw [heq] at hsch
State after:
case tl.mk.inl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')

State before:
case tl.mk.inl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
cases hsch with | cons hnmem hu =>
simp only at hnmem
have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
contradiction
State after:
no goals

State before:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬(nm, τ₁).fst ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
simp only at hnmem
State after:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')

State before:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
State after:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')

State before:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
contradiction
State after:
no goals

State before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
rw [←List.removeAllEq]
State after:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.removeAllEq ((nm₁, τ₁).fst :: List.map Prod.fst s') [nm]

State before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.removeAllEq ((nm₁, τ₁).fst :: List.map Prod.fst s') [nm]
Tactic:
rw [List.removeAllEq_singleton_hd_neq]
State after:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    (nm₁, τ₁).fst :: List.removeAllEq (List.map Prod.fst s') [nm]

case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm

State before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    (nm₁, τ₁).fst :: List.removeAllEq (List.map Prod.fst s') [nm]

case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Tactic:
. congr
  apply ih
  . cases hsch; assumption
  . exact Table.mk []
State after:
case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm

State before:
case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Tactic:
. exact hneq
State after:
no goals

State before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    (nm₁, τ₁).fst :: List.removeAllEq (List.map Prod.fst s') [nm]
Tactic:
congr
State after:
case tl.mk.inr.e_tail
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.map Prod.fst (Schema.removeName s' h) = List.removeAllEq (List.map Prod.fst s') [nm]

State before:
case tl.mk.inr.e_tail
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.map Prod.fst (Schema.removeName s' h) = List.removeAllEq (List.map Prod.fst s') [nm]
Tactic:
apply ih
State after:
case tl.mk.inr.e_tail.hsch
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.Unique (Schema.names s')

case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'

State before:
case tl.mk.inr.e_tail.hsch
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.Unique (Schema.names s')

case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Tactic:
. cases hsch; assumption
State after:
case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'

State before:
case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Tactic:
. exact Table.mk []
State after:
no goals

State before:
case tl.mk.inr.e_tail.hsch
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.Unique (Schema.names s')
Tactic:
cases hsch
State after:
case tl.mk.inr.e_tail.hsch.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
a✝¹ : List.Unique (List.map Prod.fst s')
a✝ : ¬(nm₁, τ₁).fst ∈ List.map Prod.fst s'
⊢ List.Unique (Schema.names s')

State before:
case tl.mk.inr.e_tail.hsch.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
a✝¹ : List.Unique (List.map Prod.fst s')
a✝ : ¬(nm₁, τ₁).fst ∈ List.map Prod.fst s'
⊢ List.Unique (Schema.names s')
Tactic:
assumption
State after:
no goals

State before:
case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Tactic:
exact Table.mk []
State after:
no goals

State before:
case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Tactic:
exact hneq
State after:
no goals