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

State before:
γ : Type u_1
α : Type u_2
α✝ : Type u_3
R : α → α✝ → Prop
f : γ → α
x✝ : List α✝
⊢ Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b => R (f c) b) [] x✝
Tactic:
simp only [map, forall₂_nil_left_iff]
State after:
no goals

State before:
γ : Type u_1
α : Type u_2
α✝ : Type u_3
R : α → α✝ → Prop
f : γ → α
a : γ
l : List γ
x✝ : List α✝
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b => R (f c) b) (a :: l) x✝
Tactic:
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]
State after:
no goals