Theorem: hcat_spec2 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {sch₁ sch₂ : Schema} (t₁ : Table sch₁) (t₂ : Table sch₂), nrows t₁ = nrows t₂ → nrows (hcat t₁ t₂) = nrows t₁
Tactic:
intros sch₁ sch₂ t₁ t₂ h
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : nrows t₁ = nrows t₂
⊢ nrows (hcat t₁ t₂) = nrows t₁

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : nrows t₁ = nrows t₂
⊢ nrows (hcat t₁ t₂) = nrows t₁
Tactic:
simp only [nrows, hcat, Schema.length_eq_List_length] at *
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.map (fun x => Row.append x.fst x.snd) (List.zip t₁.rows t₂.rows)) = List.length t₁.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.map (fun x => Row.append x.fst x.snd) (List.zip t₁.rows t₂.rows)) = List.length t₁.rows
Tactic:
rw [List.length_map]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.zip t₁.rows t₂.rows) = List.length t₁.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.zip t₁.rows t₂.rows) = List.length t₁.rows
Tactic:
apply List.zip_length_eq_of_length_eq _ _ h
State after:
no goals