internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.le_antisymm
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝ : n + d₁ ≃ m
⊢ n ≃ m
Tactic:
have ⟨d₂, (_ : m + d₂ ≃ n)⟩ := le_defn.mp ‹m ≤ n›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_antisymm
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
⊢ n ≃ m
Tactic:
have : n + (d₁ + d₂) ≃ n + 0 := calc
  n + (d₁ + d₂) ≃ _ := Rel.symm AA.assoc
  (n + d₁) + d₂ ≃ _ := AA.substL ‹n + d₁ ≃ m›
  m + d₂        ≃ _ := ‹m + d₂ ≃ n›
  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✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this : n + (d₁ + d₂) ≃ n + 0
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_antisymm
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this : n + (d₁ + d₂) ≃ n + 0
⊢ n ≃ m
Tactic:
have : d₁ + d₂ ≃ 0 := AA.cancelL ‹n + (d₁ + d₂) ≃ n + 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_antisymm
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
⊢ n ≃ m
Tactic:
have ⟨(_ : d₁ ≃ 0), _⟩ := zero_sum_split ‹d₁ + d₂ ≃ 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
left✝ : d₁ ≃ 0
right✝ : d₂ ≃ 0
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.le_antisymm
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
x✝ : m ≤ n
d₁ : ℕ
h✝¹ : n + d₁ ≃ m
d₂ : ℕ
h✝ : m + d₂ ≃ n
this✝ : n + (d₁ + d₂) ≃ n + 0
this : d₁ + d₂ ≃ 0
left✝ : d₁ ≃ 0
right✝ : d₂ ≃ 0
⊢ n ≃ m
Tactic:
calc
  n      ≃ _ := Rel.symm add_zero
  n + 0  ≃ _ := AA.substR (Rel.symm ‹d₁ ≃ 0›)
  n + d₁ ≃ _ := ‹n + d₁ ≃ m›
  m      ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_subst_eqv
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₂) (_ : n₁ < m)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
⊢ n₂ < m
Theorem: Lean4Axiomatic.Natural.lt_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
⊢ n₂ < m
Tactic:
have ⟨(_ : n₁ ≤ m), (_ : n₁ ≄ m)⟩ := lt_defn.mp ‹n₁ < m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
⊢ n₂ < m
Theorem: Lean4Axiomatic.Natural.lt_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
⊢ n₂ < m
Tactic:
have : n₂ ≤ m := AA.substLFn ‹n₁ ≃ n₂› ‹n₁ ≤ m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
this : n₂ ≤ m
⊢ n₂ < m
Theorem: Lean4Axiomatic.Natural.lt_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
this : n₂ ≤ m
⊢ n₂ < m
Tactic:
have : n₂ ≄ m := AA.neqv_substL ‹n₁ ≃ n₂› ‹n₁ ≄ m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
this✝ : n₂ ≤ m
this : n₂ ≄ m
⊢ n₂ < m
Theorem: Lean4Axiomatic.Natural.lt_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
this✝ : n₂ ≤ m
this : n₂ ≄ m
⊢ n₂ < m
Tactic:
apply lt_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
this✝ : n₂ ≤ m
this : n₂ ≄ m
⊢ n₂ ≤ m ∧ n₂ ≄ m
Theorem: Lean4Axiomatic.Natural.lt_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ < m
left✝ : n₁ ≤ m
right✝ : n₁ ≄ m
this✝ : n₂ ≤ m
this : n₂ ≄ m
⊢ n₂ ≤ m ∧ n₂ ≄ m
Tactic:
exact ⟨‹n₂ ≤ m›, ‹n₂ ≄ m›⟩
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_eqv_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_eqv_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:
exact lt_subst_eqv (Rel.symm ‹n ≃ m›) ‹m < k›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_eqv_subst
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₂) (_ : m < n₁)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
⊢ m < n₂
Theorem: Lean4Axiomatic.Natural.lt_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
⊢ m < n₂
Tactic:
have ⟨(_ : m ≤ n₁), (_ : m ≄ n₁)⟩ := lt_defn.mp ‹m < n₁›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
⊢ m < n₂
Theorem: Lean4Axiomatic.Natural.lt_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
⊢ m < n₂
Tactic:
have : m ≤ n₂ := AA.substRFn ‹n₁ ≃ n₂› ‹m ≤ n₁›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
this : m ≤ n₂
⊢ m < n₂
Theorem: Lean4Axiomatic.Natural.lt_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
this : m ≤ n₂
⊢ m < n₂
Tactic:
have : m ≄ n₂ := AA.neqv_substR ‹n₁ ≃ n₂› ‹m ≄ n₁›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
this✝ : m ≤ n₂
this : m ≄ n₂
⊢ m < n₂
Theorem: Lean4Axiomatic.Natural.lt_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
this✝ : m ≤ n₂
this : m ≄ n₂
⊢ m < n₂
Tactic:
apply lt_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
this✝ : m ≤ n₂
this : m ≄ n₂
⊢ m ≤ n₂ ∧ m ≄ n₂
Theorem: Lean4Axiomatic.Natural.lt_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : m < n₁
left✝ : m ≤ n₁
right✝ : m ≄ n₁
this✝ : m ≤ n₂
this : m ≄ n₂
⊢ m ≤ n₂ ∧ m ≄ n₂
Tactic:
exact ⟨‹m ≤ n₂›, ‹m ≄ n₂›⟩
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_lt_eqv_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_eqv_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:
exact lt_eqv_subst ‹m ≃ k› ‹n < m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n < step n
Tactic:
apply lt_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≤ step n ∧ n ≄ step n
Theorem: Lean4Axiomatic.Natural.lt_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≤ step n ∧ n ≄ step n
Tactic:
apply And.intro
Proof state after:
case left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≤ step n

case right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≄ step n
Theorem: Lean4Axiomatic.Natural.lt_step
Proof state before:
case left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≤ step n
Tactic:
apply le_defn.mpr
Proof state after:
case left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ ∃ k, n + k ≃ step n
Theorem: Lean4Axiomatic.Natural.lt_step
Proof state before:
case left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ ∃ k, n + k ≃ step n
Tactic:
exists (1 : ℕ)
Proof state after:
case left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n + 1 ≃ step n
Theorem: Lean4Axiomatic.Natural.lt_step
Proof state before:
case left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n + 1 ≃ step n
Tactic:
exact add_one_step
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_step
Proof state before:
case right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≄ step n
Tactic:
exact Rel.symm step_neqv
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.lt_step_le
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m ↔ step n ≤ m
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 → step n ≤ m

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