ι : Type ?u.480589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
l✝ : List α
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → All₂ p l → q x ∧ All₂ q l
ι : Type ?u.480589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
l✝ : List α
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ All₂ p (x :: l) → All₂ q (x :: l)
simp
ι : Type ?u.480589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
l✝ : List α
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ All₂ p l → q x ∧ All₂ q l
ι : Type ?u.480589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
l✝ : List α
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → All₂ p l → q x ∧ All₂ q l
rw [←and_imp]
no goals
ι : Type ?u.480589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
l✝ : List α
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ All₂ p l → q x ∧ All₂ q l
exact And.imp (h x) (All₂.imp h)