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

State before:
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
l₁ : List α✝¹
l₂ : List α✝
h : Forall₂ R l₁ l₂
⊢ ∀ (a : α✝¹), a ∈ l₁ → ∃ b, b ∈ l₂ ∧ R a b
Tactic:
induction h with simp [*] | cons _ _ ih => exact fun a h => .inr (ih _ h)
State after:
no goals

State before:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
ih : ∀ (a : α✝¹), a ∈ l₁✝ → ∃ b, b ∈ l₂✝ ∧ R a b
⊢ ∀ (a : α✝¹), a ∈ l₁✝ → R a b✝ ∨ ∃ a_2, a_2 ∈ l₂✝ ∧ R a a_2
Tactic:
exact fun a h => .inr (ih _ h)
State after:
no goals