internlm/Lean-Github huggingface dataset:
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates (getColumn2 (groupByRetentive t c) "key")
Tactic:
simp only [groupByRetentive, groupBy, getColumn2]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun r => getValue r "key")
      (List.map
        (fun klv =>
          Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
        (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows))))
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun r => getValue r "key")
      (List.map
        (fun klv =>
          Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
        (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows))))
Tactic:
rw [List.map_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => getValue r "key") ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
      (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows)))
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => getValue r "key") ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
      (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows)))
Tactic:
simp only [Function.comp, getValue]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => Cell.toOption (Row.getCell r Schema.HasCol.hd)) ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => Cell.toOption (Row.getCell r Schema.HasCol.hd)) ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
conv =>
  rhs
  lhs
  apply funext (g := _) _
  apply (λ x => Option.map ULift.up x.fst)
  apply (λ x => Cell.toOption_fromOption _)
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun x => Option.map ULift.up x.fst)
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun x => Option.map ULift.up x.fst)
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
conv =>
  rhs
  lhs
  apply funext (g := _) _
  apply (λ x => Option.map ULift.up ∘ Prod.fst)
  apply (λ x => rfl)
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map ((fun x => Option.map ULift.up ∘ Prod.fst) (Row sch))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map ((fun x => Option.map ULift.up ∘ Prod.fst) (Row sch))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
rw [←List.map_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (Option.map ULift.up)
      (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows))))
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (Option.map ULift.up)
      (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows))))
Tactic:
apply List.no_dups_map_injective
Proof state after:
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ Function.injective (Option.map ULift.up)

case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupByRetentive_spec4
Proof state before:
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ Function.injective (Option.map ULift.up)

case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
. intros x y hxy
  cases x
  . cases y
    . rfl
    . contradiction
  . cases y
    . contradiction
    . cases hxy; rfl
Proof state after:
case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupByRetentive_spec4
Proof state before:
case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
. apply List.groupByKey_fsts_no_duplicates
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ Function.injective (Option.map ULift.up)
Tactic:
intros x y hxy
Proof state after:
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
x y : Option τ
hxy : Option.map ULift.up x = Option.map ULift.up y
⊢ x = y
Theorem: groupByRetentive_spec4
Proof state before:
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
x y : Option τ
hxy : Option.map ULift.up x = Option.map ULift.up y
⊢ x = y
Tactic:
cases x
Proof state after:
case hf.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
hxy : Option.map ULift.up none = Option.map ULift.up y
⊢ none = y

case hf.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up y
⊢ some val✝ = y
Theorem: groupByRetentive_spec4
Proof state before:
case hf.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
hxy : Option.map ULift.up none = Option.map ULift.up y
⊢ none = y

case hf.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up y
⊢ some val✝ = y
Tactic:
. cases y
  . rfl
  . contradiction
Proof state after:
case hf.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up y
⊢ some val✝ = y
Theorem: groupByRetentive_spec4
Proof state before:
case hf.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up y
⊢ some val✝ = y
Tactic:
. cases y
  . contradiction
  . cases hxy; rfl
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hf.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
hxy : Option.map ULift.up none = Option.map ULift.up y
⊢ none = y
Tactic:
cases y
Proof state after:
case hf.none.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
hxy : Option.map ULift.up none = Option.map ULift.up none
⊢ none = none

case hf.none.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up none = Option.map ULift.up (some val✝)
⊢ none = some val✝
Theorem: groupByRetentive_spec4
Proof state before:
case hf.none.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
hxy : Option.map ULift.up none = Option.map ULift.up none
⊢ none = none

case hf.none.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up none = Option.map ULift.up (some val✝)
⊢ none = some val✝
Tactic:
. rfl
Proof state after:
case hf.none.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up none = Option.map ULift.up (some val✝)
⊢ none = some val✝
Theorem: groupByRetentive_spec4
Proof state before:
case hf.none.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up none = Option.map ULift.up (some val✝)
⊢ none = some val✝
Tactic:
. contradiction
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hf.none.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
hxy : Option.map ULift.up none = Option.map ULift.up none
⊢ none = none
Tactic:
rfl
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hf.none.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up none = Option.map ULift.up (some val✝)
⊢ none = some val✝
Tactic:
contradiction
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hf.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
y : Option τ
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up y
⊢ some val✝ = y
Tactic:
cases y
Proof state after:
case hf.some.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up none
⊢ some val✝ = none

case hf.some.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝¹ val✝ : τ
hxy : Option.map ULift.up (some val✝¹) = Option.map ULift.up (some val✝)
⊢ some val✝¹ = some val✝
Theorem: groupByRetentive_spec4
Proof state before:
case hf.some.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up none
⊢ some val✝ = none

