Theorem: List.forAllRel_nil_right (Algdata/Data/List/Prop.lean)

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
⊢ List.forAllRel r as [] = True
Tactic:
induction as
State after:
case nil
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ List.forAllRel r [] [] = True

case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : List.forAllRel r tail✝ [] = True
⊢ List.forAllRel r (head✝ :: tail✝) [] = True

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ List.forAllRel r [] [] = True
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : List.forAllRel r as [] = True
⊢ List.forAllRel r (a :: as) [] = True
Tactic:
case cons a as h_ind => dsimp [List.forAllRel, forAll] at *; rw [h_ind, true_and]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ List.forAllRel r [] [] = True
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : List.forAllRel r as [] = True
⊢ List.forAllRel r (a :: as) [] = True
Tactic:
dsimp [List.forAllRel, forAll] at *
State after:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : forAll (fun a => True) as = True
⊢ (True ∧ forAll (fun a => True) as) = True

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : forAll (fun a => True) as = True
⊢ (True ∧ forAll (fun a => True) as) = True
Tactic:
rw [h_ind, true_and]
State after:
no goals