case intro.intro
F : Type ?u.81616
α : Type u_1
β : Type ?u.81622
R : Type ?u.81625
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + m + (2 * n + 1))
F : Type ?u.81616
α : Type u_1
β : Type ?u.81622
R : Type ?u.81625
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Even m → Odd n → Odd (m + n)
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
no goals
case intro.intro
F : Type ?u.81616
α : Type u_1
β : Type ?u.81622
R : Type ?u.81625
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + m + (2 * n + 1))
exact ⟨m + n, by rw [mul_add, ← two_mul, add_assoc]⟩
no goals
F : Type ?u.81616
α : Type u_1
β : Type ?u.81622
R : Type ?u.81625
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ m + m + (2 * n + 1) = 2 * (m + n) + 1
rw [mul_add, ← two_mul, add_assoc]