Theorem: List.forall₂_nil_right_iff (Lean4Lean/Std/Basic.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
l : List α✝
H : Forall₂ R l []
⊢ l = []
Tactic:
cases H
State after:
case nil
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ [] = []

State before:
case nil
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ [] = []
Tactic:
rfl
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
l : List α✝
⊢ l = [] → Forall₂ R l []
Tactic:
rintro rfl
State after:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ Forall₂ R [] []

State before:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ Forall₂ R [] []
Tactic:
exact Forall₂.nil
State after:
no goals