case h
F : Type ?u.66752
α✝ : Type ?u.66755
β : Type ?u.66758
R : Type ?u.66761
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_1
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x) ↔ x ∈ {a | Even a}
F : Type ?u.66752
α✝ : Type ?u.66755
β : Type ?u.66758
R : Type ?u.66761
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_1
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x) = {a | Even a}
ext x
no goals
case h
F : Type ?u.66752
α✝ : Type ?u.66755
β : Type ?u.66758
R : Type ?u.66761
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_1
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x) ↔ x ∈ {a | Even a}
simp [eq_comm, two_mul, Even]