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

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

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

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

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

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

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