internlm/Lean-Github huggingface dataset:
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ ⟨0, isLt✝⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨0, isLt✝⟩
Tactic:
constructor
Proof state after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ ⟨0, isLt✝⟩.toIndView = j.succ → j.succ.toFin = ⟨0, isLt✝⟩

case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ j.succ.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = j.succ
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ ⟨0, isLt✝⟩.toIndView = j.succ → j.succ.toFin = ⟨0, isLt✝⟩
Tactic:
intro
Proof state after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
a✝ : ⟨0, isLt✝⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨0, isLt✝⟩
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
a✝ : ⟨0, isLt✝⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨0, isLt✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ j.succ.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = j.succ
Tactic:
intro h
Proof state after:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
h : j.succ.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = j.succ
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
h : j.succ.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = j.succ
Tactic:
cases h
Proof state after:
no goals
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero ↔ IndView.zero.toFin = ⟨i + 1, hi⟩
Tactic:
constructor
Proof state after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨i + 1, hi⟩

case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = IndView.zero
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨i + 1, hi⟩
Tactic:
intro
Proof state after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
a✝ : ⟨i + 1, hi⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
a✝ : ⟨i + 1, hi⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = IndView.zero
Tactic:
intro h
Proof state after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
h : IndView.zero.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
h : IndView.zero.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero
Tactic:
cases h
Proof state after:
no goals
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
have hsucc : ⟨i+1, hi⟩ = Fin.succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ := rfl
Proof state after:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
constructor
Proof state after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ → j.succ.toFin = ⟨i + 1, hi⟩

case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = j.succ
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ → j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
intro h
Proof state after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
rw [IndView.toFin, hsucc]
Proof state after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin.succ = ⟨i, ⋯⟩.succ
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin.succ = ⟨i, ⋯⟩.succ
Tactic:
congr
Proof state after:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin = ⟨i, ⋯⟩
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin = ⟨i, ⋯⟩
Tactic:
rw [←toIndView_eq_iff_toFin_eq]
Proof state after:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ ⟨i, ⋯⟩.toIndView = j
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ ⟨i, ⋯⟩.toIndView = j
Tactic:
exact IndView.succ.inj h
Proof state after:
no goals
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = j.succ
Tactic:
intro h
Proof state after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.succ.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = j.succ
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.succ.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = j.succ
Tactic:
rw [IndView.toFin, hsucc] at h
Proof state after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ
Tactic:
rw [Fin.toIndView]
Proof state after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView.succ = j.succ
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView.succ = j.succ
Tactic:
congr
Proof state after:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView = j
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView = j
Tactic:
rw [toIndView_eq_iff_toFin_eq]
Proof state after:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ j.toFin = ⟨i, ⋯⟩
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ j.toFin = ⟨i, ⋯⟩
Tactic:
exact succ_inj.mp h
Proof state after:
no goals
Theorem: Fin.iotaFind_zero
Proof state before:
n✝ n : Nat
⊢ (Fin.zero ⋯).iotaFind = List.Index.head
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.iotaFind_succ
Proof state before:
n✝ n : Nat
i : Fin n
⊢ i.succ.iotaFind = (List.Index.map succ i.iotaFind).tail
Tactic:
cases i
Proof state after:
case mk
n✝ n val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩.succ.iotaFind = (List.Index.map succ ⟨val✝, isLt✝⟩.iotaFind).tail
Theorem: Fin.iotaFind_succ
Proof state before:
case mk
n✝ n val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩.succ.iotaFind = (List.Index.map succ ⟨val✝, isLt✝⟩.iotaFind).tail
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
i : (Fin.iota n).Index
⊢ i.val.iotaFind = i
Tactic:
induction n with
| zero => contradiction
| succ n H =>
  match i with
  | .head => rfl
  | .tail (i : List.Index ((Fin.iota n).map Fin.succ)) =>
    calc
    _ = iotaFind (List.Index.val (.tail i : List.Index (Fin.iota (n+1)))) := rfl
    _ = iotaFind (List.Index.val i) := by rw [List.Index.val_tail]
    _ = iotaFind (List.Index.val (List.Index.map Fin.succ (List.Index.unmap Fin.succ i))) := by rw [List.Index.map_unmap]
    _ = iotaFind (Fin.succ (List.Index.val (List.Index.unmap Fin.succ i))) := by rw [List.Index.val_map]
    _ = .tail (List.Index.map Fin.succ (iotaFind (List.Index.val (List.Index.unmap Fin.succ i)))) := by rw [iotaFind_succ]
    _ = .tail (List.Index.map Fin.succ (List.Index.unmap Fin.succ i)) := by rw [H]
    _ = .tail i := by rw [List.Index.map_unmap]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
