internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ n < m
Tactic:
apply lt_step_le.mpr
Proof state after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ step n ≤ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ step n ≤ m
Tactic:
apply le_defn.mpr
Proof state after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ ∃ k, step n + k ≃ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ ∃ k, step n + k ≃ m
Tactic:
exists d
Proof state after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ step n + d ≃ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ step n + d ≃ m
Tactic:
calc
  step n + d   ≃ _ := step_add
  step (n + d) ≃ _ := Rel.symm add_step
  n + step d   ≃ _ := ‹n + step d ≃ m›
  m            ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n ≥ m → n > m ∨ n ≃ m
Tactic:
intro (_ : n ≥ m)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
⊢ n > m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
⊢ n > m ∨ n ≃ m
Tactic:
have : m ≤ n := ‹n ≥ m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this : m ≤ n
⊢ n > m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this : m ≤ n
⊢ n > m ∨ n ≃ m
Tactic:
have : m < n ∨ m ≃ n := le_split this
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝ : m ≤ n
this : m < n ∨ m ≃ n
⊢ n > m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝ : m ≤ n
this : m < n ∨ m ≃ n
⊢ n > m ∨ n ≃ m
Tactic:
match this with
| Or.inl (_ : m < n) =>
  have : n > m := ‹m < n›
  exact Or.inl this
| Or.inr (_ : m ≃ n) =>
  have : n ≃ m := Rel.symm ‹m ≃ n›
  exact Or.inr this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝ : m ≤ n
this : m < n ∨ m ≃ n
h✝ : m < n
⊢ n > m ∨ n ≃ m
Tactic:
have : n > m := ‹m < n›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝¹ : m ≤ n
this✝ : m < n ∨ m ≃ n
h✝ : m < n
this : n > m
⊢ n > m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝¹ : m ≤ n
this✝ : m < n ∨ m ≃ n
h✝ : m < n
this : n > m
⊢ n > m ∨ n ≃ m
Tactic:
exact Or.inl this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝ : m ≤ n
this : m < n ∨ m ≃ n
h✝ : m ≃ n
⊢ n > m ∨ n ≃ m
Tactic:
have : n ≃ m := Rel.symm ‹m ≃ n›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝¹ : m ≤ n
this✝ : m < n ∨ m ≃ n
h✝ : m ≃ n
this : n ≃ m
⊢ n > m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.ge_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≥ m
this✝¹ : m ≤ n
this✝ : m < n ∨ m ≃ n
h✝ : m ≃ n
this : n ≃ m
⊢ n > m ∨ n ≃ m
Tactic:
exact Or.inr this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n ↔ n ≥ 1
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n → n ≥ 1

case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≥ 1 → Positive n
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n → n ≥ 1
Tactic:
case mp =>
  intro (_ : Positive n)
  show n ≥ 1
  have : n > 0 := lt_zero_pos.mp ‹Positive n›
  have : n ≥ step 0 := lt_step_le.mp this
  have : n ≥ 1 := AA.substLFn (Rel.symm literal_step) this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≥ 1 → Positive n
Tactic:
case mpr =>
  intro (_ : n ≥ 1)
  show Positive n
  have : n ≥ step 0 := AA.substLFn literal_step ‹n ≥ 1›
  have : n > 0 := lt_step_le.mpr this
  have : Positive n := lt_zero_pos.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n → n ≥ 1
