Theorem: Lean4Axiomatic.Natural.step_neqv (Lean4Axiomatic/Natural/Core.lean)

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step n ≄ n
Tactic:
apply ind_on (motive := λ n => step n ≄ n) n
State after:
case zero
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step 0 ≄ 0

case step
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step 0 ≄ 0
Tactic:
case zero =>
  show step 0 ≄ 0
  exact step_neqv_zero
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m
Tactic:
case step =>
  intro n (ih : step n ≄ n)
  show step (step n) ≄ step n
  intro (_ : step (step n) ≃ step n)
  show False
  apply ih
  show step n ≃ n
  exact AA.inject ‹step (step n) ≃ step n›
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step 0 ≄ 0
Tactic:
exact step_neqv_zero
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m
Tactic:
intro n (ih : step n ≄ n)
State after:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
⊢ step (step n) ≄ step n

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
⊢ step (step n) ≄ step n
Tactic:
intro (_ : step (step n) ≃ step n)
State after:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ False

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ False
Tactic:
apply ih
State after:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ step n ≃ n

State before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ step n ≃ n
Tactic:
exact AA.inject ‹step (step n) ≃ step n›
State after:
no goals