case h.h
α✝ : Type uu
β : Type vv
l₁✝ l₂✝ : List α✝
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ List.beq l₁ l₂ = decide (l₁ = l₂)
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ List.beq = fun a b => decide (a = b)
funext l₁ l₂
case h.h
α✝ : Type uu
β : Type vv
l₁✝ l₂✝ : List α✝
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ == l₂) = decide (l₁ = l₂)
case h.h
α✝ : Type uu
β : Type vv
l₁✝ l₂✝ : List α✝
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ List.beq l₁ l₂ = decide (l₁ = l₂)
show (l₁ == l₂) = _
no goals
case h.h
α✝ : Type uu
β : Type vv
l₁✝ l₂✝ : List α✝
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ == l₂) = decide (l₁ = l₂)
rw [Bool.eq_iff_eq_true_iff, @beq_iff_eq _ (_), decide_eq_true_iff]