internlm/Lean-Github huggingface dataset:
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)
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: 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
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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: groupBySubtractive_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: 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
Theorem: update_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (subsch : RetypedSubschema sch) (t : Table sch) (f : Row sch → Row (RetypedSubschema.toSchema subsch)),
    nrows (update subsch t f) = nrows t
Tactic:
intros
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ nrows (update subsch✝ t✝ f✝) = nrows t✝
Theorem: update_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ nrows (update subsch✝ t✝ f✝) = nrows t✝
Tactic:
simp only [nrows, update, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ List.length (List.map (fun r => update.updateCells r (f✝ r)) t✝.rows) = List.length t✝.rows
Theorem: update_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ List.length (List.map (fun r => update.updateCells r (f✝ r)) t✝.rows) = List.length t✝.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: select_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
⊢ ∀ (t : Table sch) (f : Row sch → Fin (nrows t) → Row sch'), nrows (select t f) = nrows t
Tactic:
intros
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ nrows (select t✝ f✝) = nrows t✝
Theorem: select_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ nrows (select t✝ f✝) = nrows t✝
Tactic:
simp only [nrows, select, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ List.length
      (List.map (fun x => f✝ x.snd ((_ : List.length t✝.rows = nrows t✝) ▸ x.fst)) (List.verifiedEnum t✝.rows)) =
    List.length t✝.rows
Theorem: select_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ List.length
      (List.map (fun x => f✝ x.snd ((_ : List.length t✝.rows = nrows t✝) ▸ x.fst)) (List.verifiedEnum t✝.rows)) =
    List.length t✝.rows
Tactic:
exact Eq.trans (List.length_map _ _) (List.length_verifiedEnum _)
Proof state after:
no goals
Theorem: Schema.map_eq_List_map
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ @map = @List.map
Tactic:
funext _ _ _ xs
Proof state after:
case h.h.h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
xs : List x✝²
⊢ map x✝ xs = List.map x✝ xs
Theorem: Schema.map_eq_List_map
Proof state before:
case h.h.h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
xs : List x✝²
⊢ map x✝ xs = List.map x✝ xs
Tactic:
induction xs with
| nil => rfl
| cons _ _ ih =>
  simp only [map, List.map]
  exact congrArg _ ih
Proof state after:
no goals
Theorem: Schema.map_eq_List_map
Proof state before:
case h.h.h.h.nil
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
⊢ map x✝ [] = List.map x✝ []
Tactic:
rfl
Proof state after:
no goals
Theorem: Schema.map_eq_List_map
Proof state before:
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ map x✝ (head✝ :: tail✝) = List.map x✝ (head✝ :: tail✝)
Tactic:
simp only [map, List.map]
Proof state after:
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ x✝ head✝ :: map x✝ tail✝ = x✝ head✝ :: List.map x✝ tail✝
Theorem: Schema.map_eq_List_map
Proof state before:
case h.h.h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝² : Type u_2
x✝¹ : Type u_1
x✝ : x✝² → x✝¹
head✝ : x✝²
tail✝ : List x✝²
ih : map x✝ tail✝ = List.map x✝ tail✝
⊢ x✝ head✝ :: map x✝ tail✝ = x✝ head✝ :: List.map x✝ tail✝
Tactic:
exact congrArg _ ih
Proof state after:
no goals
Theorem: Schema.length_eq_List_length
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ @length = @List.length
Tactic:
funext _ xs
Proof state after:
case h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
xs : List x✝
⊢ length xs = List.length xs
Theorem: Schema.length_eq_List_length
Proof state before:
case h.h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
xs : List x✝
⊢ length xs = List.length xs
Tactic:
induction xs with
| nil => rfl
| cons _ _ ih =>
  simp only [length, List.length]
  exact congrArg _ ih
Proof state after:
no goals
Theorem: Schema.length_eq_List_length
Proof state before:
case h.h.nil
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
⊢ length [] = List.length []
Tactic:
rfl
Proof state after:
no goals
Theorem: Schema.length_eq_List_length
Proof state before:
case h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
head✝ : x✝
tail✝ : List x✝
ih : length tail✝ = List.length tail✝
⊢ length (head✝ :: tail✝) = List.length (head✝ :: tail✝)
Tactic:
simp only [length, List.length]
Proof state after:
case h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
head✝ : x✝
tail✝ : List x✝
ih : length tail✝ = List.length tail✝
⊢ length tail✝ + 1 = List.length tail✝ + 1
Theorem: Schema.length_eq_List_length
Proof state before:
case h.h.cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
x✝ : Type u_1
head✝ : x✝
tail✝ : List x✝
ih : length tail✝ = List.length tail✝
⊢ length tail✝ + 1 = List.length tail✝ + 1
Tactic:
exact congrArg _ ih
Proof state after:
no goals
Theorem: Schema.length_nths
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
xs : List α
ns : List (Fin (length xs))
⊢ List.length (nths xs ns) = List.length ns
Tactic:
rw [nths, Schema.map_eq_List_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
xs : List α
ns : List (Fin (length xs))
⊢ List.length (List.map (fun n => nth xs n.val (_ : n.val < length xs)) ns) = List.length ns
Theorem: Schema.length_nths
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
xs : List α
ns : List (Fin (length xs))
⊢ List.length (List.map (fun n => nth xs n.val (_ : n.val < length xs)) ns) = List.length ns
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: Schema.sieve_eq_List_sieve
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
τ : Type u_1
bs : List Bool
xs✝ xs : List τ
⊢ sieve [] xs = List.sieve [] xs
Tactic:
simp only [sieve, List.sieve]
Proof state after:
no goals
Theorem: Schema.sieve_eq_List_sieve
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
τ : Type u_1
bs : List Bool
xs : List τ
head✝ : Bool
tail✝ : List Bool
⊢ sieve (head✝ :: tail✝) [] = List.sieve (head✝ :: tail✝) []
Tactic:
simp only [sieve, List.sieve]
Proof state after:
no goals
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get (List.map Prod.fst (nths xs (n :: ns)))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [nths, map, get]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
rw [nth_eq_get]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) } ::
          map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) } ::
          map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := 0, isLt := (_ : 0 < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := 0, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := 0, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [List.get]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) }).fst =
    List.get (List.map Prod.fst xs) { val := n.val, isLt := (_ : n.val < List.length (List.map Prod.fst xs)) }
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
hi : 0 < List.length (n :: ns)
⊢ (List.get xs { val := n.val, isLt := (_ : n.val < List.length xs) }).fst =
    List.get (List.map Prod.fst xs) { val := n.val, isLt := (_ : n.val < List.length (List.map Prod.fst xs)) }
Tactic:
rw [List.get_map Prod.fst]
Proof state after:
no goals
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
⊢ List.get (List.map Prod.fst (nths xs (n :: ns)))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [nths, map, get]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
have ih := get_map_nths_eq_get_get xs ns i (Nat.lt_of_succ_lt_succ hi)
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
ih :
  List.get (List.map Prod.fst (nths xs ns))
      { val := i, isLt := (_ : i < List.length (List.map Prod.fst (nths xs ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val,
        isLt :=
          (_ : (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val < List.length (List.map Prod.fst xs)) }
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }