Theorem: List.Forall₂.rfl (Lean4Lean/Std/Basic.lean)

State before:
α : Type u_1
R : α → α → Prop
l : List α
h : ∀ (a : α), a ∈ l → R a a
⊢ Forall₂ R l l
Tactic:
induction l with
| nil => constructor
| cons _ _ ih => simp at h; exact .cons h.1 (ih h.2)
State after:
no goals

State before:
case nil
α : Type u_1
R : α → α → Prop
h : ∀ (a : α), a ∈ [] → R a a
⊢ Forall₂ R [] []
Tactic:
constructor
State after:
no goals

State before:
case cons
α : Type u_1
R : α → α → Prop
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → R a a) → Forall₂ R tail✝ tail✝
h : ∀ (a : α), a ∈ head✝ :: tail✝ → R a a
⊢ Forall₂ R (head✝ :: tail✝) (head✝ :: tail✝)
Tactic:
simp at h
State after:
case cons
α : Type u_1
R : α → α → Prop
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → R a a) → Forall₂ R tail✝ tail✝
h : R head✝ head✝ ∧ ∀ (a : α), a ∈ tail✝ → R a a
⊢ Forall₂ R (head✝ :: tail✝) (head✝ :: tail✝)

State before:
case cons
α : Type u_1
R : α → α → Prop
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → R a a) → Forall₂ R tail✝ tail✝
h : R head✝ head✝ ∧ ∀ (a : α), a ∈ tail✝ → R a a
⊢ Forall₂ R (head✝ :: tail✝) (head✝ :: tail✝)
Tactic:
exact .cons h.1 (ih h.2)
State after:
no goals