case intro.intro
F : Type ?u.88859
α : Type u_1
β : Type ?u.88865
R : Type ?u.88868
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd ((2 * m + 1) * (2 * n + 1))
F : Type ?u.88859
α : Type u_1
β : Type ?u.88865
R : Type ?u.88868
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd m → Odd n → Odd (m * n)
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
case intro.intro
F : Type ?u.88859
α : Type u_1
β : Type ?u.88865
R : Type ?u.88868
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ (2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1
case intro.intro
F : Type ?u.88859
α : Type u_1
β : Type ?u.88865
R : Type ?u.88868
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd ((2 * m + 1) * (2 * n + 1))
refine' ⟨2 * m * n + n + m, _⟩
no goals
case intro.intro
F : Type ?u.88859
α : Type u_1
β : Type ?u.88865
R : Type ?u.88868
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ (2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1
rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
  ← Nat.cast_two, ← Nat.cast_comm]