Theorem: IMOSL.IMO2019N4.good_is_linear (IMOSLLean4/IMO2019/N4/N4.lean)

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
⊢ ∃ k, f = fun x => k * x
Tactic:
have h0 {n} (h0 : C < n) : f n ≤ n * f 1 := by
  rw [← Nat.succ_le_succ_iff, Nat.succ_eq_one_add, Nat.succ_eq_one_add]
  exact Nat.le_of_dvd (Nat.add_pos_left Nat.one_pos _)
    (h 1 n <| Nat.lt_one_add_iff.mpr h0.le)
State after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
⊢ ∃ k, f = fun x => k * x

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
⊢ ∃ k, f = fun x => k * x
Tactic:
have h1 {p} (h1 : C < p) (h2 : p.Prime) : ∃ k ≤ f 1, f p = k * p := by
  suffices p ∣ f p ^ 2 by
    rcases h2.dvd_of_dvd_pow this with ⟨k, h3⟩
    exact ⟨k, Nat.le_of_mul_le_mul_left (h3.ge.trans (h0 h1)) h2.pos,
      h3.trans (p.mul_comm k)⟩
  rcases exists_gt (C + f p) with ⟨n, h3⟩
  replace h3 := Nat.exists_eq_add_of_le <|
    h3.le.trans (Nat.le_mul_of_pos_right _ h2.pos)
  rcases h3 with ⟨a, h3⟩; rw [add_right_comm] at h3
  specialize h (C + a) p <|
    (C.le_add_right a).trans_lt (Nat.lt_add_of_pos_right h2.pos)
  replace h3 : p ∣ C + a + f p := ⟨n, h3.symm.trans (n.mul_comm p)⟩
  rw [← dvd_sq_iff_dvd_sq_of_dvd_add h3, dvd_iff_of_dvd_add (h3.trans h)]
  exact p.dvd_mul_right _
State after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
⊢ ∃ k, f = fun x => k * x

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
⊢ ∃ k, f = fun x => k * x
Tactic:
rcases C.succ.exists_infinite_primes with ⟨p, (h3 : C < p), h4⟩
State after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
⊢ ∃ k, f = fun x => k * x

State before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
⊢ ∃ k, f = fun x => k * x
Tactic:
rcases h1 h3 h4 with ⟨k, -, h5⟩
State after:
case intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
⊢ ∃ k, f = fun x => k * x

State before:
case intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
⊢ ∃ k, f = fun x => k * x
Tactic:
refine ⟨k, funext λ n ↦ ?_⟩
State after:
case intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n : ℕ
⊢ f n = k * n

State before:
case intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n : ℕ
⊢ f n = k * n
Tactic:
rcases h2 p with ⟨Bp, hp⟩
State after:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
⊢ f n = k * n
Tactic:
rcases h2 n with ⟨Bn, hn⟩
State after:
case intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
⊢ f n = k * n
Tactic:
rcases (max Bp Bn).succ.exists_infinite_primes with ⟨q, h6, h7⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : (max Bp Bn).succ ≤ q
h7 : q.Prime
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : (max Bp Bn).succ ≤ q
h7 : q.Prime
⊢ f n = k * n
Tactic:
rw [Nat.succ_le_iff, max_lt_iff] at h6
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
⊢ f n = k * n
Tactic:
specialize hp q h7 h6.1
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
hp : ∃ k, f q = k * q ∧ f p = k * p
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
hp : ∃ k, f q = k * q ∧ f p = k * p
⊢ f n = k * n
Tactic:
rcases hp with ⟨kp, h8, h9⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : f p = kp * p
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : f p = kp * p
⊢ f n = k * n
Tactic:
rw [h5, Nat.mul_left_inj h4.ne_zero] at h9
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
⊢ f n = k * n
Tactic:
specialize hn q h7 h6.2
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
hn : ∃ k, f q = k * q ∧ f n = k * n
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
hn : ∃ k, f q = k * q ∧ f n = k * n
⊢ f n = k * n
Tactic:
rcases hn with ⟨kn, h10, h11⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : f q = kn * q
h11 : f n = kn * n
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : f q = kn * q
h11 : f n = kn * n
⊢ f n = k * n
Tactic:
rw [h8, Nat.mul_left_inj h7.ne_zero] at h10
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : kp = kn
h11 : f n = kn * n
⊢ f n = k * n

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : kp = kn
h11 : f n = kn * n
⊢ f n = k * n
Tactic:
rw [h11, ← h10, ← h9]
State after:
no goals

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
n : ℕ
h0 : C < n
⊢ f n ≤ n * f 1
Tactic:
rw [← Nat.succ_le_succ_iff, Nat.succ_eq_one_add, Nat.succ_eq_one_add]
State after:
C : ℕ
f : ℕ → ℕ
h : good C f
n : ℕ
h0 : C < n
⊢ 1 + f n ≤ 1 + n * f 1

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
n : ℕ
h0 : C < n
⊢ 1 + f n ≤ 1 + n * f 1
Tactic:
exact Nat.le_of_dvd (Nat.add_pos_left Nat.one_pos _)
  (h 1 n <| Nat.lt_one_add_iff.mpr h0.le)
