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

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

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n → n ≥ 1
Tactic:
case mp =>
  intro (_ : Positive n)
  show n ≥ 1
  have : n > 0 := lt_zero_pos.mp ‹Positive n›
  have : n ≥ step 0 := lt_step_le.mp this
  have : n ≥ 1 := AA.substLFn (Rel.symm literal_step) this
  exact this
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≥ 1 → Positive n
Tactic:
case mpr =>
  intro (_ : n ≥ 1)
  show Positive n
  have : n ≥ step 0 := AA.substLFn literal_step ‹n ≥ 1›
  have : n > 0 := lt_step_le.mpr this
  have : Positive n := lt_zero_pos.mpr this
  exact this
State after:
no goals

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n ≥ 1
Tactic:
have : n > 0 := lt_zero_pos.mp ‹Positive n›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this : n > 0
⊢ n ≥ 1

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this : n > 0
⊢ n ≥ 1
Tactic:
have : n ≥ step 0 := lt_step_le.mp this
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝ : n > 0
this : n ≥ step 0
⊢ n ≥ 1

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝ : n > 0
this : n ≥ step 0
⊢ n ≥ 1
Tactic:
have : n ≥ 1 := AA.substLFn (Rel.symm literal_step) this
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝¹ : n > 0
this✝ : n ≥ step 0
this : n ≥ 1
⊢ n ≥ 1

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝¹ : n > 0
this✝ : n ≥ step 0
this : n ≥ 1
⊢ n ≥ 1
Tactic:
exact this
State after:
no goals

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
⊢ Positive n
Tactic:
have : n ≥ step 0 := AA.substLFn literal_step ‹n ≥ 1›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this : n ≥ step 0
⊢ Positive n

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this : n ≥ step 0
⊢ Positive n
Tactic:
have : n > 0 := lt_step_le.mpr this
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝ : n ≥ step 0
this : n > 0
⊢ Positive n

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝ : n ≥ step 0
this : n > 0
⊢ Positive n
Tactic:
have : Positive n := lt_zero_pos.mpr this
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝¹ : n ≥ step 0
this✝ : n > 0
this : Positive n
⊢ Positive n

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝¹ : n ≥ step 0
this✝ : n > 0
this : Positive n
⊢ Positive n
Tactic:
exact this
State after:
no goals