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

State before:
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂
Tactic:
induction h <;> constructor <;> [(apply H; assumption); assumption]
State after:
no goals

State before:
case cons.a
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝
Tactic:
apply H
State after:
case cons.a.a
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ R a✝² b✝

State before:
case cons.a.a
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ R a✝² b✝
Tactic:
assumption
State after:
no goals