Tactic:
intro (_ : Positive n)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n ≥ 1
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n ≥ 1
Tactic:
have : n > 0 := lt_zero_pos.mp ‹Positive n›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this : n > 0
⊢ n ≥ 1
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this : n > 0
⊢ n ≥ 1
Tactic:
have : n ≥ step 0 := lt_step_le.mp this
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝ : n > 0
this : n ≥ step 0
⊢ n ≥ 1
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝ : n > 0
this : n ≥ step 0
⊢ n ≥ 1
Tactic:
have : n ≥ 1 := AA.substLFn (Rel.symm literal_step) this
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝¹ : n > 0
this✝ : n ≥ step 0
this : n ≥ 1
⊢ n ≥ 1
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
this✝¹ : n > 0
this✝ : n ≥ step 0
this : n ≥ 1
⊢ n ≥ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≥ 1 → Positive n
Tactic:
intro (_ : n ≥ 1)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
⊢ Positive n
Tactic:
have : n ≥ step 0 := AA.substLFn literal_step ‹n ≥ 1›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this : n ≥ step 0
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this : n ≥ step 0
⊢ Positive n
Tactic:
have : n > 0 := lt_step_le.mpr this
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝ : n ≥ step 0
this : n > 0
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝ : n ≥ step 0
this : n > 0
⊢ Positive n
Tactic:
have : Positive n := lt_zero_pos.mpr this
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝¹ : n ≥ step 0
this✝ : n > 0
this : Positive n
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.positive_ge
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this✝¹ : n ≥ step 0
this✝ : n > 0
this : Positive n
⊢ Positive n
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < step m → n < m ∨ n ≃ m
Tactic:
intro (_ : n < step m)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
⊢ n < m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.lt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
⊢ n < m ∨ n ≃ m
Tactic:
have : step n ≤ step m := lt_step_le.mp ‹n < step m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
this : step n ≤ step m
⊢ n < m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.lt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
this : step n ≤ step m
⊢ n < m ∨ n ≃ m
Tactic:
have : n ≤ m := AA.inject ‹step n ≤ step m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
this✝ : step n ≤ step m
this : n ≤ m
⊢ n < m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.lt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
this✝ : step n ≤ step m
this : n ≤ m
⊢ n < m ∨ n ≃ m
Tactic:
exact le_split ‹n ≤ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.gt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ step m > n → m ≃ n ∨ m > n
Tactic:
intro (_ : step m > n)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
⊢ m ≃ n ∨ m > n
Theorem: Lean4Axiomatic.Natural.gt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
⊢ m ≃ n ∨ m > n
Tactic:
have : n < m ∨ n ≃ m := lt_split ‹n < step m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this : n < m ∨ n ≃ m
⊢ m ≃ n ∨ m > n
Theorem: Lean4Axiomatic.Natural.gt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this : n < m ∨ n ≃ m
⊢ m ≃ n ∨ m > n
Tactic:
match this with
| Or.inl (_ : n < m) =>
  have : m ≃ n ∨ m > n := Or.inr ‹m > n›
  exact this
| Or.inr (_ : n ≃ m) =>
  have : m ≃ n ∨ m > n := Or.inl (Rel.symm ‹n ≃ m›)
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.gt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this : n < m ∨ n ≃ m
h✝ : n < m
⊢ m ≃ n ∨ m > n
Tactic:
have : m ≃ n ∨ m > n := Or.inr ‹m > n›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this✝ : n < m ∨ n ≃ m
h✝ : n < m
this : m ≃ n ∨ m > n
⊢ m ≃ n ∨ m > n
Theorem: Lean4Axiomatic.Natural.gt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this✝ : n < m ∨ n ≃ m
h✝ : n < m
this : m ≃ n ∨ m > n
⊢ m ≃ n ∨ m > n
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.gt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this : n < m ∨ n ≃ m
h✝ : n ≃ m
⊢ m ≃ n ∨ m > n
Tactic:
have : m ≃ n ∨ m > n := Or.inl (Rel.symm ‹n ≃ m›)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this✝ : n < m ∨ n ≃ m
h✝ : n ≃ m
this : m ≃ n ∨ m > n
⊢ m ≃ n ∨ m > n
Theorem: Lean4Axiomatic.Natural.gt_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : step m > n
this✝ : n < m ∨ n ≃ m
h✝ : n ≃ m
this : m ≃ n ∨ m > n
⊢ m ≃ n ∨ m > n
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
⊢ n < m → m < k → n < k
Tactic:
intro (_ : n < m) (_ : m < k)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.lt_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ n < k
Tactic:
apply lt_step_le.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ step n ≤ k
Theorem: Lean4Axiomatic.Natural.lt_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ step n ≤ k
Tactic:
calc
  step n ≤ _ := lt_step_le.mp ‹n < m›
  m      ≤ _ := le_from_lt lt_step
  step m ≤ _ := lt_step_le.mp ‹m < k›
  k      ≤ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_lt_le_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
