internlm/Lean-Github huggingface dataset:
Theorem: List.Index.find_none
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq :
  (match p head with
    | true => some head
    | false =>
      match Index.find? fun i => p i.tail with
      | some x_1 => some x_1.tail
      | none => none) =
    none
⊢ p i = false
Tactic:
split at heq
Proof state after:
case cons.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = true
heq : some head = none
⊢ p i = false

case cons.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p i = false
Theorem: List.Index.find_none
Proof state before:
case cons.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = true
heq : some head = none
⊢ p i = false
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.find_none
Proof state before:
case cons.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p i = false
Tactic:
cases i
Proof state after:
case cons.h_2.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p head = false

case cons.h_2.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
a✝ : xs.Index
⊢ p a✝.tail = false
Theorem: List.Index.find_none
Proof state before:
case cons.h_2.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p head = false
Tactic:
assumption
Proof state after:
no goals
Theorem: List.Index.find_none
Proof state before:
case cons.h_2.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
a✝ : xs.Index
⊢ p a✝.tail = false
Tactic:
split at heq
Proof state after:
case cons.h_2.tail.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
x✝ : xs.Index
heq✝ : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = none
⊢ p a✝.tail = false

case cons.h_2.tail.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
heq✝ : (Index.find? fun i => p i.tail) = none
heq : none = none
⊢ p a✝.tail = false
Theorem: List.Index.find_none
Proof state before:
case cons.h_2.tail.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
x✝ : xs.Index
heq✝ : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = none
⊢ p a✝.tail = false
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.find_none
Proof state before:
case cons.h_2.tail.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
heq✝ : (Index.find? fun i => p i.tail) = none
heq : none = none
⊢ p a✝.tail = false
Tactic:
next h => rw [ih _ h]
Proof state after:
no goals
Theorem: List.Index.find_none
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
h : (Index.find? fun i => p i.tail) = none
heq : none = none
⊢ p a✝.tail = false
Tactic:
rw [ih _ h]
Proof state after:
no goals
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ p (search h)
Tactic:
unfold search
Proof state after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ p
    (match hi : Index.find? fun i => decide ((fun i => p i) i) with
    | some i => i
    | none => absurd h ⋯)
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ p
    (match hi : Index.find? fun i => decide ((fun i => p i) i) with
    | some i => i
    | none => absurd h ⋯)
Tactic:
split
Proof state after:
case h_1
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
i✝ : xs.Index
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ p i✝

case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Theorem: List.Index.search_prop
Proof state before:
case h_1
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
i✝ : xs.Index
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ p i✝

case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Tactic:
next h =>
  apply of_decide_eq_true
  exact find_some _ h
Proof state after:
case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Theorem: List.Index.search_prop
Proof state before:
case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Tactic:
next f =>
  absurd h
  intro ⟨j, hj⟩
  have := find_none j f
  rw [decide_eq_true hj] at this
  contradiction
