no goals
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
h : m = 0
⊢ False
simp_all
no goals
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hm0 : 0 < m
h : n = 0
⊢ False
simp_all
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hm0 : 0 < m
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hm0 : 0 < m
hn0 : 0 < n
⊢ (fun x x_1 => x * x_1) 2 (m * n / 2) = (fun x x_1 => x * x_1) 2 (m * (n / 2) + m / 2)
dsimp
no goals
m✝ n✝ a b c d m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hm0 : 0 < m
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
  two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), mul_tsub, mul_one, ←
  add_tsub_assoc_of_le (succ_le_of_lt hm0),
  tsub_add_cancel_of_le (le_mul_of_one_le_right (Nat.zero_le _) hn0)]