Theorem: Lean4Axiomatic.Natural.positive_add (Lean4Axiomatic/Natural/Sign.lean)

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + m)
Tactic:
apply cases_on (motive := λ m => Positive (n + m)) m
State after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)
Tactic:
case zero =>
  show Positive (n + 0)
  apply AA.substFn (Rel.symm add_zero)
  exact ‹Positive n›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)
Tactic:
case step =>
  intro m
  show Positive (n + step m)
  apply AA.substFn (Rel.symm add_step)
  show Positive (step (n + m))
  apply Signed.positive_defn.mpr
  show step (n + m) ≄ 0
  exact step_neqv_zero
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)
Tactic:
apply AA.substFn (Rel.symm add_zero)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive n

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive n
Tactic:
exact ‹Positive n›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)
Tactic:
intro m
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (n + step m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (n + step m)
Tactic:
apply AA.substFn (Rel.symm add_step)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (step (n + m))

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (step (n + m))
Tactic:
apply Signed.positive_defn.mpr
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ step (n + m) ≄ 0

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ step (n + m) ≄ 0
Tactic:
exact step_neqv_zero
State after:
no goals