Proof state after:
no goals
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h✝ : ∃ i, p i
i✝ : xs.Index
h : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ p i✝
Tactic:
apply of_decide_eq_true
Proof state after:
case a
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h✝ : ∃ i, p i
i✝ : xs.Index
h : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ decide (p i✝) = true
Theorem: List.Index.search_prop
Proof state before:
case a
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h✝ : ∃ i, p i
i✝ : xs.Index
h : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ decide (p i✝) = true
Tactic:
exact find_some _ h
Proof state after:
no goals
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Tactic:
absurd h
Proof state after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ ¬∃ i, p i
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ ¬∃ i, p i
Tactic:
intro ⟨j, hj⟩
Proof state after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
⊢ False
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
⊢ False
Tactic:
have := find_none j f
Proof state after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : decide ((fun i => p i) j) = false
⊢ False
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : decide ((fun i => p i) j) = false
⊢ False
Tactic:
rw [decide_eq_true hj] at this
Proof state after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : true = false
⊢ False
Theorem: List.Index.search_prop
Proof state before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : true = false
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.search_eq
Proof state before:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
ip : DecidablePred p
iq : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : p = q
⊢ search hp = search hq
Tactic:
cases h
Proof state after:
case refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
iq : DecidablePred p
hq : ∃ j, p j
⊢ search hp = search hq
Theorem: List.Index.search_eq
Proof state before:
case refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
iq : DecidablePred p
hq : ∃ j, p j
⊢ search hp = search hq
Tactic:
cases Subsingleton.elim ip iq
Proof state after:
case refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp hq : ∃ j, p j
⊢ search hp = search hq
Theorem: List.Index.search_eq
Proof state before:
case refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp hq : ∃ j, p j
⊢ search hp = search hq
Tactic:
cases Subsingleton.elim hp hq
Proof state after:
case refl.refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
⊢ search hp = search hp
Theorem: List.Index.search_eq
Proof state before:
case refl.refl.refl
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
ip : DecidablePred p
hp : ∃ i, p i
⊢ search hp = search hp
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.search_ext
Proof state before:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
⊢ (∀ (i : xs.Index), p i ↔ q i) → search hp = search hq
Tactic:
intro h
Proof state after:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ search hp = search hq
Theorem: List.Index.search_ext
Proof state before:
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ search hp = search hq
Tactic:
apply search_eq
Proof state after:
case h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ (fun i => p i) = fun i => q i
Theorem: List.Index.search_ext
Proof state before:
case h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
⊢ (fun i => p i) = fun i => q i
Tactic:
funext i
Proof state after:
case h.h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
i : xs.Index
⊢ p i = q i
Theorem: List.Index.search_ext
Proof state before:
case h.h
α✝ : Type u_1
xs : List α✝
p q : xs.Index → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : ∃ i, p i
hq : ∃ j, q j
h : ∀ (i : xs.Index), p i ↔ q i
i : xs.Index
⊢ p i = q i
Tactic:
exact propext (h i)
Proof state after:
no goals
Theorem: List.Index.toNat_eq_toNatTR
Proof state before:
⊢ @Index.toNat = @toNatTR
Tactic:
funext _ _ i
Proof state after:
case h.h.h
x✝¹ : Type u_1
x✝ : List x✝¹
i : x✝.Index
⊢ i.toNat = i.toNatTR
Theorem: List.Index.toNat_eq_toNatTR
Proof state before:
case h.h.h
x✝¹ : Type u_1
x✝ : List x✝¹
i : x✝.Index
⊢ i.toNat = i.toNatTR
Tactic:
induction i with simp_all only [Index.toNat, toNatTR, toNatTR.loop]
| tail => rw [lem]
Proof state after:
no goals
Theorem: List.Index.toNat_eq_toNatTR
Proof state before:
case h.h.h.tail
x✝² : Type u_1
x✝¹ xs✝ : List x✝²
x✝ : x✝²
a✝ : xs✝.Index
a_ih✝ : a✝.toNat = toNatTR.loop a✝ 0
⊢ toNatTR.loop a✝ 0 + 1 = toNatTR.loop a✝ (0 + 1)
Tactic:
rw [lem]
Proof state after:
no goals
Theorem: List.Index.toNat_eq_toNatTR
Proof state before:
α : Type ?u.14515
xs : List α
i : xs.Index
n : Nat
⊢ toNatTR.loop i (n + 1) = toNatTR.loop i n + 1
Tactic:
induction i generalizing n with
| head => rfl
| tail _ ih => simp [toNatTR.loop, ih]
Proof state after:
no goals
Theorem: List.Index.toNat_eq_toNatTR
Proof state before:
case head
α : Type ?u.14515
xs : List α
x✝ : α
xs✝ : List α
n : Nat
⊢ toNatTR.loop head (n + 1) = toNatTR.loop head n + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.toNat_eq_toNatTR
Proof state before:
case tail
α : Type ?u.14515
xs xs✝ : List α
x✝ : α
a✝ : xs✝.Index
ih : ∀ (n : Nat), toNatTR.loop a✝ (n + 1) = toNatTR.loop a✝ n + 1
n : Nat
⊢ toNatTR.loop a✝.tail (n + 1) = toNatTR.loop a✝.tail n + 1
Tactic:
simp [toNatTR.loop, ih]
Proof state after:
no goals
Theorem: List.Index.toNat_lt_length
Proof state before:
α✝ : Type u_1
xs : List α✝
i : xs.Index
⊢ i.toNat < xs.length
Tactic:
induction xs with
| nil => cases i
| cons x xs ih =>
  cases i with
  | head => exact Nat.zero_lt_succ ..
  | tail => apply Nat.succ_lt_succ (ih _)
