Theorem: fillna_spec2 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
⊢ ∀ (t : Table sch) (c : η) (v : τ) (hc : Schema.HasCol (c, τ) sch), nrows (fillna t c v) = nrows t
Tactic:
intros
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ nrows (fillna t✝ c✝ v✝) = nrows t✝

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ nrows (fillna t✝ c✝ v✝) = nrows t✝
Tactic:
simp only [nrows, fillna, Schema.length_eq_List_length]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ List.length
      (updateWithoutRetyping [{ fst := (c✝, τ), snd := hc✝ }] t✝ fun r =>
          match Row.getCell r hc✝ with
          | Cell.emp => Row.singleValue v✝
          | Cell.val vOld => Row.singleValue vOld).rows =
    List.length t✝.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ List.length
      (updateWithoutRetyping [{ fst := (c✝, τ), snd := hc✝ }] t✝ fun r =>
          match Row.getCell r hc✝ with
          | Cell.emp => Row.singleValue v✝
          | Cell.val vOld => Row.singleValue vOld).rows =
    List.length t✝.rows
Tactic:
apply List.length_map
State after:
no goals