Theorem: crossJoin_spec2 (Table/Proofs.lean)

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

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ nrows (crossJoin t₁ t₂) = nrows t₁ * nrows t₂
Tactic:
simp only [nrows, crossJoin, List.length_map, Schema.length_eq_List_length]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ List.length (List.prod t₁.rows t₂.rows) = List.length t₁.rows * List.length t₂.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ List.length (List.prod t₁.rows t₂.rows) = List.length t₁.rows * List.length t₂.rows
Tactic:
apply List.length_prod
State after:
no goals