Theorem: Lean4Axiomatic.Natural.Impl.Nat.prelude_lt_iff_impl_lt (Lean4Axiomatic/Natural/Impl/Nat.lean)

State before:
n m : Nat
⊢ n < m ↔ lt n m
Tactic:
apply Iff.intro
State after:
case mp
n m : Nat
⊢ n < m → lt n m

case mpr
n m : Nat
⊢ lt n m → n < m

State before:
n m : Nat
⊢ n < m → lt n m
Tactic:
case mp =>
  intro (_ : n < m)
  show lt n m
  have : step n ≤ m := ‹n < m›
  have : step n ≤ step m := Nat.le_succ_of_le ‹step n ≤ m›
  have : n ≤ m := Nat.le_of_succ_le_succ ‹step n ≤ step m›
  have : le n m := prelude_le_iff_impl_le.mp ‹n ≤ m›
  have : n ≄ m := by
    intro (_ : n ≃ m)
    show False
    have : n = m := ‹n ≃ m›
    rw [‹n = m›] at ‹step n ≤ m›
    have : ¬(step m ≤ m) := Nat.not_succ_le_self m
    exact absurd ‹step m ≤ m› ‹¬(step m ≤ m)›
  have : lt n m := And.intro ‹le n m› ‹n ≄ m›
  exact this
State after:
no goals

State before:
n m : Nat
⊢ lt n m → n < m
Tactic:
case mpr =>
  intro (_ : lt n m)
  show n < m
  have (And.intro (_ : le n m) (_ : n ≄ m)) := ‹lt n m›
  have : n ≤ m := prelude_le_iff_impl_le.mpr ‹le n m›
  have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
  match ‹n = m ∨ n < m› with
  | Or.inl (_ : n = m) =>
    have : n ≠ m := ‹n ≄ m›
    exact absurd ‹n = m› ‹n ≠ m›
  | Or.inr (_ : n < m) =>
    exact ‹n < m›
State after:
no goals

State before:
n m : Nat
⊢ n < m → lt n m
Tactic:
intro (_ : n < m)
State after:
n m : Nat
x✝ : n < m
⊢ lt n m

State before:
n m : Nat
x✝ : n < m
⊢ lt n m
Tactic:
have : step n ≤ m := ‹n < m›
State after:
n m : Nat
x✝ : n < m
this : step n ≤ m
⊢ lt n m

State before:
n m : Nat
x✝ : n < m
this : step n ≤ m
⊢ lt n m
Tactic:
have : step n ≤ step m := Nat.le_succ_of_le ‹step n ≤ m›
State after:
n m : Nat
x✝ : n < m
this✝ : step n ≤ m
this : step n ≤ step m
⊢ lt n m

State before:
n m : Nat
x✝ : n < m
this✝ : step n ≤ m
this : step n ≤ step m
⊢ lt n m
Tactic:
have : n ≤ m := Nat.le_of_succ_le_succ ‹step n ≤ step m›
State after:
n m : Nat
x✝ : n < m
this✝¹ : step n ≤ m
this✝ : step n ≤ step m
this : n ≤ m
⊢ lt n m

State before:
n m : Nat
x✝ : n < m
this✝¹ : step n ≤ m
this✝ : step n ≤ step m
this : n ≤ m
⊢ lt n m
Tactic:
have : le n m := prelude_le_iff_impl_le.mp ‹n ≤ m›
State after:
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ lt n m

State before:
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ lt n m
Tactic:
have : n ≄ m := by
  intro (_ : n ≃ m)
  show False
  have : n = m := ‹n ≃ m›
  rw [‹n = m›] at ‹step n ≤ m›
  have : ¬(step m ≤ m) := Nat.not_succ_le_self m
  exact absurd ‹step m ≤ m› ‹¬(step m ≤ m)›
State after:
n m : Nat
x✝ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
this : n ≄ m
⊢ lt n m

State before:
n m : Nat
x✝ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
this : n ≄ m
⊢ lt n m
Tactic:
have : lt n m := And.intro ‹le n m› ‹n ≄ m›
State after:
n m : Nat
x✝ : n < m
this✝⁴ : step n ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
this✝ : n ≄ m
this : lt n m
⊢ lt n m

State before:
n m : Nat
x✝ : n < m
this✝⁴ : step n ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
this✝ : n ≄ m
this : lt n m
⊢ lt n m
Tactic:
exact this
State after:
no goals

State before:
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ n ≄ m
Tactic:
intro (_ : n ≃ m)
State after:
n m : Nat
x✝¹ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
x✝ : n ≃ m
⊢ False

State before:
n m : Nat
x✝¹ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
x✝ : n ≃ m
⊢ False
Tactic:
have : n = m := ‹n ≃ m›
State after:
n m : Nat
x✝¹ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False

State before:
n m : Nat
x✝¹ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False
Tactic:
rw [‹n = m›] at ‹step n ≤ m›
State after:
n m : Nat
x✝¹ : n < m
this✝³ : step m ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False

State before:
n m : Nat
x✝¹ : n < m
this✝³ : step m ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
x✝ : n ≃ m
this : n = m
⊢ False
Tactic:
have : ¬(step m ≤ m) := Nat.not_succ_le_self m
State after:
n m : Nat
x✝¹ : n < m
this✝⁴ : step m ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
x✝ : n ≃ m
this✝ : n = m
this : ¬step m ≤ m
⊢ False

State before:
n m : Nat
x✝¹ : n < m
this✝⁴ : step m ≤ m
this✝³ : step n ≤ step m
this✝² : n ≤ m
this✝¹ : le n m
x✝ : n ≃ m
this✝ : n = m
this : ¬step m ≤ m
⊢ False
Tactic:
exact absurd ‹step m ≤ m› ‹¬(step m ≤ m)›
State after:
no goals

State before:
n m : Nat
⊢ lt n m → n < m
Tactic:
intro (_ : lt n m)
State after:
n m : Nat
x✝ : lt n m
⊢ n < m

State before:
n m : Nat
x✝ : lt n m
⊢ n < m
Tactic:
have (And.intro (_ : le n m) (_ : n ≄ m)) := ‹lt n m›
State after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
⊢ n < m

State before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
⊢ n < m
Tactic:
have : n ≤ m := prelude_le_iff_impl_le.mpr ‹le n m›
State after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this : n ≤ m
⊢ n < m

State before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this : n ≤ m
⊢ n < m
Tactic:
have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
State after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
⊢ n < m

State before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
⊢ n < m
Tactic:
match ‹n = m ∨ n < m› with
| Or.inl (_ : n = m) =>
  have : n ≠ m := ‹n ≄ m›
  exact absurd ‹n = m› ‹n ≠ m›
| Or.inr (_ : n < m) =>
  exact ‹n < m›
State after:
no goals

State before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
h✝ : n = m
⊢ n < m
Tactic:
have : n ≠ m := ‹n ≄ m›
State after:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝¹ : n ≤ m
this✝ : n = m ∨ n < m
h✝ : n = m
this : n ≠ m
⊢ n < m

State before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝¹ : n ≤ m
this✝ : n = m ∨ n < m
h✝ : n = m
this : n ≠ m
⊢ n < m
Tactic:
exact absurd ‹n = m› ‹n ≠ m›
State after:
no goals

State before:
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
h✝ : n < m
⊢ n < m
Tactic:
exact ‹n < m›
State after:
no goals