case h.e'_2.h.e'_2
α : Type ?u.433649
β : Type ?u.433652
γ : Type ?u.433655
n✝ m✝ l n m : ℕ
⊢ (fun x => x = m) = Eq m

case h.e'_3.h₁.a
α : Type ?u.433649
β : Type ?u.433652
γ : Type ?u.433655
n✝ m✝ l n m : ℕ
⊢ m < n ↔ m ∈ range n
α : Type ?u.433649
β : Type ?u.433652
γ : Type ?u.433655
n✝ m✝ l n m : ℕ
⊢ filter (fun x => x = m) (range n) = if m < n then {m} else ∅
convert filter_eq (range n) m using 2
case h.e'_2.h.e'_2.h.a
α : Type ?u.433649
β : Type ?u.433652
γ : Type ?u.433655
n✝ m✝ l n m x✝ : ℕ
⊢ x✝ = m ↔ m = x✝
case h.e'_2.h.e'_2
α : Type ?u.433649
β : Type ?u.433652
γ : Type ?u.433655
n✝ m✝ l n m : ℕ
⊢ (fun x => x = m) = Eq m
ext
no goals
case h.e'_2.h.e'_2.h.a
α : Type ?u.433649
β : Type ?u.433652
γ : Type ?u.433655
n✝ m✝ l n m x✝ : ℕ
⊢ x✝ = m ↔ m = x✝
rw [eq_comm]
no goals
case h.e'_3.h₁.a
α : Type ?u.433649
β : Type ?u.433652
γ : Type ?u.433655
n✝ m✝ l n m : ℕ
⊢ m < n ↔ m ∈ range n
simp