Theorem: Misc.Nat.even_pred_of_odd (LeanSAT/Util/Misc.lean)

State before:
n : Nat
h : n > 0
⊢ Odd n → Even (n - 1)
Tactic:
intro
State after:
n : Nat
h : n > 0
a✝ : Odd n
⊢ Even (n - 1)

State before:
n : Nat
h : n > 0
a✝ : Odd n
⊢ Even (n - 1)
Tactic:
apply Classical.byContradiction
State after:
case h
n : Nat
h : n > 0
a✝ : Odd n
⊢ ¬Even (n - 1) → False

State before:
case h
n : Nat
h : n > 0
a✝ : Odd n
⊢ ¬Even (n - 1) → False
Tactic:
intro h'
State after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
⊢ False
Tactic:
have := Iff.mpr Nat.odd_iff_not_even h'
State after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this : Odd (n - 1)
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this : Odd (n - 1)
⊢ False
Tactic:
have : Even (n - 1 + 1) := Nat.even_succ_of_odd this
State after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even (n - 1 + 1)
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even (n - 1 + 1)
⊢ False
Tactic:
rw [Nat.sub_add_cancel h] at this
State after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even n
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝ : Odd (n - 1)
this : Even n
⊢ False
Tactic:
have := Iff.mpr Nat.not_odd_iff_even this
State after:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝¹ : Odd (n - 1)
this✝ : Even n
this : ¬Odd n
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Odd n
h' : ¬Even (n - 1)
this✝¹ : Odd (n - 1)
this✝ : Even n
this : ¬Odd n
⊢ False
Tactic:
contradiction
State after:
no goals