Theorem: Imo2007P5.bad_exists_descent (Compfiles/Imo2007P5.lean)

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a ∧ ∃ b, a < b ∧ n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
rcases h with ⟨h, b, h0, k, h1⟩
State after:
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k : ℤ
h1 : (n * ↑a ^ 2 - 1) ^ 2 = (n * ↑a * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2

State before:
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k : ℤ
h1 : (n * ↑a ^ 2 - 1) ^ 2 = (n * ↑a * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
rw [sq (a : ℤ), ← mul_assoc] at h1
State after:
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k : ℤ
h1 : (n * ↑a * ↑a - 1) ^ 2 = (n * ↑a * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2

State before:
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k : ℤ
h1 : (n * ↑a * ↑a - 1) ^ 2 = (n * ↑a * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
generalize ht : n * a = t at h1
State after:
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2

State before:
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
obtain ⟨c, rfl⟩ : ∃ c : ℤ, k = t * c - 1 := by
  replace h1 : (t * a - 1) ^ 2 ≡ (t * b - 1) * k [ZMOD t] := by rw [h1]
  have X : ∀ m : ℤ, t * m - 1 ≡ -1 [ZMOD t] := fun m ↦ by
    symm; rw [Int.modEq_iff_dvd, sub_neg_eq_add, sub_add_cancel]; exact ⟨m, rfl⟩
  replace h1 := ((X a).pow 2).symm.trans (h1.trans ((X b).mul_right _))
  rw [Int.modEq_iff_dvd, sq, ← mul_sub, sub_neg_eq_add, neg_one_mul, dvd_neg] at h1
  cases' h1 with c h1
  exact ⟨c, eq_sub_of_add_eq h1⟩
State after:
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2

State before:
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
suffices h2 : c < a ∧ 0 < c by
  lift c to ℕ using le_of_lt h2.2
  rw [Int.natCast_pos, Int.ofNat_lt] at h2
  refine ⟨c, h2.2, h2.1, bad_symm ⟨t * b - 1, ?_⟩⟩
  rw [sq (a : ℤ), ← mul_assoc, ht, h1, mul_comm]
State after:
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ c < ↑a ∧ 0 < c

State before:
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ c < ↑a ∧ 0 < c
Tactic:
replace ht : 1 < t := by
  rw [← Int.natCast_pos] at h
  have h2 := le_trans Int.one_nonneg (le_of_lt hn)
  rw [Int.lt_iff_add_one_le] at hn h ⊢
  rw [← ht]
  exact le_mul_of_le_of_one_le_of_nonneg hn h h2
State after:
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
⊢ c < ↑a ∧ 0 < c

State before:
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
⊢ c < ↑a ∧ 0 < c
Tactic:
clear hn n
State after:
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
⊢ c < ↑a ∧ 0 < c

State before:
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
⊢ c < ↑a ∧ 0 < c
Tactic:
have h2 := lt_trans one_pos ht
State after:
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
⊢ c < ↑a ∧ 0 < c

State before:
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
⊢ c < ↑a ∧ 0 < c
Tactic:
have h3 : ∀ x y : ℤ, x < y ↔ t * x - 1 < t * y - 1 :=
  λ x y ↦ by rw [sub_lt_sub_iff_right, ← mul_lt_mul_left h2]
State after:
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

State before:
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
Tactic:
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
State after:
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

State before:
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
Tactic:
rw [← Int.natCast_pos, h2] at h
State after:
case intro.intro.intro.intro.intro
a b : ℕ
h0 : a < b
t : ℤ
h : 0 < t * ↑a - 1
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

State before:
case intro.intro.intro.intro.intro
a b : ℕ
h0 : a < b
t : ℤ
h : 0 < t * ↑a - 1
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
Tactic:
rw [← Int.ofNat_lt, h3] at h0
State after:
case intro.intro.intro.intro.intro
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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

State before:
case intro.intro.intro.intro.intro
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
Tactic:
rw [h2, h3 c]
State after:
case intro.intro.intro.intro.intro
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ t * c - 1 < t * ↑a - 1 ∧ 0 < t * c - 1

State before:
case intro.intro.intro.intro.intro
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ t * c - 1 < t * ↑a - 1 ∧ 0 < t * c - 1
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.left
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ t * c - 1 < t * ↑a - 1

case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ 0 < t * c - 1

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * k
⊢ ∃ c, k = t * c - 1
Tactic:
replace h1 : (t * a - 1) ^ 2 ≡ (t * b - 1) * k [ZMOD t] := by rw [h1]
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
⊢ ∃ c, k = t * c - 1

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
⊢ ∃ c, k = t * c - 1
Tactic:
have X : ∀ m : ℤ, t * m - 1 ≡ -1 [ZMOD t] := fun m ↦ by
  symm; rw [Int.modEq_iff_dvd, sub_neg_eq_add, sub_add_cancel]; exact ⟨m, rfl⟩
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
⊢ ∃ c, k = t * c - 1

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
⊢ ∃ c, k = t * c - 1
Tactic:
replace h1 := ((X a).pow 2).symm.trans (h1.trans ((X b).mul_right _))
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
h1 : (-1) ^ 2 ≡ -1 * k [ZMOD t]
⊢ ∃ c, k = t * c - 1

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
h1 : (-1) ^ 2 ≡ -1 * k [ZMOD t]
⊢ ∃ c, k = t * c - 1
Tactic:
rw [Int.modEq_iff_dvd, sq, ← mul_sub, sub_neg_eq_add, neg_one_mul, dvd_neg] at h1
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
h1 : t ∣ k + 1
⊢ ∃ c, k = t * c - 1

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
h1 : t ∣ k + 1
⊢ ∃ c, k = t * c - 1
Tactic:
cases' h1 with c h1
State after:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
c : ℤ
h1 : k + 1 = t * c
⊢ ∃ c, k = t * c - 1

State before:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
c : ℤ
h1 : k + 1 = t * c
⊢ ∃ c, k = t * c - 1
Tactic:
exact ⟨c, eq_sub_of_add_eq h1⟩
State after:
no goals

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * k
⊢ (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
Tactic:
rw [h1]
State after:
no goals

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
m : ℤ
⊢ t * m - 1 ≡ -1 [ZMOD t]
Tactic:
symm
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
m : ℤ
⊢ -1 ≡ t * m - 1 [ZMOD t]

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
m : ℤ
⊢ -1 ≡ t * m - 1 [ZMOD t]
Tactic:
rw [Int.modEq_iff_dvd, sub_neg_eq_add, sub_add_cancel]
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
m : ℤ
⊢ t ∣ t * m

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 ≡ (t * ↑b - 1) * k [ZMOD t]
m : ℤ
⊢ t ∣ t * m
Tactic:
exact ⟨m, rfl⟩
State after:
no goals

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : c < ↑a ∧ 0 < c
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
lift c to ℕ using le_of_lt h2.2
State after:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℕ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * ↑c - 1)
h2 : ↑c < ↑a ∧ 0 < ↑c
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2

State before:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℕ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * ↑c - 1)
h2 : ↑c < ↑a ∧ 0 < ↑c
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
rw [Int.natCast_pos, Int.ofNat_lt] at h2
State after:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℕ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * ↑c - 1)
h2 : c < a ∧ 0 < c
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2

State before:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℕ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * ↑c - 1)
h2 : c < a ∧ 0 < c
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
Tactic:
refine ⟨c, h2.2, h2.1, bad_symm ⟨t * b - 1, ?_⟩⟩
State after:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℕ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * ↑c - 1)
h2 : c < a ∧ 0 < c
⊢ (n * ↑a ^ 2 - 1) ^ 2 = (n * ↑a * ↑c - 1) * (t * ↑b - 1)

