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

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

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ ∀ (m : ℕ), Positive (step m) → ∃ m_1, step m_1 ≃ step m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive 0 → ∃ m, step m ≃ 0
Tactic:
case zero =>
  intro (_ : Positive (0:ℕ))
  apply False.elim
  show False
  have : (0:ℕ) ≄ 0 := Signed.positive_defn.mp ‹Positive (0:ℕ)›
  apply this
  show 0 ≃ 0
  exact Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ ∀ (m : ℕ), Positive (step m) → ∃ m_1, step m_1 ≃ step m
Tactic:
case step =>
  intro n (_ : Positive (step n))
  exists n
  show step n ≃ step n
  exact Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
⊢ ∃ m, step m ≃ 0
Tactic:
apply False.elim
State after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
⊢ False

State before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
⊢ False
Tactic:
have : (0:ℕ) ≄ 0 := Signed.positive_defn.mp ‹Positive (0:ℕ)›
State after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ False

State before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ False
Tactic:
apply this
State after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ 0 ≃ 0

State before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ 0 ≃ 0
Tactic:
exact Rel.refl
State after:
no goals

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

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n✝ n : ℕ
x✝ : Positive (step n)
⊢ step n ≃ step n
Tactic:
exact Rel.refl
State after:
no goals