Proof state after:
no goals
Theorem: List.Index.toNat_lt_length
Proof state before:
case nil
α✝ : Type u_1
i : [].Index
⊢ i.toNat < [].length
Tactic:
cases i
Proof state after:
no goals
Theorem: List.Index.toNat_lt_length
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), i.toNat < xs.length
i : (x :: xs).Index
⊢ i.toNat < (x :: xs).length
Tactic:
cases i with
| head => exact Nat.zero_lt_succ ..
| tail => apply Nat.succ_lt_succ (ih _)
Proof state after:
no goals
Theorem: List.Index.toNat_lt_length
Proof state before:
case cons.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), i.toNat < xs.length
⊢ head.toNat < (x :: xs).length
Tactic:
exact Nat.zero_lt_succ ..
Proof state after:
no goals
Theorem: List.Index.toNat_lt_length
Proof state before:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), i.toNat < xs.length
a✝ : xs.Index
⊢ a✝.tail.toNat < (x :: xs).length
Tactic:
apply Nat.succ_lt_succ (ih _)
Proof state after:
no goals
Theorem: List.Index.ofFin_toFin
Proof state before:
α✝ : Type u_1
xs : List α✝
i : xs.Index
⊢ Index.ofFin i.toFin = i
Tactic:
induction xs with
| nil => cases i
| cons x xs ih =>
  cases i with
  | head => rfl
  | tail i =>
    apply congrArg tail
    exact ih ..
Proof state after:
no goals
Theorem: List.Index.ofFin_toFin
Proof state before:
case nil
α✝ : Type u_1
i : [].Index
⊢ Index.ofFin i.toFin = i
Tactic:
cases i
Proof state after:
no goals
Theorem: List.Index.ofFin_toFin
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : (x :: xs).Index
⊢ Index.ofFin i.toFin = i
Tactic:
cases i with
| head => rfl
| tail i =>
  apply congrArg tail
  exact ih ..
Proof state after:
no goals
Theorem: List.Index.ofFin_toFin
Proof state before:
case cons.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
⊢ Index.ofFin head.toFin = head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.ofFin_toFin
Proof state before:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : xs.Index
⊢ Index.ofFin i.tail.toFin = i.tail
Tactic:
apply congrArg tail
Proof state after:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : xs.Index
⊢ Index.ofFin ⟨i.toNat, ⋯⟩ = i
Theorem: List.Index.ofFin_toFin
Proof state before:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : xs.Index
⊢ Index.ofFin ⟨i.toNat, ⋯⟩ = i
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: List.Index.toNat_ofFin
Proof state before:
α : Type u_1
xs : List α
i : Fin xs.length
⊢ (Index.ofFin i).toNat = ↑i
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨0,_⟩ => rfl
  | ⟨i+1,h⟩ =>
    apply congrArg Nat.succ
    rw [ih]
Proof state after:
no goals
Theorem: List.Index.toNat_ofFin
Proof state before:
case nil
α : Type u_1
i : Fin [].length
⊢ (Index.ofFin i).toNat = ↑i
Tactic:
cases i
Proof state after:
case nil.mk
α : Type u_1
val✝ : Nat
isLt✝ : val✝ < [].length
⊢ (Index.ofFin ⟨val✝, isLt✝⟩).toNat = ↑⟨val✝, isLt✝⟩
Theorem: List.Index.toNat_ofFin
Proof state before:
case nil.mk
α : Type u_1
val✝ : Nat
isLt✝ : val✝ < [].length
⊢ (Index.ofFin ⟨val✝, isLt✝⟩).toNat = ↑⟨val✝, isLt✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.toNat_ofFin
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i : Fin (x :: xs).length
⊢ (Index.ofFin i).toNat = ↑i
Tactic:
match i with
| ⟨0,_⟩ => rfl
| ⟨i+1,h⟩ =>
  apply congrArg Nat.succ
  rw [ih]
Proof state after:
no goals
Theorem: List.Index.toNat_ofFin
Proof state before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i : Fin (x :: xs).length
isLt✝ : 0 < (x :: xs).length
⊢ (Index.ofFin ⟨0, isLt✝⟩).toNat = ↑⟨0, isLt✝⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.toNat_ofFin
Proof state before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i✝ : Fin (x :: xs).length
i : Nat
h : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i + 1, h⟩).toNat = ↑⟨i + 1, h⟩
Tactic:
apply congrArg Nat.succ
Proof state after:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i✝ : Fin (x :: xs).length
i : Nat
h : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i, ⋯⟩).toNat = i
Theorem: List.Index.toNat_ofFin
Proof state before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i✝ : Fin (x :: xs).length
i : Nat
h : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i, ⋯⟩).toNat = i
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.Index.toFin_ofFin
Proof state before:
α : Type u_1
xs : List α
i : Fin xs.length
⊢ (Index.ofFin i).toFin = i
Tactic:
apply Fin.eq_of_val_eq
Proof state after:
case a
α : Type u_1
xs : List α
i : Fin xs.length
⊢ ↑(Index.ofFin i).toFin = ↑i
Theorem: List.Index.toFin_ofFin
Proof state before:
case a
α : Type u_1
xs : List α
i : Fin xs.length
⊢ ↑(Index.ofFin i).toFin = ↑i
Tactic:
apply toNat_ofFin
Proof state after:
no goals
Theorem: List.Index.val_ofFin_eq_get
Proof state before:
α : Type u_1
xs : List α
i : Fin xs.length
⊢ (Index.ofFin i).val = xs.get i
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨0, _⟩ => rfl
  | ⟨i+1, _⟩ => simp [Index.ofFin, ih]
