n : ℕ
this : bodd (n % 2 + 2 * (n / 2)) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
n : ℕ
⊢ n % 2 = bif bodd n then 1 else 0
have := congr_arg bodd (mod_add_div n 2)
n : ℕ
this : bodd (n % 2) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
n : ℕ
this : bodd (n % 2 + 2 * (n / 2)) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
simp [not] at this
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ n % 2 = bif bodd n then 1 else 0
n : ℕ
this : bodd (n % 2) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
have _ : ∀ b, and false b = false := by
  intro b
  cases b <;> rfl
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd n then 1 else 0
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ n % 2 = bif bodd n then 1 else 0
have _ : ∀ b, bxor b false = b := by
  intro b
  cases b <;> rfl
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd n then 1 else 0
rw [← this]
no goals
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
cases' mod_two_eq_zero_or_one n with h h <;> rw [h] <;> rfl
n : ℕ
this : bodd (n % 2) = bodd n
b : Bool
⊢ (false && b) = false
n : ℕ
this : bodd (n % 2) = bodd n
⊢ ∀ (b : Bool), (false && b) = false
intro b
no goals
n : ℕ
this : bodd (n % 2) = bodd n
b : Bool
⊢ (false && b) = false
cases b <;> rfl
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
b : Bool
⊢ bxor b false = b
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ ∀ (b : Bool), bxor b false = b
intro b
no goals
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
b : Bool
⊢ bxor b false = b
cases b <;> rfl