case zero
n : Nat
i : (Fin.iota 0).Index
⊢ i.val.iotaFind = i
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
case succ
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i : (Fin.iota (n + 1)).Index
⊢ i.val.iotaFind = i
Tactic:
match i with
| .head => rfl
| .tail (i : List.Index ((Fin.iota n).map Fin.succ)) =>
  calc
  _ = iotaFind (List.Index.val (.tail i : List.Index (Fin.iota (n+1)))) := rfl
  _ = iotaFind (List.Index.val i) := by rw [List.Index.val_tail]
  _ = iotaFind (List.Index.val (List.Index.map Fin.succ (List.Index.unmap Fin.succ i))) := by rw [List.Index.map_unmap]
  _ = iotaFind (Fin.succ (List.Index.val (List.Index.unmap Fin.succ i))) := by rw [List.Index.val_map]
  _ = .tail (List.Index.map Fin.succ (iotaFind (List.Index.val (List.Index.unmap Fin.succ i)))) := by rw [iotaFind_succ]
  _ = .tail (List.Index.map Fin.succ (List.Index.unmap Fin.succ i)) := by rw [H]
  _ = .tail i := by rw [List.Index.map_unmap]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i : (Fin.iota (n + 1)).Index
⊢ List.Index.head.val.iotaFind = List.Index.head
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ i.tail.val.iotaFind = i.tail
Tactic:
calc
_ = iotaFind (List.Index.val (.tail i : List.Index (Fin.iota (n+1)))) := rfl
_ = iotaFind (List.Index.val i) := by rw [List.Index.val_tail]
_ = iotaFind (List.Index.val (List.Index.map Fin.succ (List.Index.unmap Fin.succ i))) := by rw [List.Index.map_unmap]
_ = iotaFind (Fin.succ (List.Index.val (List.Index.unmap Fin.succ i))) := by rw [List.Index.val_map]
_ = .tail (List.Index.map Fin.succ (iotaFind (List.Index.val (List.Index.unmap Fin.succ i)))) := by rw [iotaFind_succ]
_ = .tail (List.Index.map Fin.succ (List.Index.unmap Fin.succ i)) := by rw [H]
_ = .tail i := by rw [List.Index.map_unmap]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ i.tail.val.iotaFind = i.val.iotaFind
Tactic:
rw [List.Index.val_tail]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ i.val.iotaFind = (List.Index.map succ (List.Index.unmap succ i)).val.iotaFind
Tactic:
rw [List.Index.map_unmap]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.map succ (List.Index.unmap succ i)).val.iotaFind = (List.Index.unmap succ i).val.succ.iotaFind
Tactic:
rw [List.Index.val_map]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.unmap succ i).val.succ.iotaFind = (List.Index.map succ (List.Index.unmap succ i).val.iotaFind).tail
Tactic:
rw [iotaFind_succ]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.map succ (List.Index.unmap succ i).val.iotaFind).tail =
    (List.Index.map succ (List.Index.unmap succ i)).tail
Tactic:
rw [H]
Proof state after:
no goals
Theorem: Fin.iotaFind_val
Proof state before:
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ (List.Index.map succ (List.Index.unmap succ i)).tail = i.tail
Tactic:
rw [List.Index.map_unmap]
Proof state after:
no goals
Theorem: Fin.val_iotaFind
Proof state before:
n✝ n : Nat
i : Fin n
⊢ i.iotaFind.val = i
Tactic:
induction n with
| zero => cases i; contradiction
| succ n H =>
  match i with
  | ⟨0,_⟩ => rfl
  | ⟨i+1,hi⟩ =>
    apply Fin.eq
    open List.Index in rw [iotaFind, val_tail, val_map, H, Fin.succ]
Proof state after:
no goals
Theorem: Fin.val_iotaFind
Proof state before:
case zero
n : Nat
i : Fin 0
⊢ i.iotaFind.val = i
Tactic:
cases i
Proof state after:
case zero.mk
n val✝ : Nat
isLt✝ : val✝ < 0
⊢ ⟨val✝, isLt✝⟩.iotaFind.val = ⟨val✝, isLt✝⟩
Theorem: Fin.val_iotaFind
Proof state before:
case zero.mk
n val✝ : Nat
isLt✝ : val✝ < 0
⊢ ⟨val✝, isLt✝⟩.iotaFind.val = ⟨val✝, isLt✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.val_iotaFind
Proof state before:
case succ
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i : Fin (n + 1)
⊢ i.iotaFind.val = i
Tactic:
match i with
| ⟨0,_⟩ => rfl
| ⟨i+1,hi⟩ =>
  apply Fin.eq
  open List.Index in rw [iotaFind, val_tail, val_map, H, Fin.succ]