Proof state after:
no goals
Theorem: List.Index.val_ofFin_eq_get
Proof state before:
case nil
α : Type u_1
i : Fin [].length
⊢ (Index.ofFin i).val = [].get i
Tactic:
cases i
Proof state after:
case nil.mk
α : Type u_1
val✝ : Nat
isLt✝ : val✝ < [].length
⊢ (Index.ofFin ⟨val✝, isLt✝⟩).val = [].get ⟨val✝, isLt✝⟩
Theorem: List.Index.val_ofFin_eq_get
Proof state before:
case nil.mk
α : Type u_1
val✝ : Nat
isLt✝ : val✝ < [].length
⊢ (Index.ofFin ⟨val✝, isLt✝⟩).val = [].get ⟨val✝, isLt✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.val_ofFin_eq_get
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).val = xs.get i
i : Fin (x :: xs).length
⊢ (Index.ofFin i).val = (x :: xs).get i
Tactic:
match i with
| ⟨0, _⟩ => rfl
| ⟨i+1, _⟩ => simp [Index.ofFin, ih]
Proof state after:
no goals
Theorem: List.Index.val_ofFin_eq_get
Proof state before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).val = xs.get i
i : Fin (x :: xs).length
isLt✝ : 0 < (x :: xs).length
⊢ (Index.ofFin ⟨0, isLt✝⟩).val = (x :: xs).get ⟨0, isLt✝⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.val_ofFin_eq_get
Proof state before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).val = xs.get i
i✝ : Fin (x :: xs).length
i : Nat
isLt✝ : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i + 1, isLt✝⟩).val = (x :: xs).get ⟨i + 1, isLt✝⟩
Tactic:
simp [Index.ofFin, ih]
Proof state after:
no goals
Theorem: List.Index.unmap_map
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
⊢ unmap f (map f i) = i
Tactic:
induction i with
| head => rfl
| tail i ih => exact congrArg tail ih
Proof state after:
no goals
Theorem: List.Index.unmap_map
Proof state before:
case head
α : Type u_1
β : Type u_2
f : α → β
xs : List α
x✝ : α
xs✝ : List α
⊢ unmap f (map f head) = head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.unmap_map
Proof state before:
case tail
α : Type u_1
β : Type u_2
f : α → β
xs xs✝ : List α
x✝ : α
i : xs✝.Index
ih : unmap f (map f i) = i
⊢ unmap f (map f i.tail) = i.tail
Tactic:
exact congrArg tail ih
Proof state after:
no goals
Theorem: List.Index.map_unmap
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
⊢ map f (unmap f i) = i
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  match i with
  | head => rfl
  | tail i => exact congrArg tail (ih i)
Proof state after:
no goals
Theorem: List.Index.map_unmap
Proof state before:
case nil
α : Type u_1
β : Type u_2
f : α → β
i : (List.map f []).Index
⊢ map f (unmap f i) = i
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.map_unmap
Proof state before:
case cons
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : ∀ (i : (List.map f xs).Index), map f (unmap f i) = i
i : (List.map f (x :: xs)).Index
⊢ map f (unmap f i) = i
Tactic:
match i with
| head => rfl
| tail i => exact congrArg tail (ih i)
Proof state after:
no goals
Theorem: List.Index.map_unmap
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : ∀ (i : (List.map f xs).Index), map f (unmap f i) = i
i : (List.map f (x :: xs)).Index
⊢ map f (unmap f head) = head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.map_unmap
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : ∀ (i : (List.map f xs).Index), map f (unmap f i) = i
i✝ : (List.map f (x :: xs)).Index
i : (List.map f xs).Index
⊢ map f (unmap f i.tail) = i.tail
Tactic:
exact congrArg tail (ih i)
Proof state after:
no goals