case intro.intro
F : Type ?u.83706
α : Type u_1
β : Type ?u.83712
R : Type ?u.83715
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Even (2 * m + 1 + (2 * n + 1))
F : Type ?u.83706
α : Type u_1
β : Type ?u.83712
R : Type ?u.83715
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd m → Odd n → Even (m + n)
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
case intro.intro
F : Type ?u.83706
α : Type u_1
β : Type ?u.83712
R : Type ?u.83715
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ 2 * m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1)
case intro.intro
F : Type ?u.83706
α : Type u_1
β : Type ?u.83712
R : Type ?u.83715
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Even (2 * m + 1 + (2 * n + 1))
refine' ⟨n + m + 1, _⟩
case intro.intro
F : Type ?u.83706
α : Type u_1
β : Type ?u.83712
R : Type ?u.83715
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ m + m + 1 + (n + n + 1) = n + m + 1 + (n + m + 1)
case intro.intro
F : Type ?u.83706
α : Type u_1
β : Type ?u.83712
R : Type ?u.83715
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ 2 * m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1)
rw [two_mul, two_mul]
no goals
case intro.intro
F : Type ?u.83706
α : Type u_1
β : Type ?u.83712
R : Type ?u.83715
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ m + m + 1 + (n + n + 1) = n + m + 1 + (n + m + 1)
ac_rfl