Theorem: orderBy_spec3 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cmps : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))), nrows (orderBy t cmps) = nrows t
Tactic:
intro t _
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ nrows (orderBy t cmps✝) = nrows t

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ nrows (orderBy t cmps✝) = nrows t
Tactic:
simp only [nrows, orderBy, Schema.length_eq_List_length]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ List.length
      (List.mergeSortWith
        (fun r₁ r₂ =>
          match List.find? (fun x => !Prod.snd x.2 (Prod.fst x.2 r₁) (Prod.fst x.2 r₂)) cmps✝ with
          | none => Ordering.lt
          | x => Ordering.gt)
        t.rows) =
    List.length t.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ List.length
      (List.mergeSortWith
        (fun r₁ r₂ =>
          match List.find? (fun x => !Prod.snd x.2 (Prod.fst x.2 r₁) (Prod.fst x.2 r₂)) cmps✝ with
          | none => Ordering.lt
          | x => Ordering.gt)
        t.rows) =
    List.length t.rows
Tactic:
exact List.length_mergeSortWith _ t.rows
State after:
no goals