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

State before:
a b : Nat
⊢ succ a ≤ b → a ≤ b ∧ ¬b ≤ a
Tactic:
intro
| ⟨w , pw⟩  =>
  constructor
  case left =>
    exists (w + one)
    rw [pw, succ_eq_add_one]
    simp
  case right =>
    intro
    have _ : succ a ≤ b := by exists w
    have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
    apply (@not_succ_le_self a)
    assumption
State after:
no goals

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b ∧ ¬b ≤ a
Tactic:
constructor
State after:
case left
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b

case right
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ ¬b ≤ a

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b
Tactic:
case left =>
  exists (w + one)
  rw [pw, succ_eq_add_one]
  simp
State after:
no goals

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ ¬b ≤ a
Tactic:
case right =>
  intro
  have _ : succ a ≤ b := by exists w
  have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
  apply (@not_succ_le_self a)
  assumption
State after:
no goals

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b
Tactic:
exists (w + one)
State after:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ b = a + (w + one)

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ b = a + (w + one)
Tactic:
rw [pw, succ_eq_add_one]
State after:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a + one + w = a + (w + one)

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a + one + w = a + (w + one)
Tactic:
simp
State after:
no goals

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ ¬b ≤ a
Tactic:
intro
State after:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
⊢ False

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
⊢ False
Tactic:
have _ : succ a ≤ b := by exists w
State after:
a b : Nat
x✝¹ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝ : succ a ≤ b
⊢ False

State before:
a b : Nat
x✝¹ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝ : succ a ≤ b
⊢ False
Tactic:
have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
State after:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ False

State before:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ False
Tactic:
apply (@not_succ_le_self a)
State after:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ succ a ≤ a

State before:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ succ a ≤ a
Tactic:
assumption
State after:
no goals

State before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
⊢ succ a ≤ b
Tactic:
exists w
State after:
no goals

State before:
a b : Nat
x✝¹ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝ : succ a ≤ b
⊢ succ a ≤ a
Tactic:
apply (@le_trans (succ a) b) <;> assumption
State after:
no goals