internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.lt_step_le
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝¹ : n + step d ≃ m
this✝ : ∃ d, n + d ≃ m
this : n ≤ m
x✝ : n ≃ m
⊢ False
Tactic:
have : n + step d ≃ n + 0 := calc
  n + step d ≃ _ := ‹n + step d ≃ m›
  m          ≃ _ := Rel.symm ‹n ≃ m›
  n          ≃ _ := Rel.symm add_zero
  n + 0      ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
x✝ : n ≃ m
this : n + step d ≃ n + 0
⊢ False
Theorem: Lean4Axiomatic.Natural.lt_step_le
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝² : n + step d ≃ m
this✝¹ : ∃ d, n + d ≃ m
this✝ : n ≤ m
x✝ : n ≃ m
this : n + step d ≃ n + 0
⊢ False
Tactic:
have : step d ≃ 0 := AA.cancelL ‹n + step d ≃ n + 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝³ : n + step d ≃ m
this✝² : ∃ d, n + d ≃ m
this✝¹ : n ≤ m
x✝ : n ≃ m
this✝ : n + step d ≃ n + 0
this : step d ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.lt_step_le
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : step n ≤ m
d : ℕ
h✝ : step n + d ≃ m
this✝³ : n + step d ≃ m
this✝² : ∃ d, n + d ≃ m
this✝¹ : n ≤ m
x✝ : n ≃ m
this✝ : n + step d ≃ n + 0
this : step d ≃ 0
⊢ False
Tactic:
exact absurd ‹step d ≃ 0› step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m ↔ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m → ∃ k, Positive k ∧ m ≃ n + k

case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ (∃ k, Positive k ∧ m ≃ n + k) → n < m
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m → ∃ k, Positive k ∧ m ≃ n + k
Tactic:
intro (_ : n < m)
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : step n ≤ m := lt_step_le.mp ‹n < m›
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have ⟨k, (_ : step n + k ≃ m)⟩ := le_defn.mp ‹step n ≤ m›
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
exists step k
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k) ∧ m ≃ n + step k
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k) ∧ m ≃ n + step k
Tactic:
apply And.intro
Proof state after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k)

case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ m ≃ n + step k
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k)
Tactic:
have : step k ≄ 0 := step_neqv_zero
Proof state after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this : step k ≄ 0
⊢ Positive (step k)
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this : step k ≄ 0
⊢ Positive (step k)
Tactic:
have : Positive (step k) := Signed.positive_defn.mpr ‹step k ≄ 0›
Proof state after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝¹ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this✝ : step k ≄ 0
this : Positive (step k)
⊢ Positive (step k)
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝¹ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this✝ : step k ≄ 0
this : Positive (step k)
⊢ Positive (step k)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ m ≃ n + step k
Tactic:
calc
  m            ≃ _ := Rel.symm ‹step n + k ≃ m›
  step n + k   ≃ _ := step_add
  step (n + k) ≃ _ := Rel.symm add_step
  n + step k   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ (∃ k, Positive k ∧ m ≃ n + k) → n < m
Tactic:
intro ⟨k, (_ : Positive k), (_ : m ≃ n + k)⟩
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n < m
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n < m
Tactic:
apply lt_step_le.mpr
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ step n ≤ m
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ step n ≤ m
Tactic:
apply le_defn.mpr
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ ∃ k, step n + k ≃ m
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ ∃ k, step n + k ≃ m
Tactic:
have ⟨k', (_ : step k' ≃ k)⟩ := positive_step ‹Positive k›
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ ∃ k, step n + k ≃ m
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ ∃ k, step n + k ≃ m
Tactic:
exists k'
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ step n + k' ≃ m
Theorem: Lean4Axiomatic.Natural.lt_defn_add
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ step n + k' ≃ m
Tactic:
calc
  step n + k'   ≃ _ := step_add
  step (n + k') ≃ _ := Rel.symm add_step
  n + step k'   ≃ _ := AA.substR ‹step k' ≃ k›
  n + k         ≃ _ := Rel.symm ‹m ≃ n + k›
  m             ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_zero
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≮ 0
Tactic:
intro (_ : n < 0)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
⊢ False
Theorem: Lean4Axiomatic.Natural.lt_zero
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
⊢ False
Tactic:
have : step n ≤ 0 := lt_step_le.mp ‹n < 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.lt_zero
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
⊢ False
Tactic:
have ⟨d, (_ : step n + d ≃ 0)⟩ := le_defn.mp ‹step n ≤ 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.lt_zero
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
⊢ False
Tactic:
have : step (n + d) ≃ 0 := calc
  step (n + d) ≃ _ := Rel.symm step_add
  step n + d   ≃ _ := ‹step n + d ≃ 0›
  0            ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this✝ : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
this : step (n + d) ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.lt_zero
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this✝ : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
this : step (n + d) ≃ 0
⊢ False
Tactic:
exact absurd ‹step (n + d) ≃ 0› step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n ↔ n > 0
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 > 0

case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n > 0 → Positive n
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ Positive n → n > 0
Tactic:
intro (_ : Positive n)
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n > 0
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n > 0
Tactic:
show 0 < n
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ 0 < n
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ 0 < n
Tactic:
apply lt_defn_add.mpr
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ ∃ k, Positive k ∧ n ≃ 0 + k
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ ∃ k, Positive k ∧ n ≃ 0 + k
Tactic:
exists n
Proof state after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n ∧ n ≃ 0 + n
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n ∧ n ≃ 0 + n
Tactic:
apply And.intro
Proof state after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n

case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n ≃ 0 + n
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ Positive n
Tactic:
exact ‹Positive n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : Positive n
⊢ n ≃ 0 + n
Tactic:
exact Rel.symm zero_add
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n > 0 → Positive n
Tactic:
intro (_ : 0 < n)
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
⊢ Positive n
Tactic:
have ⟨k, ⟨(_ : Positive k), (_ : n ≃ 0 + k)⟩⟩ := lt_defn_add.mp ‹0 < n›
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
⊢ Positive n
Tactic:
have : k ≃ n := Rel.symm (Rel.trans ‹n ≃ 0 + k› zero_add)
Proof state after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
this : k ≃ n
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.lt_zero_pos
Proof state before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
this : k ≃ n
⊢ Positive n
Tactic:
exact AA.substFn ‹k ≃ n› ‹Positive k›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_from_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
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
Theorem: Lean4Axiomatic.Natural.le_from_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n ≤ m
Tactic:
have : n ≤ n := Rel.refl
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≃ m
this : n ≤ n
⊢ n ≤ m
Theorem: Lean4Axiomatic.Natural.le_from_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≃ m
this : n ≤ n
⊢ n ≤ m
Tactic:
exact AA.substRFn ‹n ≃ m› ‹n ≤ n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_from_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
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
Theorem: Lean4Axiomatic.Natural.le_from_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
⊢ n ≤ m
Tactic:
have ⟨(_ : n ≤ m), _⟩ := lt_defn.mp ‹n < m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ n ≤ m
Theorem: Lean4Axiomatic.Natural.le_from_lt
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
left✝ : n ≤ m
right✝ : n ≄ m
⊢ n ≤ m
Tactic:
exact ‹n ≤ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_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.le_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 ⟨d, (h : n + d ≃ m)⟩ := le_defn.mp ‹n ≤ m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
h : n + d ≃ m
⊢ n < m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
h : n + d ≃ m
⊢ n < m ∨ n ≃ m
Tactic:
revert h
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + d ≃ m → n < m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + d ≃ m → n < m ∨ n ≃ m
Tactic:
apply cases_on (motive := λ d => n + d ≃ m → n < m ∨ n ≃ m) d
Proof state after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + 0 ≃ m → n < m ∨ n ≃ m

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ ∀ (m_1 : ℕ), n + step m_1 ≃ m → n < m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + 0 ≃ m → n < m ∨ n ≃ m
Tactic:
case zero =>
  intro (_ : n + 0 ≃ m)
  apply Or.inr
  show n ≃ m
  calc
    n     ≃ _ := Rel.symm add_zero
    n + 0 ≃ _ := ‹n + 0 ≃ m›
    m     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ ∀ (m_1 : ℕ), n + step m_1 ≃ m → n < m ∨ n ≃ m
Tactic:
case step =>
  intro d (_ : n + step d ≃ m)
  apply Or.inl
  show n < m
  apply lt_step_le.mpr
  show step n ≤ m
  apply le_defn.mpr
  exists d
  show step n + d ≃ m
  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.le_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + 0 ≃ m → n < m ∨ n ≃ m
Tactic:
intro (_ : n + 0 ≃ m)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d : ℕ
x✝ : n + 0 ≃ m
⊢ n < m ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d : ℕ
x✝ : n + 0 ≃ m
⊢ n < m ∨ n ≃ m
Tactic:
apply Or.inr
Proof state after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d : ℕ
x✝ : n + 0 ≃ m
⊢ 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 : ℕ
x✝ : n + 0 ≃ m
⊢ n ≃ m
Tactic:
calc
  n     ≃ _ := Rel.symm add_zero
  n + 0 ≃ _ := ‹n + 0 ≃ m›
  m     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ ∀ (m_1 : ℕ), n + step m_1 ≃ m → n < m ∨ n ≃ m
Tactic:
intro d (_ : n + step d ≃ m)
Proof state after:
ℕ : 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 ∨ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_split
Proof state before:
ℕ : 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 ∨ n ≃ m
Tactic:
apply Or.inl
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
⊢ n < m