case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type ?u.86642
inst✝² : Semiring α
inst✝¹ : Semiring β
n : α
inst✝ : RingHomClass F α β
f : F
m : α
⊢ Odd (↑f (2 * m + 1))
F : Type u_1
α : Type u_2
β : Type u_3
R : Type ?u.86642
inst✝² : Semiring α
inst✝¹ : Semiring β
m n : α
inst✝ : RingHomClass F α β
f : F
⊢ Odd m → Odd (↑f m)
rintro ⟨m, rfl⟩
no goals
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type ?u.86642
inst✝² : Semiring α
inst✝¹ : Semiring β
n : α
inst✝ : RingHomClass F α β
f : F
m : α
⊢ Odd (↑f (2 * m + 1))
exact ⟨f m, by simp [two_mul]⟩
no goals
F : Type u_1
α : Type u_2
β : Type u_3
R : Type ?u.86642
inst✝² : Semiring α
inst✝¹ : Semiring β
n : α
inst✝ : RingHomClass F α β
f : F
m : α
⊢ ↑f (2 * m + 1) = 2 * ↑f m + 1
simp [two_mul]