Theorem: pivotWider_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
this :
  List.map Prod.fst
      (List.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.append
      (List.map Prod.fst
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil))))
      (List.map Prod.fst (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1)))))
⊢ List.append
      (List.map Prod.fst
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil))))
      (List.map (Prod.fst ∘ fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1)))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Tactic:
have hf : (Prod.fst ∘ fun x => (x, τ)) = @id η := funext (λ _ => rfl)
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
this :
  List.map Prod.fst
      (List.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.append
      (List.map Prod.fst
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil))))
      (List.map Prod.fst (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1)))))
hf : (Prod.fst ∘ fun x => (x, τ)) = id
⊢ List.append
      (List.map Prod.fst
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil))))
      (List.map (Prod.fst ∘ fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1)))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))