Theorem: Lean4Axiomatic.Natural.lt_zero (Lean4Axiomatic/Natural/Order.lean)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≮ 0
Tactic:
intro (_ : n < 0)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
⊢ False
Tactic:
have : step n ≤ 0 := lt_step_le.mp ‹n < 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
⊢ False
Tactic:
have ⟨d, (_ : step n + d ≃ 0)⟩ := le_defn.mp ‹step n ≤ 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
⊢ False
Tactic:
have : step (n + d) ≃ 0 := calc
  step (n + d) ≃ _ := Rel.symm step_add
  step n + d   ≃ _ := ‹step n + d ≃ 0›
  0            ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this✝ : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
this : step (n + d) ≃ 0
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this✝ : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
this : step (n + d) ≃ 0
⊢ False
Tactic:
exact absurd ‹step (n + d) ≃ 0› step_neqv_zero
State after:
no goals