Proof state after:
no goals
Theorem: Fin.val_iotaFind
Proof state before:
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.iotaFind.val = ⟨0, isLt✝⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.val_iotaFind
Proof state before:
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.iotaFind.val = ⟨i + 1, hi⟩
Tactic:
apply Fin.eq
Proof state after:
case a
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ↑⟨i + 1, hi⟩.iotaFind.val = ↑⟨i + 1, hi⟩
Theorem: Fin.val_iotaFind
Proof state before:
case a
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ↑⟨i + 1, hi⟩.iotaFind.val = ↑⟨i + 1, hi⟩
Tactic:
open List.Index in rw [iotaFind, val_tail, val_map, H, Fin.succ]
Proof state after:
no goals
Theorem: Fin.val_iotaFind
Proof state before:
case a
n✝ n : Nat
H : ∀ (i : Fin n), i.iotaFind.val = i
i✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
⊢ ↑⟨i + 1, hi⟩.iotaFind.val = ↑⟨i + 1, hi⟩
Tactic:
rw [iotaFind, val_tail, val_map, H, Fin.succ]
Proof state after:
no goals
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
⊢ loop p i hi = some k → p k = true
Tactic:
intro h
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h : loop p i hi = some k
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h : loop p i hi = some k
⊢ p k = true
Tactic:
unfold loop at h
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h :
  (if h : i = n then none
    else
      let_fun hi := ⋯;
      if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h :
  (if h : i = n then none
    else
      let_fun hi := ⋯;
      if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Tactic:
split at h
Proof state after:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : i = n
h : False
⊢ p k = true

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : i = n
h : False
⊢ p k = true

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Tactic:
next => contradiction
Proof state after:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Tactic:
next hne =>
  have hi : i < n := Nat.lt_of_le_of_ne hi hne
  simp only at h
  split at h
  next hp =>
    cases h
    exact hp
  next =>
    exact loop_some (i+1) (Nat.succ_le_of_lt hi) k h
Proof state after:
no goals
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
h✝ : i = n
h : False
⊢ p k = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
⊢ p k = true
Tactic:
have hi : i < n := Nat.lt_of_le_of_ne hi hne
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
hi : i < n
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    some k
hi : i < n
⊢ p k = true
Tactic:
simp only at h
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
h : (if p ⟨i, ⋯⟩ = true then some ⟨i, ⋯⟩ else loop p (i + 1) ⋯) = some k
hi : i < n
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
h : (if p ⟨i, ⋯⟩ = true then some ⟨i, ⋯⟩ else loop p (i + 1) ⋯) = some k
hi : i < n
⊢ p k = true
Tactic:
split at h
Proof state after:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : p ⟨i, ⋯⟩ = true
h : some ⟨i, ⋯⟩ = some k
⊢ p k = true

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = some k
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : p ⟨i, ⋯⟩ = true
h : some ⟨i, ⋯⟩ = some k
⊢ p k = true

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = some k
⊢ p k = true
Tactic:
next hp =>
  cases h
  exact hp
Proof state after:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = some k
⊢ p k = true
Theorem: Fin.find?.loop_some
Proof state before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = some k
⊢ p k = true
Tactic:
next =>
  exact loop_some (i+1) (Nat.succ_le_of_lt hi) k h
Proof state after:
no goals
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
h : some ⟨i, ⋯⟩ = some k
⊢ p k = true
Tactic:
cases h
Proof state after:
case refl
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
⊢ p ⟨i, ⋯⟩ = true
Theorem: Fin.find?.loop_some
Proof state before:
case refl
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
⊢ p ⟨i, ⋯⟩ = true
Tactic:
exact hp
Proof state after:
no goals
Theorem: Fin.find?.loop_some
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = some k
⊢ p k = true
Tactic:
exact loop_some (i+1) (Nat.succ_le_of_lt hi) k h
Proof state after:
no goals
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
⊢ i ≤ ↑k → loop p i hi = none → p k = false
Tactic:
intro hik h
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h : loop p i hi = none
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h : loop p i hi = none
⊢ p k = false
Tactic:
unfold loop at h
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h :
  (if h : i = n then none
    else
      let_fun hi := ⋯;
      if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false