⊢ n < m → m ≤ k → n < k
Tactic:
intro (_ : n < m) (_ : m ≤ k)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_lt_le_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
⊢ n < k
Tactic:
have : m < k ∨ m ≃ k := le_split ‹m ≤ k›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this : m < k ∨ m ≃ k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_lt_le_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this : m < k ∨ m ≃ k
⊢ n < k
Tactic:
match this with
| Or.inl (_ : m < k) =>
  have : n < k := lt_trans ‹n < m› ‹m < k›
  exact this
| Or.inr (_ : m ≃ k) =>
  have : n < k := trans_lt_eqv_lt ‹n < m› ‹m ≃ k›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_lt_le_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this : m < k ∨ m ≃ k
h✝ : m < k
⊢ n < k
Tactic:
have : n < k := lt_trans ‹n < m› ‹m < k›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this✝ : m < k ∨ m ≃ k
h✝ : m < k
this : n < k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_lt_le_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this✝ : m < k ∨ m ≃ k
h✝ : m < k
this : n < k
⊢ n < k
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_lt_le_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this : m < k ∨ m ≃ k
h✝ : m ≃ k
⊢ n < k
Tactic:
have : n < k := trans_lt_eqv_lt ‹n < m› ‹m ≃ k›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this✝ : m < k ∨ m ≃ k
h✝ : m ≃ k
this : n < k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_lt_le_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≤ k
this✝ : m < k ∨ m ≃ k
h✝ : m ≃ k
this : n < k
⊢ n < k
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
⊢ n ≤ m → m < k → n < k
Tactic:
intro (_ : n ≤ m) (_ : m < k)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
⊢ n < k
Tactic:
have : n < m ∨ n ≃ m := le_split ‹n ≤ m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this : n < m ∨ n ≃ m
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this : n < m ∨ n ≃ m
⊢ n < k
Tactic:
match this with
| Or.inl (_ : n < m) =>
  have : n < k := lt_trans ‹n < m› ‹m < k›
  exact this
| Or.inr (_ : n ≃ m) =>
  have : n < k := trans_eqv_lt_lt ‹n ≃ m› ‹m < k›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this : n < m ∨ n ≃ m
h✝ : n < m
⊢ n < k
Tactic:
have : n < k := lt_trans ‹n < m› ‹m < k›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this✝ : n < m ∨ n ≃ m
h✝ : n < m
this : n < k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this✝ : n < m ∨ n ≃ m
h✝ : n < m
this : n < k
⊢ n < k
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this : n < m ∨ n ≃ m
h✝ : n ≃ m
⊢ n < k
Tactic:
have : n < k := trans_eqv_lt_lt ‹n ≃ m› ‹m < k›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this✝ : n < m ∨ n ≃ m
h✝ : n ≃ m
this : n < k
⊢ n < k
Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this✝ : n < m ∨ n ≃ m
h✝ : n ≃ m
this : n < k
⊢ n < k
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_substL_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
⊢ n₁ < n₂ → n₁ + m < n₂ + m
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₂
⊢ 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₂
⊢ n₁ + m < n₂ + m
Tactic:
have (And.intro (_ : n₁ ≤ n₂) (_ : n₁ ≄ n₂)) := lt_defn.mp ‹n₁ < n₂›
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₂
⊢ 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₂
⊢ n₁ + m < n₂ + m
Tactic:
have : n₁ + m ≤ n₂ + m := AA.substL ‹n₁ ≤ n₂›
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
⊢ 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
⊢ n₁ + m < n₂ + m
Tactic:
have : n₁ + m ≄ n₂ + m := mt AA.cancelR ‹n₁ ≄ n₂›
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
⊢ n₁ + m < n₂ + m