Theorem: List.forall₂_nil_left_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