State before:
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℕ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * ↑c - 1)
h2 : c < a ∧ 0 < c
⊢ (n * ↑a ^ 2 - 1) ^ 2 = (n * ↑a * ↑c - 1) * (t * ↑b - 1)
Tactic:
rw [sq (a : ℤ), ← mul_assoc, ht, h1, mul_comm]
State after:
no goals

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ 1 < t
Tactic:
rw [← Int.natCast_pos] at h
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ 1 < t

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ 1 < t
Tactic:
have h2 := le_trans Int.one_nonneg (le_of_lt hn)
State after:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 < t

State before:
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 < t
Tactic:
rw [Int.lt_iff_add_one_le] at hn h ⊢
State after:
n : ℤ
hn : 1 + 1 ≤ n
a : ℕ
h : 0 + 1 ≤ ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 + 1 ≤ t

State before:
n : ℤ
hn : 1 + 1 ≤ n
a : ℕ
h : 0 + 1 ≤ ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 + 1 ≤ t
Tactic:
rw [← ht]
State after:
n : ℤ
hn : 1 + 1 ≤ n
a : ℕ
h : 0 + 1 ≤ ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 + 1 ≤ n * ↑a

State before:
n : ℤ
hn : 1 + 1 ≤ n
a : ℕ
h : 0 + 1 ≤ ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 + 1 ≤ n * ↑a
Tactic:
exact le_mul_of_le_of_one_le_of_nonneg hn h h2
State after:
no goals

State before:
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
x y : ℤ
⊢ x < y ↔ t * x - 1 < t * y - 1
Tactic:
rw [sub_lt_sub_iff_right, ← mul_lt_mul_left h2]
State after:
no goals

State before:
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
⊢ ∀ (x : ℤ), 0 < x ↔ 0 < t * x - 1
Tactic:
intro x
State after:
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
x : ℤ
⊢ 0 < x ↔ 0 < t * x - 1

State before:
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
x : ℤ
⊢ 0 < x ↔ 0 < t * x - 1
Tactic:
rw [h3, mul_zero, Int.lt_iff_add_one_le, sub_add_cancel, le_iff_eq_or_lt]
State after:
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
x : ℤ
⊢ 0 = t * x - 1 ∨ 0 < t * x - 1 ↔ 0 < t * x - 1

State before:
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
x : ℤ
⊢ 0 = t * x - 1 ∨ 0 < t * x - 1 ↔ 0 < t * x - 1
Tactic:
refine or_iff_right (λ h4 ↦ ne_of_gt ht ?_)
State after:
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
x : ℤ
h4 : 0 = t * x - 1
⊢ t = 1

State before:
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
x : ℤ
h4 : 0 = t * x - 1
⊢ t = 1
Tactic:
rw [eq_comm, sub_eq_zero] at h4
State after:
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
x : ℤ
h4 : t * x = 1
⊢ t = 1

State before:
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
x : ℤ
h4 : t * x = 1
⊢ t = 1
Tactic:
exact Int.eq_one_of_mul_eq_one_right (le_of_lt h2) h4
State after:
no goals

State before:
case intro.intro.intro.intro.intro.left
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ t * c - 1 < t * ↑a - 1
Tactic:
rwa [← mul_lt_mul_left (lt_trans h h0), ← h1, sq, mul_lt_mul_right h]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ 0 < t * c - 1
Tactic:
rw [← mul_lt_mul_left (lt_trans h h0), mul_zero, ← h1]
State after:
case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ 0 < (t * ↑a - 1) ^ 2

State before:
case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
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
⊢ 0 < (t * ↑a - 1) ^ 2
Tactic:
exact pow_pos h 2
State after:
no goals