Theorem: Lean4Axiomatic.Natural.lt_eqv_subst (Lean4Axiomatic/Natural/Order.lean)

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₁)
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₂

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₁›
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₂

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₁›
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₂

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₁›
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₂

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
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₂

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₂›⟩
State after:
no goals