replace h2 : ∀ x : ℤ, 0 < x ↔ 0 < t * x - 1 := by
  intro x
  rw [h3, mul_zero, Int.lt_iff_add_one_le, sub_add_cancel, le_iff_eq_or_lt]
  refine or_iff_right (λ h4 ↦ ne_of_gt ht ?_)
  rw [eq_comm, sub_eq_zero] at h4
  exact Int.eq_one_of_mul_eq_one_right (le_of_lt h2) h4
case intro.intro.intro.intro.intro
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
⊢ c < ↑a ∧ 0 < c
case intro.intro.intro.intro.intro
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
h2 : ∀ (x : ℤ), 0 < x ↔ 0 < t * x - 1
⊢ c < ↑a ∧ 0 < c