Theorem: Int.eq_zero_of_lt_neg_iff_lt (LeanSAT/Upstream/ToMathlib.lean)

State before:
i : ℤ
⊢ (0 < -i ↔ 0 < i) → i = 0
Tactic:
intro h
State after:
i : ℤ
h : 0 < -i ↔ 0 < i
⊢ i = 0

State before:
i : ℤ
h : 0 < -i ↔ 0 < i
⊢ i = 0
Tactic:
by_cases hLt : 0 < i
State after:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
⊢ i = 0

case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0

State before:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
⊢ i = 0

case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Tactic:
. have := h.mpr hLt; linarith
State after:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0

State before:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Tactic:
. have : ¬ 0 < -i := fun h₂ => hLt (h.mp h₂); linarith
State after:
no goals

State before:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
⊢ i = 0
Tactic:
have := h.mpr hLt
State after:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
this : 0 < -i
⊢ i = 0

State before:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
this : 0 < -i
⊢ i = 0
Tactic:
linarith
State after:
no goals

State before:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Tactic:
have : ¬ 0 < -i := fun h₂ => hLt (h.mp h₂)
State after:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
this : ¬0 < -i
⊢ i = 0

State before:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
this : ¬0 < -i
⊢ i = 0
Tactic:
linarith
State after:
no goals