internlm/Lean-Github huggingface dataset:
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₁ as₂ bs : List α
⊢ reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
Tactic:
revert bs
Proof state after:
α : Type u
β : Type v
γ : Type w
as₁ as₂ : List α
⊢ ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₁ as₂ : List α
⊢ ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
Tactic:
induction as₁ <;> intro bs
Proof state after:
case nil
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs

case cons
α : Type u
β : Type v
γ : Type w
as₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {bs : List α}, reverseAux (tail✝ ++ as₂) bs = reverse as₂ ++ reverseAux tail✝ bs
bs : List α
⊢ reverseAux (head✝ :: tail✝ ++ as₂) bs = reverse as₂ ++ reverseAux (head✝ :: tail✝) bs
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs
Tactic:
case nil => rw [reverseAux_eq_append]; rfl
Proof state after:
no goals
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: as₁ ++ as₂) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
Tactic:
case cons a₁ as₁ h_ind =>
  rw [cons_append]
  unfold reverseAux
  rw [h_ind]
Proof state after:
no goals
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs
Tactic:
rw [reverseAux_eq_append]
Proof state after:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) [] ++ bs = reverse as₂ ++ reverseAux [] bs
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) [] ++ bs = reverse as₂ ++ reverseAux [] bs
Tactic:
rfl
Proof state after:
no goals
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: as₁ ++ as₂) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
Tactic:
rw [cons_append]
Proof state after:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: (as₁ ++ as₂)) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: (as₁ ++ as₂)) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
Tactic:
unfold reverseAux
Proof state after:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (as₁ ++ as₂) (a₁ :: bs) = reverse as₂ ++ reverseAux as₁ (a₁ :: bs)
Theorem: List.reverseAux_append_left
Proof state before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (as₁ ++ as₂) (a₁ :: bs) = reverse as₂ ++ reverseAux as₁ (a₁ :: bs)
Tactic:
rw [h_ind]
Proof state after:
no goals
Theorem: List.bind_map_binary_eq_map_bind_map
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
as : List α
bs : List β
⊢ (List.bind as fun a => map (f a) bs) = List.bind (map f as) fun f => map f bs
Tactic:
induction as with
| nil => rfl
| cons a as hi =>
  rw [cons_bind, map, cons_bind]
  rw [hi]
Proof state after:
no goals
Theorem: List.bind_map_binary_eq_map_bind_map
Proof state before:
case nil
α : Type u
β : Type v
γ : Type w
f : α → β → γ
bs : List β
⊢ (List.bind [] fun a => map (f a) bs) = List.bind (map f []) fun f => map f bs
Tactic:
rfl
Proof state after:
no goals
Theorem: List.bind_map_binary_eq_map_bind_map
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
bs : List β
a : α
as : List α
hi : (List.bind as fun a => map (f a) bs) = List.bind (map f as) fun f => map f bs
⊢ (List.bind (a :: as) fun a => map (f a) bs) = List.bind (map f (a :: as)) fun f => map f bs
Tactic:
rw [cons_bind, map, cons_bind]
Proof state after:
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
bs : List β
a : α
as : List α
hi : (List.bind as fun a => map (f a) bs) = List.bind (map f as) fun f => map f bs
⊢ (map (f a) bs ++ List.bind as fun a => map (f a) bs) = map (f a) bs ++ List.bind (map f as) fun f => map f bs
Theorem: List.bind_map_binary_eq_map_bind_map
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
bs : List β
a : α
as : List α
hi : (List.bind as fun a => map (f a) bs) = List.bind (map f as) fun f => map f bs
⊢ (map (f a) bs ++ List.bind as fun a => map (f a) bs) = map (f a) bs ++ List.bind (map f as) fun f => map f bs
Tactic:
rw [hi]
Proof state after:
no goals
Theorem: List.mapIdx'_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ mapIdx' (a :: as) f = f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ)
Tactic:
suffices ∀ (l : List α) (b : β) (acc : Array β) (h : l.length + (acc.size + 1) = as.length + 1), mapIdx'.go (a :: as) f l ⟨b :: acc.data⟩ h = b :: mapIdx'.go as (f ∘ Fin.succ) l acc (Nat.succ.inj h)
by
  dsimp [mapIdx', mapIdx'.go, Array.push, concat]
  exact this as _ #[] _
