Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv (Lean4Analysis/Ch4/Ch4Sec1Integers.lean)

State before:
n m : ℤ
⊢ n > m ↔ n ≥ m ∧ n ≄ m
Tactic:
apply Iff.intro
State after:
case mp
n m : ℤ
⊢ n > m → n ≥ m ∧ n ≄ m

case mpr
n m : ℤ
⊢ n ≥ m ∧ n ≄ m → n > m

State before:
n m : ℤ
⊢ n > m → n ≥ m ∧ n ≄ m
Tactic:
case mp =>
  intro (_ : n > m)
  show n ≥ m ∧ n ≄ m
  have (And.intro (_ : n ≥ m) (_ : m ≄ n)) :=
    Integer.lt_iff_le_neqv.mp ‹n > m›
  have : n ≄ m := Rel.symm ‹m ≄ n›
  exact And.intro ‹n ≥ m› ‹n ≄ m›
State after:
no goals

State before:
n m : ℤ
⊢ n ≥ m ∧ n ≄ m → n > m
Tactic:
case mpr =>
  intro (And.intro (_ : n ≥ m) (_ : n ≄ m))
  show n > m
  apply Integer.lt_iff_le_neqv.mpr
  show n ≥ m ∧ m ≄ n
  have : m ≄ n := Rel.symm ‹n ≄ m›
  exact And.intro ‹n ≥ m› ‹m ≄ n›
State after:
no goals

State before:
n m : ℤ
⊢ n > m → n ≥ m ∧ n ≄ m
Tactic:
intro (_ : n > m)
State after:
n m : ℤ
x✝ : n > m
⊢ n ≥ m ∧ n ≄ m

State before:
n m : ℤ
x✝ : n > m
⊢ n ≥ m ∧ n ≄ m
Tactic:
have (And.intro (_ : n ≥ m) (_ : m ≄ n)) :=
  Integer.lt_iff_le_neqv.mp ‹n > m›
State after:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
⊢ n ≥ m ∧ n ≄ m

State before:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
⊢ n ≥ m ∧ n ≄ m
Tactic:
have : n ≄ m := Rel.symm ‹m ≄ n›
State after:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
this : n ≄ m
⊢ n ≥ m ∧ n ≄ m

State before:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
this : n ≄ m
⊢ n ≥ m ∧ n ≄ m
Tactic:
exact And.intro ‹n ≥ m› ‹n ≄ m›
State after:
no goals

State before:
n m : ℤ
⊢ n ≥ m ∧ n ≄ m → n > m
Tactic:
intro (And.intro (_ : n ≥ m) (_ : n ≄ m))
State after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n > m

State before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n > m
Tactic:
apply Integer.lt_iff_le_neqv.mpr
State after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ m ≤ n ∧ m ≄ n

State before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ m ≤ n ∧ m ≄ n
Tactic:
show n ≥ m ∧ m ≄ n
State after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n ≥ m ∧ m ≄ n

State before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n ≥ m ∧ m ≄ n
Tactic:
have : m ≄ n := Rel.symm ‹n ≄ m›
State after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
this : m ≄ n
⊢ n ≥ m ∧ m ≄ n

State before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
this : m ≄ n
⊢ n ≥ m ∧ m ≄ n
Tactic:
exact And.intro ‹n ≥ m› ‹m ≄ n›
State after:
no goals