internlm/Lean-Github huggingface dataset:
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : ¬0 < N
⊢ False
Tactic:
push_neg at H
Proof state after:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False
Tactic:
rw [le_zero_iff.mp H] at hN
Proof state after:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ 0
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ 0
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ f (x + (a ^ N - x)) = f (a ^ N)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ ↑a ^ N = ↑x + (↑a ^ N - ↑x)
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
⊢ f x + f (a ^ N - x) ≤ ↑x + ↑(a ^ N - x)
Tactic:
exact_mod_cast h2
Proof state after:
no goals
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑b * ↑a - 1 ∣ (n * ↑b ^ 2 - 1) ^ 2
Tactic:
rw [mul_right_comm, sub_sq', add_comm, mul_right_comm _ _ (1 : ℤ), ← sub_sq']
Proof state after:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Tactic:
replace h := dvd_mul_of_dvd_left h ((n * b ^ 2) ^ 2)
Proof state after:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 * (n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 * (n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Tactic:
rw [← mul_pow, sub_one_mul, mul_mul_mul_comm, ← sq, ← mul_pow, ← mul_pow, ← mul_assoc] at h
Proof state after:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Tactic:
rw [← Int.modEq_zero_iff_dvd] at h ⊢
Proof state after:
n : ℤ
a b : ℕ
h : ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
⊢ (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
h : ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
⊢ (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
Tactic:
revert h
Proof state after:
n : ℤ
a b : ℕ
⊢ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1] → (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
⊢ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1] → (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
Tactic:
refine ((Int.ModEq.sub_right _ ?_).pow _).trans
Proof state after:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1]
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1]
Tactic:
nth_rewrite 1 [← one_pow 2]
Proof state after:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1 ^ 2]
Theorem: Imo2007P5.bad_symm
Proof state before:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1 ^ 2]
Tactic:
exact ((n * a * b).modEq_sub 1).symm.pow 2
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof 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⟩
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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⟩
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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⟩
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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 _))
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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⟩
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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]
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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⟩
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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, ?_⟩⟩
Proof 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)
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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)
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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 ⊢
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof 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
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof 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]
Proof state after:
no goals
Theorem: Imo2007P5.bad_exists_descent
Proof 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
Proof 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