Theorem: MyNat.lt_aux_one (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ a ≤ b ∧ ¬b ≤ a → succ a ≤ b
Tactic:
intro h
State after:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
⊢ succ a ≤ b

State before:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
⊢ succ a ≤ b
Tactic:
let ⟨⟨w, pw⟩, hc⟩ := h
State after:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
w : Nat
pw : b = a + w
hc : ¬b ≤ a
⊢ succ a ≤ b

State before:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
w : Nat
pw : b = a + w
hc : ¬b ≤ a
⊢ succ a ≤ b
Tactic:
cases w with
| zero =>
  rw [add_zero] at pw
  have _ : b ≤ a := pw ▸ (le_refl b)  contradiction
| succ w' =>
  exists w'
  rw [pw, add_succ, succ_add]
State after:
no goals

State before:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a + zero
⊢ succ a ≤ b
Tactic:
rw [add_zero] at pw
State after:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
⊢ succ a ≤ b

State before:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
⊢ succ a ≤ b
Tactic:
have _ : b ≤ a := pw ▸ (le_refl b)
State after:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
x✝ : b ≤ a
⊢ succ a ≤ b

State before:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
x✝ : b ≤ a
⊢ succ a ≤ b
Tactic:
contradiction
State after:
no goals

State before:
case succ
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
w' : Nat
pw : b = a + succ w'
⊢ succ a ≤ b
Tactic:
exists w'
State after:
case succ
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
w' : Nat
pw : b = a + succ w'
⊢ b = succ a + w'

State before:
case succ
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
w' : Nat
pw : b = a + succ w'
⊢ b = succ a + w'
Tactic:
rw [pw, add_succ, succ_add]
State after:
no goals