State after:
no goals

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
⊢ ∃ k ≤ f 1, f p = k * p
Tactic:
suffices p ∣ f p ^ 2 by
  rcases h2.dvd_of_dvd_pow this with ⟨k, h3⟩
  exact ⟨k, Nat.le_of_mul_le_mul_left (h3.ge.trans (h0 h1)) h2.pos,
    h3.trans (p.mul_comm k)⟩
State after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
⊢ p ∣ f p ^ 2

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
⊢ p ∣ f p ^ 2
Tactic:
rcases exists_gt (C + f p) with ⟨n, h3⟩
State after:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : C + f p < n
⊢ p ∣ f p ^ 2

State before:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : C + f p < n
⊢ p ∣ f p ^ 2
Tactic:
replace h3 := Nat.exists_eq_add_of_le <|
  h3.le.trans (Nat.le_mul_of_pos_right _ h2.pos)
State after:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : ∃ k, n * p = C + f p + k
⊢ p ∣ f p ^ 2

State before:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : ∃ k, n * p = C + f p + k
⊢ p ∣ f p ^ 2
Tactic:
rcases h3 with ⟨a, h3⟩
State after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + f p + a
⊢ p ∣ f p ^ 2

State before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + f p + a
⊢ p ∣ f p ^ 2
Tactic:
rw [add_right_comm] at h3
State after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
⊢ p ∣ f p ^ 2

State before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
⊢ p ∣ f p ^ 2
Tactic:
specialize h (C + a) p <|
  (C.le_add_right a).trans_lt (Nat.lt_add_of_pos_right h2.pos)
State after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
⊢ p ∣ f p ^ 2

State before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
⊢ p ∣ f p ^ 2
Tactic:
replace h3 : p ∣ C + a + f p := ⟨n, h3.symm.trans (n.mul_comm p)⟩
State after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ f p ^ 2

State before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ f p ^ 2
Tactic:
rw [← dvd_sq_iff_dvd_sq_of_dvd_add h3, dvd_iff_of_dvd_add (h3.trans h)]
State after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ p * f (C + a)

State before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ p * f (C + a)
Tactic:
exact p.dvd_mul_right _
State after:
no goals

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
this : p ∣ f p ^ 2
⊢ ∃ k ≤ f 1, f p = k * p
Tactic:
rcases h2.dvd_of_dvd_pow this with ⟨k, h3⟩
State after:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
this : p ∣ f p ^ 2
k : ℕ
h3 : f p = p * k
⊢ ∃ k ≤ f 1, f p = k * p

State before:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
this : p ∣ f p ^ 2
k : ℕ
h3 : f p = p * k
⊢ ∃ k ≤ f 1, f p = k * p
Tactic:
exact ⟨k, Nat.le_of_mul_le_mul_left (h3.ge.trans (h0 h1)) h2.pos,
  h3.trans (p.mul_comm k)⟩
State after:
no goals

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x : ℕ
⊢ ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
Tactic:
refine ⟨max C (max (f x) (max (x * f 1) (x ^ 2))), λ p h2 h3 ↦ ?_⟩
State after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : max C (max (f x) (max (x * f 1) (x ^ 2))) < p
⊢ ∃ k, f p = k * p ∧ f x = k * x

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : max C (max (f x) (max (x * f 1) (x ^ 2))) < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
rw [max_lt_iff, max_lt_iff, max_lt_iff] at h3
State after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : C < p ∧ f x < p ∧ x * f 1 < p ∧ x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : C < p ∧ f x < p ∧ x * f 1 < p ∧ x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
rcases h3 with ⟨hp1, hp2, hp3, hp4⟩
State after:
case intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x

