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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
Tactic:
constructor
State after:
case atLeastOne
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ AA.OneOfThree (n < m) (n ≃ m) (n > m)

case atMostOne
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ ¬AA.TwoOfThree (n < m) (n ≃ m) (n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ ¬AA.TwoOfThree (n < m) (n ≃ m) (n > m)
Tactic:
case atMostOne =>
  show ¬ AA.TwoOfThree (n < m) (n ≃ m) (n > m)
  intro
  | AA.TwoOfThree.oneAndTwo (_ : n < m) (_ : n ≃ m) =>
    show False
    have ⟨_, (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
    exact absurd ‹n ≃ m› ‹n ≄ m›
  | AA.TwoOfThree.oneAndThree (_ : n < m) (_ : n > m) =>
    show False
    have ⟨(_ : n ≤ m), (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
    have ⟨(_ : m ≤ n), _⟩ := lt_defn.mp ‹n > m›
    have : n ≃ m := le_antisymm ‹n ≤ m› ‹m ≤ n›
    exact absurd ‹n ≃ m› ‹n ≄ m›
  | AA.TwoOfThree.twoAndThree (_ : n ≃ m) (_ : n > m) =>
    show False
    have ⟨_, (_ : m ≄ n)⟩ := lt_defn.mp ‹n > m›
    exact absurd ‹n ≃ m› (Rel.symm ‹m ≄ n›)
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ AA.OneOfThree (n < m) (n ≃ m) (n > m)
Tactic:
let motive := λ n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (n < m) (n ≃ m) (n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (n < m) (n ≃ m) (n > m)
Tactic:
apply ind_on (motive := motive) n
State after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ motive 0

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ ∀ (m : ℕ), motive m → motive (step m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ ∀ (m : ℕ), motive m → motive (step m)
Tactic:
case step =>
  intro n (ih : AA.OneOfThree (n < m) (n ≃ m) (n > m))
  show AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
  match ih with
  | AA.OneOfThree.first (_ : n < m) =>
    have : step n ≤ m := lt_step_le.mp ‹n < m›
    have : step n < m ∨ step n ≃ m := le_split ‹step n ≤ m›
    match ‹step n < m ∨ step n ≃ m› with
    | Or.inl (_ : step n < m) => exact AA.OneOfThree.first ‹step n < m›
    | Or.inr (_ : step n ≃ m) => exact AA.OneOfThree.second ‹step n ≃ m›
  | AA.OneOfThree.second (_ : n ≃ m) =>
    have : m ≃ n := Rel.symm ‹n ≃ m›
    have : m ≤ n := le_from_eqv ‹m ≃ n›
    have : step m ≤ step n := AA.subst₁ ‹m ≤ n›
    have : m < step n := lt_step_le.mpr ‹step m ≤ step n›
    apply AA.OneOfThree.third
    exact ‹m < step n›
  | AA.OneOfThree.third (_ : n > m) =>
    apply AA.OneOfThree.third
    show m < step n
    exact lt_trans ‹m < n› lt_step
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ motive 0
Tactic:
show AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
Tactic:
let motive := λ m : ℕ => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
Tactic:
apply cases_on (motive := motive) m
State after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ motive 0

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ ∀ (m : ℕ), motive (step m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ motive 0
Tactic:
case zero =>
  apply AA.OneOfThree.second
  show 0 ≃ 0
  exact Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ motive 0
Tactic:
apply AA.OneOfThree.second
State after:
case b
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ 0 ≃ 0

State before:
case b
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ 0 ≃ 0
Tactic:
exact Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
⊢ ∀ (m : ℕ), motive (step m)
Tactic:
intro m
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ motive (step m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ motive (step m)
Tactic:
apply AA.OneOfThree.first
State after:
case a
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 < step m

State before:
case a
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 < step m
Tactic:
apply lt_defn.mpr
State after:
case a
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 ≤ step m ∧ 0 ≄ step m

State before:
case a
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 ≤ step m ∧ 0 ≄ step m
Tactic:
apply And.intro
State after:
case a.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 ≤ step m

case a.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 ≄ step m

State before:
case a.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 ≤ step m
Tactic:
apply le_defn.mpr
State after:
case a.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ ∃ k, 0 + k ≃ step m

State before:
case a.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ ∃ k, 0 + k ≃ step m
Tactic:
exists step m
State after:
case a.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 + step m ≃ step m

State before:
case a.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 + step m ≃ step m
Tactic:
exact zero_add
State after:
no goals

State before:
case a.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m✝ : ℕ
motive✝ : ℕ → Prop := fun n => AA.OneOfThree (n < m✝) (n ≃ m✝) (n > m✝)
motive : ℕ → Prop := fun m => AA.OneOfThree (0 < m) (0 ≃ m) (0 > m)
m : ℕ
⊢ 0 ≄ step m
Tactic:
exact Rel.symm step_neqv_zero
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ ∀ (m : ℕ), motive m → motive (step m)
Tactic:
intro n (ih : AA.OneOfThree (n < m) (n ≃ m) (n > m))
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ motive (step n)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ motive (step n)
Tactic:
show AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
match ih with
| AA.OneOfThree.first (_ : n < m) =>
  have : step n ≤ m := lt_step_le.mp ‹n < m›
  have : step n < m ∨ step n ≃ m := le_split ‹step n ≤ m›
  match ‹step n < m ∨ step n ≃ m› with
  | Or.inl (_ : step n < m) => exact AA.OneOfThree.first ‹step n < m›
  | Or.inr (_ : step n ≃ m) => exact AA.OneOfThree.second ‹step n ≃ m›
| AA.OneOfThree.second (_ : n ≃ m) =>
  have : m ≃ n := Rel.symm ‹n ≃ m›
  have : m ≤ n := le_from_eqv ‹m ≃ n›
  have : step m ≤ step n := AA.subst₁ ‹m ≤ n›
  have : m < step n := lt_step_le.mpr ‹step m ≤ step n›
  apply AA.OneOfThree.third
  exact ‹m < step n›
| AA.OneOfThree.third (_ : n > m) =>
  apply AA.OneOfThree.third
  show m < step n
  exact lt_trans ‹m < n› lt_step
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
have : step n ≤ m := lt_step_le.mp ‹n < m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this : step n ≤ m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this : step n ≤ m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
have : step n < m ∨ step n ≃ m := le_split ‹step n ≤ m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝ : step n ≤ m
this : step n < m ∨ step n ≃ m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝ : step n ≤ m
this : step n < m ∨ step n ≃ m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
match ‹step n < m ∨ step n ≃ m› with
| Or.inl (_ : step n < m) => exact AA.OneOfThree.first ‹step n < m›
| Or.inr (_ : step n ≃ m) => exact AA.OneOfThree.second ‹step n ≃ m›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝ : step n ≤ m
this : step n < m ∨ step n ≃ m
h✝ : step n < m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
exact AA.OneOfThree.first ‹step n < m›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this✝ : step n ≤ m
this : step n < m ∨ step n ≃ m
h✝ : step n ≃ m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
exact AA.OneOfThree.second ‹step n ≃ m›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
have : m ≃ n := Rel.symm ‹n ≃ m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this : m ≃ n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this : m ≃ n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
have : m ≤ n := le_from_eqv ‹m ≃ n›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝ : m ≃ n
this : m ≤ n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝ : m ≃ n
this : m ≤ n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
have : step m ≤ step n := AA.subst₁ ‹m ≤ n›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝¹ : m ≃ n
this✝ : m ≤ n
this : step m ≤ step n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝¹ : m ≃ n
this✝ : m ≤ n
this : step m ≤ step n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
have : m < step n := lt_step_le.mpr ‹step m ≤ step n›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
apply AA.OneOfThree.third
State after:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ step n > m

State before:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this✝² : m ≃ n
this✝¹ : m ≤ n
this✝ : step m ≤ step n
this : m < step n
⊢ step n > m
Tactic:
exact ‹m < step n›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
Tactic:
apply AA.OneOfThree.third
State after:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ step n > m

State before:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ step n > m
Tactic:
show m < step n
State after:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ m < step n

State before:
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ m < step n
Tactic:
exact lt_trans ‹m < n› lt_step
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ ¬AA.TwoOfThree (n < m) (n ≃ m) (n > m)
Tactic:
intro
| AA.TwoOfThree.oneAndTwo (_ : n < m) (_ : n ≃ m) =>
  show False
  have ⟨_, (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
  exact absurd ‹n ≃ m› ‹n ≄ m›
| AA.TwoOfThree.oneAndThree (_ : n < m) (_ : n > m) =>
  show False
  have ⟨(_ : n ≤ m), (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
  have ⟨(_ : m ≤ n), _⟩ := lt_defn.mp ‹n > m›
  have : n ≃ m := le_antisymm ‹n ≤ m› ‹m ≤ n›
  exact absurd ‹n ≃ m› ‹n ≄ m›
| AA.TwoOfThree.twoAndThree (_ : n ≃ m) (_ : n > m) =>
  show False
  have ⟨_, (_ : m ≄ n)⟩ := lt_defn.mp ‹n > m›
  exact absurd ‹n ≃ m› (Rel.symm ‹m ≄ n›)
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
b✝ : n ≃ m
⊢ False
Tactic:
have ⟨_, (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
b✝ : n ≃ m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
b✝ : n ≃ m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False
Tactic:
exact absurd ‹n ≃ m› ‹n ≄ m›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
⊢ False
Tactic:
have ⟨(_ : n ≤ m), (_ : n ≄ m)⟩ := lt_defn.mp ‹n < m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ False
Tactic:
have ⟨(_ : m ≤ n), _⟩ := lt_defn.mp ‹n > m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False
Tactic:
have : n ≃ m := le_antisymm ‹n ≤ m› ‹m ≤ n›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
this : n ≃ m
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
c✝ : n > m
left✝¹ : n ≤ m
right✝¹ : n ≄ m
left✝ : m ≤ n
right✝ : m ≄ n
this : n ≃ m
⊢ False
Tactic:
exact absurd ‹n ≃ m› ‹n ≄ m›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
c✝ : n > m
⊢ False
Tactic:
have ⟨_, (_ : m ≄ n)⟩ := lt_defn.mp ‹n > m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
c✝ : n > m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
c✝ : n > m
left✝ : m ≤ n
right✝ : m ≄ n
⊢ False
Tactic:
exact absurd ‹n ≃ m› (Rel.symm ‹m ≄ n›)
State after:
no goals