Theorem: nrows_groupBySubtractive (Table/Demo.lean)

State before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
⊢ nrows (groupBySubtractive t c) ≤ nrows t
Tactic:
have h_gbs := groupBySubtractive_spec7 t c hc
State after:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ nrows (groupBySubtractive t c) ≤ nrows t

State before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ nrows (groupBySubtractive t c) ≤ nrows t
Tactic:
rw [h_gbs]
State after:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ nrows t

State before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ nrows t
Tactic:
rw [←getColumn2_spec2 t c hc]
State after:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ List.length (getColumn2 t c)

State before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ List.length (getColumn2 t c)
Tactic:
apply List.length_unique_le
State after:
no goals