case h
F : Type ?u.76433
α✝ : Type ?u.76436
β : Type ?u.76439
R : Type ?u.76442
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_1
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x + 1) ↔ x ∈ {a | Odd a}
F : Type ?u.76433
α✝ : Type ?u.76436
β : Type ?u.76439
R : Type ?u.76442
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_1
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x + 1) = {a | Odd a}
ext x
no goals
case h
F : Type ?u.76433
α✝ : Type ?u.76436
β : Type ?u.76439
R : Type ?u.76442
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_1
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x + 1) ↔ x ∈ {a | Odd a}
simp [Odd, eq_comm]