case hf.some.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝¹ val✝ : τ
hxy : Option.map ULift.up (some val✝¹) = Option.map ULift.up (some val✝)
⊢ some val✝¹ = some val✝
Tactic:
. contradiction
Proof state after:
case hf.some.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝¹ val✝ : τ
hxy : Option.map ULift.up (some val✝¹) = Option.map ULift.up (some val✝)
⊢ some val✝¹ = some val✝
Theorem: groupByRetentive_spec4
Proof state before:
case hf.some.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝¹ val✝ : τ
hxy : Option.map ULift.up (some val✝¹) = Option.map ULift.up (some val✝)
⊢ some val✝¹ = some val✝
Tactic:
. cases hxy; rfl
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hf.some.none
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
hxy : Option.map ULift.up (some val✝) = Option.map ULift.up none
⊢ some val✝ = none
Tactic:
contradiction
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hf.some.some
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝¹ val✝ : τ
hxy : Option.map ULift.up (some val✝¹) = Option.map ULift.up (some val✝)
⊢ some val✝¹ = some val✝
Tactic:
cases hxy
Proof state after:
case hf.some.some.refl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
⊢ some val✝ = some val✝
Theorem: groupByRetentive_spec4
Proof state before:
case hf.some.some.refl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
val✝ : τ
⊢ some val✝ = some val✝
Tactic:
rfl
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
apply List.groupByKey_fsts_no_duplicates
Proof state after:
no goals
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
⊢ ∀ (t : Table sch) (c : η) (hc : Schema.HasCol (c, τ) sch),
    List.NoDuplicates (getColumn2 (groupBySubtractive t c) "key")
Tactic:
intros t c hc
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates (getColumn2 (groupBySubtractive t c) "key")
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates (getColumn2 (groupBySubtractive t c) "key")
Tactic:
simp only [groupBySubtractive, groupBy, getColumn2]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun r => getValue r "key")
      (List.map
        (fun klv =>
          Row.cons (Cell.fromOption (Option.map ULift.up klv.fst))
            (Row.cons (Cell.val { rows := List.map (fun r => Row.removeColumn (Schema.colImpliesName hc) r) klv.snd })
              Row.nil))
        (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows))))
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun r => getValue r "key")
      (List.map
        (fun klv =>
          Row.cons (Cell.fromOption (Option.map ULift.up klv.fst))
            (Row.cons (Cell.val { rows := List.map (fun r => Row.removeColumn (Schema.colImpliesName hc) r) klv.snd })
              Row.nil))
        (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows))))
Tactic:
rw [List.map_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => getValue r "key") ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst))
          (Row.cons (Cell.val { rows := List.map (fun r => Row.removeColumn (Schema.colImpliesName hc) r) klv.snd })
            Row.nil))
      (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows)))
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => getValue r "key") ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst))
          (Row.cons (Cell.val { rows := List.map (fun r => Row.removeColumn (Schema.colImpliesName hc) r) klv.snd })
            Row.nil))
      (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows)))
Tactic:
simp only [Function.comp, getValue]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => Cell.toOption (Row.getCell r Schema.HasCol.hd)) ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst))
          (Row.cons (Cell.val { rows := List.map (fun r => Row.removeColumn (Schema.colImpliesName hc) r) klv.snd })
            Row.nil))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => Cell.toOption (Row.getCell r Schema.HasCol.hd)) ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst))
          (Row.cons (Cell.val { rows := List.map (fun r => Row.removeColumn (Schema.colImpliesName hc) r) klv.snd })
            Row.nil))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
conv =>
  rhs
  lhs
  apply funext (g := _) _
  apply (λ x => Option.map ULift.up x.fst)
  apply (λ x => Cell.toOption_fromOption _)
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun x => Option.map ULift.up x.fst)
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (fun x => Option.map ULift.up x.fst)
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
conv =>
  rhs
  lhs
  apply funext (g := _) _
  apply (λ x => Option.map ULift.up ∘ Prod.fst)
  apply (λ x => rfl)
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map ((fun x => Option.map ULift.up ∘ Prod.fst) (Row sch))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map ((fun x => Option.map ULift.up ∘ Prod.fst) (Row sch))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
rw [←List.map_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (Option.map ULift.up)
      (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows))))
Theorem: groupBySubtractive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map (Option.map ULift.up)
      (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows))))
Tactic:
apply List.no_dups_map_injective
Proof state after:
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ Function.injective (Option.map ULift.up)

case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupBySubtractive_spec4
Proof state before:
case hf
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ Function.injective (Option.map ULift.up)

case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
. intros x y hxy
  cases x
  . cases y
    . rfl
    . contradiction
  . cases y
    . contradiction
    . cases hxy; rfl
Proof state after:
case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Theorem: groupBySubtractive_spec4
Proof state before:
case hxs
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map Prod.fst (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))
Tactic:
. apply List.groupByKey_fsts_no_duplicates
Proof state after:
no goals