-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_getElem {l : List α} {p : α → Prop} :
    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a

Proof state:
case cons.mpr.intro.zero
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
h : 0 < l.length + 1
⊢ p (a :: l)[0]

Tactic:
simpa

Result:
no goals

Proof state:
case cons.mpr.intro.succ.a
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
n : Nat
h : n + 1 < l.length + 1
⊢ (a :: l)[n + 1] ∈ l

Tactic:
simp only [getElem_cons_succ]

Result:
case cons.mpr.intro.succ.a
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
n : Nat
h : n + 1 < l.length + 1
⊢ l[n] ∈ l

Proof state:
case cons.mpr
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
⊢ (p a ∧ ∀ (a : α), a ∈ l → p a) → ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]

Tactic:
rintro ⟨h, w⟩

Result:
case cons.mpr.intro
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h : p a
w : ∀ (a : α), a ∈ l → p a
⊢ ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]

Proof state:
case cons
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
⊢ (∀ (i : Nat) (h : i < (a :: l).length), p (a :: l)[i]) ↔ ∀ (a_1 : α), a_1 ∈ a :: l → p a_1

Tactic:
simp only [length_cons, mem_cons, forall_eq_or_imp]

Result:
case cons
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
⊢ (∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]) ↔ p a ∧ ∀ (a : α), a ∈ l → p a

Proof state:
case cons.mpr.intro
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h : p a
w : ∀ (a : α), a ∈ l → p a
⊢ ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]

Tactic:
rintro (_ | n) h

Result:
case cons.mpr.intro.zero
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
h : 0 < l.length + 1
⊢ p (a :: l)[0]

case cons.mpr.intro.succ
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
n : Nat
h : n + 1 < l.length + 1
⊢ p (a :: l)[n + 1]

Proof state:
case cons.mp.right
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ ∀ (a : α), a ∈ l → p a

Tactic:
apply ih.1

Result:
case cons.mp.right
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ ∀ (i : Nat) (h : i < l.length), p l[i]

Proof state:
case cons.mp
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
⊢ (∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]) → p a ∧ ∀ (a : α), a ∈ l → p a

Tactic:
intro w

Result:
case cons.mp
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ p a ∧ ∀ (a : α), a ∈ l → p a

Proof state:
case cons.mp.right
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ ∀ (i : Nat) (h : i < l.length), p l[i]

Tactic:
intro n h

Result:
case cons.mp.right
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
n : Nat
h : n < l.length
⊢ p l[n]

Proof state:
case cons
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
⊢ (∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]) ↔ p a ∧ ∀ (a : α), a ∈ l → p a

Tactic:
constructor

Result:
case cons.mp
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
⊢ (∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]) → p a ∧ ∀ (a : α), a ∈ l → p a

case cons.mpr
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
⊢ (p a ∧ ∀ (a : α), a ∈ l → p a) → ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]

Proof state:
case cons.mp.right
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
n : Nat
h : n < l.length
⊢ p l[n]

Tactic:
simpa using w (n+1) (Nat.add_lt_add_right h 1)

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Prop
⊢ (∀ (i : Nat) (h : i < [].length), p [][i]) ↔ ∀ (a : α), a ∈ [] → p a

Tactic:
simp

Result:
no goals

Proof state:
case cons.mpr.intro.succ.a
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
n : Nat
h : n + 1 < l.length + 1
⊢ l[n] ∈ l

Tactic:
exact getElem_mem (lt_of_succ_lt_succ h)

Result:
no goals

Proof state:
case cons.mpr.intro.succ
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
n : Nat
h : n + 1 < l.length + 1
⊢ p (a :: l)[n + 1]

Tactic:
apply w

Result:
case cons.mpr.intro.succ.a
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
h✝ : p a
w : ∀ (a : α), a ∈ l → p a
n : Nat
h : n + 1 < l.length + 1
⊢ (a :: l)[n + 1] ∈ l

Proof state:
case cons.mp.left
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ p a

Tactic:
exact w 0 (by simp)

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ 0 < l.length + 1

Tactic:
simp

Result:
no goals

Proof state:
case cons.mp
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ p a ∧ ∀ (a : α), a ∈ l → p a

Tactic:
constructor

Result:
case cons.mp.left
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ p a

case cons.mp.right
α : Type u_1
p : α → Prop
a : α
l : List α
ih : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a
w : ∀ (i : Nat) (h : i < l.length + 1), p (a :: l)[i]
⊢ ∀ (a : α), a ∈ l → p a