Theorem: pivotWider_spec1 (Table/Proofs.lean)

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))))],
    header (pivotWider t c1 c2) =
      Schema.names
          (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:
intro t c1 c2 hc1 hc2 inst
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))))
⊢ header (pivotWider t c1 c2) =
    Schema.names
        (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))

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))))
⊢ header (pivotWider t c1 c2) =
    Schema.names
        (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:
simp only [header, Schema.names]
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))))
⊢ List.map Prod.fst
      (Schema.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.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))

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))))
⊢ List.map Prod.fst
      (Schema.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.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:
rw [Schema.append_eq_List_append]
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))))
⊢ 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.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))

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))))
⊢ 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.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 := List.map_append Prod.fst
  (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 hc1))))
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
      (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.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.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.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))

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
      (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.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.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.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:
simp only [HAppend.hAppend, Append.append] at this
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)))))
⊢ 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.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))

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.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.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:
rw [this]
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)))))
⊢ 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.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))

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 (List.map (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:
rw [List.map_map]
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)))))
⊢ 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))

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)
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))

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)))))
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))
Tactic:
rw [hf]
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 id (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))

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)))))
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 id (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:
rw [List.map_id]
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.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))

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)))))
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.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:
rfl
State after:
no goals