Proof state after:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
Theorem: List.mapIdx'_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
⊢ ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
Tactic:
intros l b acc h
Proof state after:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
l : List α
b : β
acc : Array β
h : length l + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
Theorem: List.mapIdx'_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
l : List α
b : β
acc : Array β
h : length l + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
Tactic:
induction l generalizing acc with
| nil => dsimp [mapIdx'.go]; simp only [Array.toList_eq]
| cons a' tl IH =>
  dsimp [mapIdx'.go, Array.push, concat]
  exact IH (acc.push (f _ a')) _
Proof state after:
no goals
Theorem: List.mapIdx'_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
this :
  ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
⊢ mapIdx' (a :: as) f = f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ)
Tactic:
dsimp [mapIdx', mapIdx'.go, Array.push, concat]
Proof state after:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
this :
  ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
⊢ mapIdx'.go (a :: as) f as { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] }
      (_ :
        length as +
            Array.size { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] } =
          Nat.succ (length as)) =
    f 0 a :: mapIdx'.go as (f ∘ Fin.succ) as #[] (_ : length as + Array.size #[] = length as + Array.size #[])
Theorem: List.mapIdx'_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
this :
  ∀ (l : List α) (b : β) (acc : Array β) (h : length l + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f l { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) l acc (_ : length l + Array.size acc = length as)
⊢ mapIdx'.go (a :: as) f as { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] }
      (_ :
        length as +
            Array.size { data := [f { val := Array.size #[], isLt := (_ : Array.size #[] < length (a :: as)) } a] } =
          Nat.succ (length as)) =
    f 0 a :: mapIdx'.go as (f ∘ Fin.succ) as #[] (_ : length as + Array.size #[] = length as + Array.size #[])
Tactic:
exact this as _ #[] _
Proof state after:
no goals
Theorem: List.mapIdx'_cons
Proof state before:
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f [] { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) [] acc (_ : length [] + Array.size acc = length as)
Tactic:
dsimp [mapIdx'.go]
Proof state after:
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ Array.toList { data := b :: acc.data } = b :: Array.toList acc
Theorem: List.mapIdx'_cons
Proof state before:
case nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
acc : Array β
h : length [] + (Array.size acc + 1) = length as + 1
⊢ Array.toList { data := b :: acc.data } = b :: Array.toList acc
Tactic:
simp only [Array.toList_eq]
Proof state after:
no goals
Theorem: List.mapIdx'_cons
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
a' : α
tl : List α
IH :
  ∀ (acc : Array β) (h : length tl + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f tl { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) tl acc (_ : length tl + Array.size acc = length as)
acc : Array β
h : length (a' :: tl) + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f (a' :: tl) { data := b :: acc.data } h =
    b :: mapIdx'.go as (f ∘ Fin.succ) (a' :: tl) acc (_ : length (a' :: tl) + Array.size acc = length as)
Tactic:
dsimp [mapIdx'.go, Array.push, concat]
Proof state after:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
a' : α
tl : List α
IH :
  ∀ (acc : Array β) (h : length tl + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f tl { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) tl acc (_ : length tl + Array.size acc = length as)
acc : Array β
h : length (a' :: tl) + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f tl
      {
        data :=
          b ::
            concat acc.data
              (f
                { val := Array.size { data := b :: acc.data },
                  isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                a') }
      (_ :
        length tl +
            Array.size
              {
                data :=
                  b ::
                    concat acc.data
                      (f
                        { val := Array.size { data := b :: acc.data },
                          isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                        a') } =
          Nat.succ (length as)) =
    b ::
      mapIdx'.go as (f ∘ Fin.succ) tl
        {
          data :=
            concat acc.data
              (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) } a') }
        (_ :
          length tl +
              Array.size
                {
                  data :=
                    concat acc.data
                      (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) }
                        a') } =
            length as)
Theorem: List.mapIdx'_cons
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
f : Fin (length as + 1) → α → β
b : β
a' : α
tl : List α
IH :
  ∀ (acc : Array β) (h : length tl + (Array.size acc + 1) = length as + 1),
    mapIdx'.go (a :: as) f tl { data := b :: acc.data } h =
      b :: mapIdx'.go as (f ∘ Fin.succ) tl acc (_ : length tl + Array.size acc = length as)
acc : Array β
h : length (a' :: tl) + (Array.size acc + 1) = length as + 1
⊢ mapIdx'.go (a :: as) f tl
      {
        data :=
          b ::
            concat acc.data
              (f
                { val := Array.size { data := b :: acc.data },
                  isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                a') }
      (_ :
        length tl +
            Array.size
              {
                data :=
                  b ::
                    concat acc.data
                      (f
                        { val := Array.size { data := b :: acc.data },
                          isLt := (_ : Array.size { data := b :: acc.data } < length (a :: as)) }
                        a') } =
          Nat.succ (length as)) =
    b ::
      mapIdx'.go as (f ∘ Fin.succ) tl
        {
          data :=
            concat acc.data
              (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) } a') }
        (_ :
          length tl +
              Array.size
                {
                  data :=
                    concat acc.data
                      (f { val := Array.size acc + 1, isLt := (_ : Nat.succ (Array.size acc) < Nat.succ (length as)) }
                        a') } =
            length as)
Tactic:
exact IH (acc.push (f _ a')) _
Proof state after:
no goals
Theorem: List.length_mapIdx'
Proof state before:
α : Type u
β : Type v
γ : Type w
as✝ : List α
f✝ : Fin (length as✝) → α → β
a : α
as : List α
IH : ∀ (x : Fin (length as) → α → β), length (mapIdx' as x) = length as
f : Fin (length (a :: as)) → α → β
⊢ length (mapIdx' (a :: as) f) = length (a :: as)
Tactic:
simp only [mapIdx'_cons, length, IH]
Proof state after:
no goals
Theorem: List.getElem_mapIdx'
Proof state before:
α : Type u
β : Type v
γ : Type w
as : List α
f : Fin (length as) → α → β
i : Nat
hi : i < length (mapIdx' as f)
⊢ (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
Tactic:
induction as generalizing i with
| nil => cases hi
| cons a as IH =>
  simp only [mapIdx'_cons]
  cases i with
  | zero => rfl
  | succ i => simp only [cons_getElem_succ, IH]; rfl
Proof state after:
no goals
Theorem: List.getElem_mapIdx'
Proof state before:
case nil
α : Type u
β : Type v
γ : Type w
f : Fin (length []) → α → β
i : Nat
hi : i < length (mapIdx' [] f)
⊢ (mapIdx' [] f)[i] = f { val := i, isLt := (_ : i < length []) } [][i]
Tactic:
cases hi
Proof state after:
no goals
Theorem: List.getElem_mapIdx'
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (mapIdx' (a :: as) f)[i] = f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]
Tactic:
simp only [mapIdx'_cons]
Proof state after:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[i] =
    f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]
Theorem: List.getElem_mapIdx'
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : i < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[i] =
    f { val := i, isLt := (_ : i < length (a :: as)) } (a :: as)[i]
Tactic:
cases i with
| zero => rfl
| succ i => simp only [cons_getElem_succ, IH]; rfl
Proof state after:
no goals
Theorem: List.getElem_mapIdx'
Proof state before:
case cons.zero
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
hi : Nat.zero < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[Nat.zero] =
    f { val := Nat.zero, isLt := (_ : Nat.zero < length (a :: as)) } (a :: as)[Nat.zero]
Tactic:
rfl
Proof state after:
no goals
Theorem: List.getElem_mapIdx'
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : Nat.succ i < length (mapIdx' (a :: as) f)
⊢ (f { val := 0, isLt := (_ : 0 < Nat.succ (length as)) } a :: mapIdx' as (f ∘ Fin.succ))[Nat.succ i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < length (a :: as)) } (a :: as)[Nat.succ i]
Tactic:
simp only [cons_getElem_succ, IH]
Proof state after:
case cons.succ
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : Nat.succ i < length (mapIdx' (a :: as) f)
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < length as) } as[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < length (a :: as)) } as[i]
Theorem: List.getElem_mapIdx'
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
a : α
as : List α
IH :
  ∀ (f : Fin (length as) → α → β) (i : Nat) (hi : i < length (mapIdx' as f)),
    (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
f : Fin (length (a :: as)) → α → β
i : Nat
hi : Nat.succ i < length (mapIdx' (a :: as) f)
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < length as) } as[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < length (a :: as)) } as[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: UInt.toNat_inj
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ {a b : α}, toNat a = toNat b → a = b
Tactic:
intro a b h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : toNat a = toNat b
⊢ a = b
Theorem: UInt.toNat_inj
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : toNat a = toNat b
⊢ a = b
Tactic:
rw [←ofNat_toNat a, ←ofNat_toNat b, h]
Proof state after:
no goals
Theorem: UInt.toNat_lt
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a < 2 ^ length α
Tactic:
rw [←ofNat_toNat a, toNat_ofNat]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α < 2 ^ length α
Theorem: UInt.toNat_lt
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α < 2 ^ length α
Tactic:
exact Nat.mod_lt (toNat a) (y:=2^(length α)) (Nat.pos_pow_of_pos _ (Nat.zero_lt_succ 1))
Proof state after:
no goals
Theorem: UInt.toNat_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (~~~a) = 2 ^ length α - (toNat a + 1)
Tactic:
simp [complement_eq, toNat_sub, toNat_add, toNat_zero]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : toNat (1 : α) = 1 % 2^length α := toNat_ofNat 1
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
rw [this, Nat.add_mod_mod]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
cases Nat.lt_or_eq_of_le (toNat_lt a)
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h✝ : Nat.succ (toNat a) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h✝ : Nat.succ (toNat a) = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
case inl h =>
  have : toNat a + 1 < 2^length α := h
  have : 2^length α - (toNat a + 1) < 2^length α :=
    Nat.sub_lt_self (Nat.zero_lt_succ _) (toNat_lt a)
  rw [
    Nat.mod_eq_of_lt ‹toNat a + 1 < 2^length α›,
    Nat.mod_eq_of_lt ‹2^length α - (toNat a + 1) < 2^length α›
  ]
Proof state after:
no goals
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
case inr h =>
  have : toNat a + 1 = 2^length α := h
  simp [this]
Proof state after:
no goals