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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n ↔ n > 0
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n → n > 0

case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n > 0 → Positive n

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n → n > 0
Tactic:
intro (_ : Positive n)
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n > 0

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n > 0
Tactic:
show 0 < n
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ 0 < n

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ 0 < n
Tactic:
apply lt_defn_add.mpr
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ ∃ k, Positive k ∧ n ≃ 0 + k

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ ∃ k, Positive k ∧ n ≃ 0 + k
Tactic:
exists n
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n ∧ n ≃ 0 + n

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n ∧ n ≃ 0 + n
Tactic:
apply And.intro
State after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n

case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n ≃ 0 + n

State before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n
Tactic:
exact ‹Positive n›
State after:
no goals

State before:
case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n ≃ 0 + n
Tactic:
exact Rel.symm zero_add
State after:
no goals

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n > 0 → Positive n
Tactic:
intro (_ : 0 < n)
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
⊢ Positive n

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
⊢ Positive n
Tactic:
have ⟨k, ⟨(_ : Positive k), (_ : n ≃ 0 + k)⟩⟩ := lt_defn_add.mp ‹0 < n›
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
⊢ Positive n

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
⊢ Positive n
Tactic:
have : k ≃ n := Rel.symm (Rel.trans ‹n ≃ 0 + k› zero_add)
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
this : k ≃ n
⊢ Positive n

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
this : k ≃ n
⊢ Positive n
Tactic:
exact AA.substFn ‹k ≃ n› ‹Positive k›
State after:
no goals