State before:
case intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
rcases h1 hp1 h2 with ⟨k, h3, h4⟩
State after:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ ∃ k, f p = k * p ∧ f x = k * x

State before:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
refine ⟨k, h4, ?_⟩
State after:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ f x = k * x
Tactic:
rcases (f x).eq_zero_or_pos with h5 | h5
State after:
case intro.intro.intro.intro.intro.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
⊢ f x = k * x

case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
⊢ f x = k * x
Tactic:
rcases k.eq_zero_or_pos with rfl | h6
State after:
case intro.intro.intro.intro.intro.inl.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
h5 : f x = 0
h3 : 0 ≤ f 1
h4 : f p = 0 * p
⊢ f x = 0 * x

case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro.inl.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
h5 : f x = 0
h3 : 0 ≤ f 1
h4 : f p = 0 * p
⊢ f x = 0 * x
Tactic:
rw [h5, zero_mul]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ f x = k * x
Tactic:
suffices x ^ 2 = 0 by rw [h5, pow_eq_zero this, mul_zero]
State after:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ x ^ 2 = 0

State before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ x ^ 2 = 0
Tactic:
specialize h x p (Nat.lt_add_left x hp1)
State after:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + f p ∣ x ^ 2 + p * f x
⊢ x ^ 2 = 0

State before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + f p ∣ x ^ 2 + p * f x
⊢ x ^ 2 = 0
Tactic:
rw [h5, mul_zero, add_zero, h4] at h
State after:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + k * p ∣ x ^ 2
⊢ x ^ 2 = 0

State before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + k * p ∣ x ^ 2
⊢ x ^ 2 = 0
Tactic:
exact Nat.eq_zero_of_dvd_of_lt h <|
  Nat.lt_add_left x (lt_mul_of_one_le_of_lt h6 hp4)
State after:
no goals

State before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
this : x ^ 2 = 0
⊢ f x = k * x
Tactic:
rw [h5, pow_eq_zero this, mul_zero]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
⊢ f x = k * x
Tactic:
specialize h p x (Nat.lt_add_right x hp1)
State after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ f x = k * x
Tactic:
have h6 : (p + f x).Coprime p := by
  rw [Nat.coprime_self_add_left, Nat.coprime_comm, h2.coprime_iff_not_dvd]
  exact Nat.not_dvd_of_pos_of_lt h5 hp2
State after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
h6 : (p + f x).Coprime p
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
h6 : (p + f x).Coprime p
⊢ f x = k * x
Tactic:
rw [sq, h4, ← mul_assoc, ← add_mul, h6.dvd_mul_right] at h
State after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
h6 : (p + f x).Coprime p
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
h6 : (p + f x).Coprime p
⊢ f x = k * x
Tactic:
clear h6
State after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
⊢ f x = k * x
Tactic:
rcases h with ⟨_ | _ | t, h⟩
State after:
case intro.intro.intro.intro.intro.inr.intro.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * 0
⊢ f x = k * x

case intro.intro.intro.intro.intro.inr.intro.succ.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * (0 + 1)
⊢ f x = k * x

case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * (t + 1 + 1)
⊢ f x = k * x

State before:
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ (p + f x).Coprime p
Tactic:
rw [Nat.coprime_self_add_left, Nat.coprime_comm, h2.coprime_iff_not_dvd]
State after:
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ ¬p ∣ f x

State before:
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ ¬p ∣ f x
Tactic:
exact Nat.not_dvd_of_pos_of_lt h5 hp2
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.intro.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * 0
⊢ f x = k * x
Tactic:
exact h.not_gt.elim (Nat.lt_add_right _ h2.pos)
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.intro.succ.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * (0 + 1)
⊢ f x = k * x
Tactic:
rwa [Nat.mul_one, add_right_inj, eq_comm, mul_comm] at h
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * (t + 1 + 1)
⊢ f x = k * x
Tactic:
rw [add_assoc, mul_add, add_mul _ _ 2] at h
State after:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ f x = k * x

State before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ f x = k * x
Tactic:
refine h.not_lt.elim (Nat.lt_add_left _ (Nat.lt_add_right _ ?_))
State after:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ p + x * k < p * 2

State before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ p + x * k < p * 2
Tactic:
rw [mul_two, add_lt_add_iff_left]
State after:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ x * k < p

State before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ x * k < p
Tactic:
exact hp3.trans_le' (Nat.mul_le_mul_left x h3)
State after:
no goals