Theorem: sortByColumns_spec1 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)), nrows (sortByColumns t hs) = nrows t
Tactic:
intros t hs
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows (sortByColumns t hs) = nrows t

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows (sortByColumns t hs) = nrows t
Tactic:
simp only [nrows, sortByColumns]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ Schema.length (List.foldr (fun ohdr acc => tsort acc ohdr.fst.fst true) t hs).rows = Schema.length t.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ Schema.length (List.foldr (fun ohdr acc => tsort acc ohdr.fst.fst true) t hs).rows = Schema.length t.rows
Tactic:
apply List.foldr_invariant (λ x => nrows x = nrows t)
State after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows t = nrows t

case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t

State before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows t = nrows t

case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t
Tactic:
. rfl
State after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t

State before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t
Tactic:
. intros x acc h
  rw [←h]
  apply tsort_spec1 (inst := x.snd.snd)
State after:
no goals

State before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows t = nrows t
Tactic:
rfl
State after:
no goals

State before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t
Tactic:
intros x acc h
State after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows t

State before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows t
Tactic:
rw [←h]
State after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows acc

State before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows acc
Tactic:
apply tsort_spec1 (inst := x.snd.snd)
State after:
no goals