internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.lt_substL_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝ : n₁ + m ≤ n₂ + m
this : n₁ + m ≄ n₂ + m
⊢ n₁ + m < n₂ + m
Tactic:
have : n₁ + m < n₂ + m :=
  lt_defn.mpr (And.intro ‹n₁ + m ≤ n₂ + m› ‹n₁ + m ≄ n₂ + m›)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝¹ : n₁ + m ≤ n₂ + m
this✝ : n₁ + m ≄ n₂ + m
this : n₁ + m < n₂ + m
⊢ n₁ + m < n₂ + m
Theorem: Lean4Axiomatic.Natural.lt_substL_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝¹ : n₁ + m ≤ n₂ + m
this✝ : n₁ + m ≄ n₂ + m
this : n₁ + m < n₂ + m
⊢ n₁ + m < n₂ + m
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_substR_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
⊢ n₁ < n₂ → m + n₁ < m + n₂
Tactic:
intro (_ : n₁ < n₂)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
⊢ m + n₁ < m + n₂
Theorem: Lean4Axiomatic.Natural.lt_substR_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
⊢ m + n₁ < m + n₂
Tactic:
have : n₁ + m < n₂ + m := lt_substL_add ‹n₁ < n₂›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
this : n₁ + m < n₂ + m
⊢ m + n₁ < m + n₂
Theorem: Lean4Axiomatic.Natural.lt_substR_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
this : n₁ + m < n₂ + m
⊢ m + n₁ < m + n₂
Tactic:
have : m + n₁ < n₂ + m := AA.substLFn AA.comm ‹n₁ + m < n₂ + m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
this✝ : n₁ + m < n₂ + m
this : m + n₁ < n₂ + m
⊢ m + n₁ < m + n₂
Theorem: Lean4Axiomatic.Natural.lt_substR_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
this✝ : n₁ + m < n₂ + m
this : m + n₁ < n₂ + m
⊢ m + n₁ < m + n₂
Tactic:
have : m + n₁ < m + n₂ := AA.substRFn AA.comm ‹m + n₁ < n₂ + m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
this✝¹ : n₁ + m < n₂ + m
this✝ : m + n₁ < n₂ + m
this : m + n₁ < m + n₂
⊢ m + n₁ < m + n₂
Theorem: Lean4Axiomatic.Natural.lt_substR_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
this✝¹ : n₁ + m < n₂ + m
this✝ : m + n₁ < n₂ + m
this : m + n₁ < m + n₂
⊢ m + n₁ < m + n₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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))
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof 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)
Theorem: Lean4Axiomatic.Natural.trichotomy
Proof 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›
Proof 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)