internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.le_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
⊢ m₁ ≃ m₂ → n ≤ m₁ → n ≤ m₂
Tactic:
intro (_ : m₁ ≃ m₂) (_ : n ≤ m₁)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
⊢ n ≤ m₂
Theorem: Lean4Axiomatic.Natural.le_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
⊢ n ≤ m₂
Tactic:
have ⟨d, (_ : 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₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
d : ℕ
h✝ : n + d ≃ m₁
⊢ n ≤ m₂
Theorem: Lean4Axiomatic.Natural.le_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
d : ℕ
h✝ : n + d ≃ m₁
⊢ n ≤ m₂
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
d : ℕ
h✝ : n + d ≃ m₁
⊢ ∃ k, n + k ≃ m₂
Theorem: Lean4Axiomatic.Natural.le_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
d : ℕ
h✝ : n + d ≃ m₁
⊢ ∃ k, n + k ≃ m₂
Tactic:
exists d
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
d : ℕ
h✝ : n + d ≃ m₁
⊢ n + d ≃ m₂
Theorem: Lean4Axiomatic.Natural.le_eqv_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝¹ : m₁ ≃ m₂
x✝ : n ≤ m₁
d : ℕ
h✝ : n + d ≃ m₁
⊢ n + d ≃ m₂
Tactic:
exact Rel.trans ‹n + d ≃ m₁› ‹m₁ ≃ m₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_le_eqv_le
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_eqv_le
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 le_eqv_subst ‹m ≃ k› ‹n ≤ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_refl
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≤ n
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ ∃ k, n + k ≃ n
Theorem: Lean4Axiomatic.Natural.le_refl
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ ∃ k, n + k ≃ n
Tactic:
exists (0 : ℕ)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n + 0 ≃ n
Theorem: Lean4Axiomatic.Natural.le_refl
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n + 0 ≃ n
Tactic:
exact add_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n ≤ step m → n ≤ m ∨ n ≃ step 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 ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step_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 ≃ step m
Tactic:
have ⟨d, (_ : n + d ≃ step m)⟩ := le_defn.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
d : ℕ
h✝ : n + d ≃ step m
⊢ n ≤ m ∨ n ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
⊢ n ≤ m ∨ n ≃ step m
Tactic:
let motive := λ x => d ≃ x → n ≤ m ∨ n ≃ step m
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
⊢ n ≤ m ∨ n ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
⊢ motive 0
Tactic:
intro (_ : d ≃ 0)
Proof state after:
case x
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
x✝ : d ≃ 0
⊢ n ≤ m ∨ n ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
x✝ : d ≃ 0
⊢ n ≤ m ∨ n ≃ step m
Tactic:
apply Or.inr
Proof state after:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
x✝ : d ≃ 0
⊢ n ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
x✝ : d ≃ 0
⊢ n ≃ step m
Tactic:
calc
  n      ≃ _ := Rel.symm add_zero
  n + 0  ≃ _ := AA.substR (Rel.symm ‹d ≃ 0›)
  n + d  ≃ _ := ‹n + d ≃ step m›
  step m ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
⊢ ∀ (m : ℕ), motive (step m)
Tactic:
intro e (_ : d ≃ step e)
Proof state after:
case x
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ n ≤ m ∨ n ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ n ≤ m ∨ n ≃ step m
Tactic:
apply Or.inl
Proof state after:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ n ≤ m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ n ≤ m
Tactic:
apply le_defn.mpr
Proof state after:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ ∃ k, n + k ≃ m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ ∃ k, n + k ≃ m
Tactic:
exists e
Proof state after:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ n + e ≃ m
Theorem: Lean4Axiomatic.Natural.le_step_split
Proof state before:
case x.h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ step m
d : ℕ
h✝ : n + d ≃ step m
motive : ℕ → Prop := fun x => d ≃ x → n ≤ m ∨ n ≃ step m
e : ℕ
x✝ : d ≃ step e
⊢ step (n + e) ≃ step m
Tactic:
calc
  step (n + e) ≃ _ := Rel.symm add_step
  n + step e   ≃ _ := AA.substR (Rel.symm ‹d ≃ step e›)
  n + d        ≃ _ := ‹n + d ≃ step m›
  step m       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n ≤ m → n ≤ step 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 ≤ step m
Theorem: Lean4Axiomatic.Natural.le_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
⊢ n ≤ step m
Tactic:
have ⟨d, (_ : 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 ≤ step m
Theorem: Lean4Axiomatic.Natural.le_step
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 ≤ step m
Tactic:
apply le_defn.mpr
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
⊢ ∃ k, n + k ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step
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
⊢ ∃ k, n + k ≃ step m
Tactic:
exists step d
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 + step d ≃ step m
Theorem: Lean4Axiomatic.Natural.le_step
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 + step d ≃ step m
Tactic:
calc
  n + step d   ≃ _ := add_step
  step (n + d) ≃ _ := AA.subst₁ ‹n + d ≃ m›
  step m       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_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)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
⊢ m ≤ k → n ≤ k
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
⊢ m ≤ k → n ≤ k
Tactic:
have ⟨d, (_ : 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 k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ k → n ≤ k
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ k → n ≤ k
Tactic:
apply ind_on (motive := λ k => m ≤ k → n ≤ k) k
Proof state after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ 0 → n ≤ 0

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ 0 → n ≤ 0
Tactic:
case zero =>
  intro (_ : m ≤ 0)
  have ⟨e, (_ : m + e ≃ 0)⟩ := le_defn.mp ‹m ≤ 0›
  show n ≤ 0
  apply le_defn.mpr
  exists d + e
  show n + (d + e) ≃ 0
  calc
    n + (d + e) ≃ _ := Rel.symm AA.assoc
    (n + d) + e ≃ _ := AA.substL ‹n + d ≃ m›
    m + e       ≃ _ := ‹m + e ≃ 0›
    0           ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1
Tactic:
case step =>
  intro k (ih : m ≤ k → n ≤ k) (_ : m ≤ step k)
  show n ≤ step k
  match le_step_split ‹m ≤ step k› with
  | Or.inl (_ : m ≤ k) =>
    exact le_step (ih ‹m ≤ k›)
  | Or.inr (_ : m ≃ step k) =>
    exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ 0 → n ≤ 0
Tactic:
intro (_ : m ≤ 0)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
x✝ : m ≤ 0
⊢ n ≤ 0
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
x✝ : m ≤ 0
⊢ n ≤ 0
Tactic:
have ⟨e, (_ : m + e ≃ 0)⟩ := le_defn.mp ‹m ≤ 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n ≤ 0
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n ≤ 0
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ ∃ k, n + k ≃ 0
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ ∃ k, n + k ≃ 0
Tactic:
exists d + e
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n + (d + e) ≃ 0
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n + (d + e) ≃ 0
Tactic:
calc
  n + (d + e) ≃ _ := Rel.symm AA.assoc
  (n + d) + e ≃ _ := AA.substL ‹n + d ≃ m›
  m + e       ≃ _ := ‹m + e ≃ 0›
  0           ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1
Tactic:
intro k (ih : m ≤ k → n ≤ k) (_ : m ≤ step k)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
⊢ n ≤ step k
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
⊢ n ≤ step k
Tactic:
match le_step_split ‹m ≤ step k› with
| Or.inl (_ : m ≤ k) =>
  exact le_step (ih ‹m ≤ k›)
| Or.inr (_ : m ≃ step k) =>
  exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
h✝ : m ≤ k
⊢ n ≤ step k
Tactic:
exact le_step (ih ‹m ≤ k›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_trans
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
h✝ : m ≃ step k
⊢ n ≤ step k
Tactic:
exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_subst_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.le_subst_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 ⟨d, (_ : n₁ + d ≃ n₂)⟩ := le_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₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ n₁ + m ≤ n₂ + m
Theorem: Lean4Axiomatic.Natural.le_subst_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ n₁ + m ≤ n₂ + m
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ ∃ k, n₁ + m + k ≃ n₂ + m
Theorem: Lean4Axiomatic.Natural.le_subst_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ ∃ k, n₁ + m + k ≃ n₂ + m
Tactic:
exists d
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ n₁ + m + d ≃ n₂ + m
Theorem: Lean4Axiomatic.Natural.le_subst_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ n₁ + m + d ≃ n₂ + m
Tactic:
calc
  (n₁ + m) + d ≃ _ := AA.assoc
  n₁ + (m + d) ≃ _ := AA.substR AA.comm
  n₁ + (d + m) ≃ _ := Rel.symm AA.assoc
  (n₁ + d) + m ≃ _ := AA.substL ‹n₁ + d ≃ n₂›
  n₂ + m       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_cancel_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
⊢ n + m₁ ≤ n + m₂ → m₁ ≤ m₂
Tactic:
intro (_ : n + m₁ ≤ n + m₂)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
⊢ m₁ ≤ m₂
Theorem: Lean4Axiomatic.Natural.le_cancel_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
⊢ m₁ ≤ m₂
Tactic:
have ⟨d, (_ : (n + m₁) + d ≃ n + m₂)⟩ := le_defn.mp ‹n + m₁ ≤ n + m₂›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
⊢ m₁ ≤ m₂
Theorem: Lean4Axiomatic.Natural.le_cancel_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
⊢ m₁ ≤ m₂
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
⊢ ∃ k, m₁ + k ≃ m₂
Theorem: Lean4Axiomatic.Natural.le_cancel_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
⊢ ∃ k, m₁ + k ≃ m₂
Tactic:
exists d
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
⊢ m₁ + d ≃ m₂
Theorem: Lean4Axiomatic.Natural.le_cancel_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
⊢ m₁ + d ≃ m₂
Tactic:
have : n + (m₁ + d) ≃ n + m₂ := calc
  n + (m₁ + d) ≃ _ := Rel.symm AA.assoc
  (n + m₁) + d ≃ _ := ‹(n + m₁) + d ≃ n + m₂›
  n + m₂       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
this : n + (m₁ + d) ≃ n + m₂
⊢ m₁ + d ≃ m₂
Theorem: Lean4Axiomatic.Natural.le_cancel_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m₁ m₂ : ℕ
x✝ : n + m₁ ≤ n + m₂
d : ℕ
h✝ : n + m₁ + d ≃ n + m₂
this : n + (m₁ + d) ≃ n + m₂
⊢ m₁ + d ≃ m₂
Tactic:
exact AA.cancelL ‹n + (m₁ + d) ≃ n + m₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_antisymm
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n ≤ m → m ≤ n → n ≃ m
Tactic:
intro (_ : n ≤ m) (_ : 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
⊢ 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
⊢ n ≃ m
Tactic:
have ⟨d₁, (_ : 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
x✝ : m ≤ n
d₁ : ℕ
h✝ : n + d₁ ≃ m
⊢ n ≃ m