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

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

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