[GOAL]
n : ℕ
⊢ Nat.IsSqrt n (sqrt n)
[PROOFSTEP]
match n with
| 0 => simp [IsSqrt]
| 1 => simp [IsSqrt]
| n + 2 =>
  have h : ¬(n + 2) ≤ 1 := by simp
  simp only [IsSqrt, sqrt, h, ite_false]
  refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
  simp only [mul_add, add_mul, one_mul, mul_one, ← add_assoc]
  rw [lt_add_one_iff, add_assoc, ← mul_two]
  refine le_trans (div_add_mod' (n + 2) 2).ge ?_
  rw [add_comm, add_le_add_iff_right, add_mod_right]
  simp only [zero_lt_two, add_div_right, succ_mul_succ_eq]
  refine le_trans (b := 1) ?_ ?_
  · exact (lt_succ.1 $ mod_lt n zero_lt_two)
  · simp only [le_add_iff_nonneg_left]; exact zero_le _
[GOAL]
n : ℕ
⊢ Nat.IsSqrt 0 (sqrt 0)
[PROOFSTEP]
simp [IsSqrt]
[GOAL]
n : ℕ
⊢ Nat.IsSqrt 1 (sqrt 1)
[PROOFSTEP]
simp [IsSqrt]
[GOAL]
n✝ n : ℕ
⊢ Nat.IsSqrt (n + 2) (sqrt (n + 2))
[PROOFSTEP]
have h : ¬(n + 2) ≤ 1 := by simp
[GOAL]
n✝ n : ℕ
⊢ ¬n + 2 ≤ 1
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ Nat.IsSqrt (n + 2) (sqrt (n + 2))
[PROOFSTEP]
simp only [IsSqrt, sqrt, h, ite_false]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ sqrt.iter (n + 2) ((n + 2) / 2) * sqrt.iter (n + 2) ((n + 2) / 2) ≤ n + 2 ∧
    n + 2 < (sqrt.iter (n + 2) ((n + 2) / 2) + 1) * (sqrt.iter (n + 2) ((n + 2) / 2) + 1)
[PROOFSTEP]
refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < ((n + 2) / 2 + 1) * ((n + 2) / 2 + 1)
[PROOFSTEP]
simp only [mul_add, add_mul, one_mul, mul_one, ← add_assoc]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 + (n + 2) / 2 + 1
[PROOFSTEP]
rw [lt_add_one_iff, add_assoc, ← mul_two]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
[PROOFSTEP]
refine le_trans (div_add_mod' (n + 2) 2).ge ?_
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
[PROOFSTEP]
rw [add_comm, add_le_add_iff_right, add_mod_right]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ (n + 2) / 2 * ((n + 2) / 2)
[PROOFSTEP]
simp only [zero_lt_two, add_div_right, succ_mul_succ_eq]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
[PROOFSTEP]
refine le_trans (b := 1) ?_ ?_
[GOAL]
case refine_1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ 1
[PROOFSTEP]
exact (lt_succ.1 $ mod_lt n zero_lt_two)
[GOAL]
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 1 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
[PROOFSTEP]
simp only [le_add_iff_nonneg_left]
[GOAL]
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 0 ≤ n / 2 * (n / 2) + n / 2 + n / 2
[PROOFSTEP]
exact zero_le _
[GOAL]
n : ℕ
⊢ n ≤ sqrt n * sqrt n + sqrt n + sqrt n
[PROOFSTEP]
rw [← succ_mul]
[GOAL]
n : ℕ
⊢ n ≤ succ (sqrt n) * sqrt n + sqrt n
[PROOFSTEP]
exact le_of_lt_succ (lt_succ_sqrt n)
[GOAL]
m n : ℕ
⊢ m ≤ sqrt n ↔ m ^ 2 ≤ n
[PROOFSTEP]
simpa only [pow_two] using le_sqrt
[GOAL]
n : ℕ
h : sqrt n = 0
⊢ sqrt n < 1
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
h : sqrt n = 0
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ n = 0 → sqrt n = 0
[PROOFSTEP]
rintro rfl
[GOAL]
⊢ sqrt 0 = 0
[PROOFSTEP]
simp
[GOAL]
n q : ℕ
⊢ q = sqrt n ↔ q ^ 2 ≤ n ∧ n < (q + 1) ^ 2
[PROOFSTEP]
simpa only [pow_two] using eq_sqrt
[GOAL]
n : ℕ
h : sqrt n = 1
⊢ sqrt n < 2
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
h : sqrt n = 1
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
h : 1 < n
⊢ n < n * n
[PROOFSTEP]
have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h)
[GOAL]
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n
[PROOFSTEP]
rwa [mul_one] at this
[GOAL]
n a : ℕ
h : a ≤ n + n
⊢ n * n + a < succ n * succ n
[PROOFSTEP]
rw [succ_mul, mul_succ, add_succ, add_assoc]
[GOAL]
n a : ℕ
h : a ≤ n + n
⊢ n * n + a < succ (n * n + (n + n))
[PROOFSTEP]
exact lt_succ_of_le (Nat.add_le_add_left h _)
[GOAL]
n : ℕ
⊢ sqrt n * sqrt n + sqrt n ≤ Nat.mul (succ (succ (sqrt n))) (succ (sqrt n))
[PROOFSTEP]
refine' add_le_add (Nat.mul_le_mul_right _ _) _
[GOAL]
case refine'_1
n : ℕ
⊢ sqrt n ≤ succ (succ (sqrt n))
[PROOFSTEP]
exact Nat.le_add_right _ 2
[GOAL]
case refine'_2
n : ℕ
⊢ sqrt n ≤ succ (succ (sqrt n))
[PROOFSTEP]
exact Nat.le_add_right _ 2
[GOAL]
x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [← hn, sqrt_eq]
[GOAL]
x : ℕ
⊢ (∃ n, n ^ 2 = x) ↔ sqrt x ^ 2 = x
[PROOFSTEP]
simpa only [pow_two] using exists_mul_self x
[GOAL]
n m : ℕ
hl : m * m < n
hr : n < (m + 1) * (m + 1)
⊢ ¬∃ t, t * t = n
[PROOFSTEP]
rintro ⟨t, rfl⟩
[GOAL]
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False
[PROOFSTEP]
have h1 : m < t := Nat.mul_self_lt_mul_self_iff.mpr hl
[GOAL]
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False
[PROOFSTEP]
have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.mpr hr
[GOAL]
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False
[PROOFSTEP]
exact (not_lt_of_ge <| le_of_lt_succ h2) h1
[GOAL]
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ ¬∃ t, t ^ 2 = n
[PROOFSTEP]
simpa only [pow_two] using not_exists_sq (by simpa only [pow_two] using hl) (by simpa only [pow_two] using hr)
[GOAL]
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ ?m.11228 * ?m.11228 < n
[PROOFSTEP]
simpa only [pow_two] using hl
[GOAL]
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ n < (m + 1) * (m + 1)
[PROOFSTEP]
simpa only [pow_two] using hr


[GOAL]
s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h =>
  subst h
  simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
    not_false_iff]
| inr h => simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
s : Set ℕ
x✝ : s = ∅ ∨ Set.Nonempty s
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h =>
  subst h
  simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
    not_false_iff]
| inr h => simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]

| inl h =>
  subst h
  simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
    not_false_iff]
[GOAL]
case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
subst h
[GOAL]
case inl
⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅
[PROOFSTEP]
simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
  not_false_iff]
[GOAL]
case inr
s : Set ℕ
h : Set.Nonempty s
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]

| inr h => simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
case inr
s : Set ℕ
h : Set.Nonempty s
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
⊢ sInf ∅ = 0
[PROOFSTEP]
rw [sInf_eq_zero]
[GOAL]
⊢ 0 ∈ ∅ ∨ ∅ = ∅
[PROOFSTEP]
right
[GOAL]
case h
⊢ ∅ = ∅
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0
[PROOFSTEP]
rw [iInf_of_empty', sInf_empty]
[GOAL]
s : Set ℕ
h : Set.Nonempty s
⊢ sInf s ∈ s
[PROOFSTEP]
rw [Nat.sInf_def h]
[GOAL]
s : Set ℕ
h : Set.Nonempty s
⊢ Nat.find h ∈ s
[PROOFSTEP]
exact Nat.find_spec h
[GOAL]
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ ¬m ∈ s
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h => subst h; apply not_mem_empty
| inr h => rw [Nat.sInf_def h] at hm ; exact Nat.find_min h hm
[GOAL]
s : Set ℕ
m : ℕ
hm : m < sInf s
x✝ : s = ∅ ∨ Set.Nonempty s
⊢ ¬m ∈ s
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h => subst h; apply not_mem_empty
| inr h => rw [Nat.sInf_def h] at hm ; exact Nat.find_min h hm
[GOAL]
case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ ¬m ∈ s
[PROOFSTEP]

| inl h => subst h; apply not_mem_empty
[GOAL]
case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ ¬m ∈ s
[PROOFSTEP]
subst h
[GOAL]
case inl
m : ℕ
hm : m < sInf ∅
⊢ ¬m ∈ ∅
[PROOFSTEP]
apply not_mem_empty
[GOAL]
case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : Set.Nonempty s
⊢ ¬m ∈ s
[PROOFSTEP]

| inr h => rw [Nat.sInf_def h] at hm ; exact Nat.find_min h hm
[GOAL]
case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : Set.Nonempty s
⊢ ¬m ∈ s
[PROOFSTEP]
rw [Nat.sInf_def h] at hm
[GOAL]
case inr
s : Set ℕ
m : ℕ
h : Set.Nonempty s
hm : m < Nat.find h
⊢ ¬m ∈ s
[PROOFSTEP]
exact Nat.find_min h hm
[GOAL]
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m
[PROOFSTEP]
rw [Nat.sInf_def ⟨m, hm⟩]
[GOAL]
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find (_ : ∃ x, x ∈ s) ≤ m
[PROOFSTEP]
exact Nat.find_min' ⟨m, hm⟩ hm
[GOAL]
s : Set ℕ
h : 0 < sInf s
⊢ Set.Nonempty s
[PROOFSTEP]
by_contra contra
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : ¬Set.Nonempty s
⊢ False
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty] at contra
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False
[PROOFSTEP]
have h' : sInf s ≠ 0 := ne_of_gt h
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False
[PROOFSTEP]
apply h'
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0
[PROOFSTEP]
rw [Nat.sInf_eq_zero]
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
right
[GOAL]
case h
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅
[PROOFSTEP]
assumption
[GOAL]
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
intro H
[GOAL]
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
[GOAL]
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ
s : Set ℕ hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s k : ℕ H : sInf s = k + 1 ⊢ sInf s = ?m.6254 + 1
[PROOFSTEP]
exact ⟨le_rfl, k.not_succ_le_self⟩
[GOAL]
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ
s : Set ℕ hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s k : ℕ H : sInf s = k + 1 ⊢ sInf s = ?m.6254 + 1
[PROOFSTEP]
exact k
[GOAL]
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1
[PROOFSTEP]
assumption
[GOAL]
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ ¬k ∈ s → sInf s = k + 1
[PROOFSTEP]
rintro ⟨H, H'⟩
[GOAL]
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : ¬k ∈ s
⊢ sInf s = k + 1
[PROOFSTEP]
rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
[GOAL]
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : ¬k ∈ s
⊢ k + 1 ∈ s ∧ ∀ (n : ℕ), n < k + 1 → ¬n ∈ s
[PROOFSTEP]
exact ⟨H, fun n hnk hns ↦ H' <| hs n k (lt_succ_iff.mp hnk) hns⟩
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hb : BddAbove s
ha : a ∈ s
⊢ a ≤ sSup s
[PROOFSTEP]
rw [sSup_def hb]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hb : BddAbove s
ha : a ∈ s
⊢ a ≤ Nat.find hb
[PROOFSTEP]
revert a ha
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hb : BddAbove s
⊢ ∀ (a : ℕ), a ∈ s → a ≤ Nat.find hb
[PROOFSTEP]
exact @Nat.find_spec _ _ hb
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : Set.Nonempty s
ha : a ∈ upperBounds s
⊢ sSup s ≤ a
[PROOFSTEP]
rw [sSup_def ⟨a, ha⟩]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : Set.Nonempty s
ha : a ∈ upperBounds s
⊢ Nat.find (_ : ∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n) ≤ a
[PROOFSTEP]
exact Nat.find_min' _ ha
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : BddBelow s
ha : a ∈ s
⊢ sInf s ≤ a
[PROOFSTEP]
rw [sInf_def ⟨a, ha⟩]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : BddBelow s
ha : a ∈ s
⊢ Nat.find (_ : ∃ x, x ∈ s) ≤ a
[PROOFSTEP]
exact Nat.find_min' _ ha
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hs : Set.Nonempty s
hb : a ∈ lowerBounds s
⊢ a ≤ sInf s
[PROOFSTEP]
rw [sInf_def hs]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hs : Set.Nonempty s
hb : a ∈ lowerBounds s
⊢ a ≤ Nat.find hs
[PROOFSTEP]
exact hb (@Nat.find_spec (fun n ↦ n ∈ s) _ _)
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ ∀ (s : Set ℕ), ¬BddAbove s → sSup s = sSup univ
[PROOFSTEP]
intro s hs
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ sSup s = sSup univ
[PROOFSTEP]
simp only [mem_univ, forall_true_left, sSup]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ (if h : ∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n then Nat.find h else 0) =
    if h : ∃ n, ∀ (a : ℕ), a ≤ n then Nat.find (_ : ∃ n, (fun n => ∀ (a : ℕ), a ≤ n) n) else 0
[PROOFSTEP]
rw [dif_neg, dif_neg]
[GOAL]
case hnc
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ (a : ℕ), a ≤ n
[PROOFSTEP]
simp only [not_exists, not_forall, not_le]
[GOAL]
case hnc
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ ∀ (x : ℕ), ∃ x_1, x < x_1
[PROOFSTEP]
exact fun n ↦ ⟨n + 1, lt.base n⟩
[GOAL]
case hnc
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n
[PROOFSTEP]
exact hs
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddBelow s
⊢ sInf s = sInf univ
[PROOFSTEP]
simp at hs
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ sSup ∅ = ⊥
[PROOFSTEP]
simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false, not_false_iff, exists_const]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ Nat.find (_ : ∃ n, (fun n => True) n) = ⊥
[PROOFSTEP]
apply bot_unique (Nat.find_min' _ _)
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ True
[PROOFSTEP]
trivial
[GOAL]
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
obtain h | ⟨m, hm⟩ := {m | p (m + n)}.eq_empty_or_nonempty
[GOAL]
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
rw [h, Nat.sInf_empty, zero_add]
[GOAL]
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ n = sInf {m | p m}
[PROOFSTEP]
obtain hnp | hnp := hn.eq_or_lt
[GOAL]
case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}
[PROOFSTEP]
exact hnp
[GOAL]
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}
[PROOFSTEP]
suffices hp : p (sInf {m | p m} - n + n)
[GOAL]
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
hp : p (sInf {m | p m} - n + n)
⊢ n = sInf {m | p m}
[PROOFSTEP]
exact (h.subset hp).elim
[GOAL]
case hp
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m} - n + n)
[PROOFSTEP]
rw [tsub_add_cancel_of_le hn]
[GOAL]
case hp
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m})
[PROOFSTEP]
exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
have hp : ∃ n, n ∈ {m | p m} := ⟨_, hm⟩
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find (_ : ∃ x, x ∈ {m | p (m + n)}) + n = Nat.find hp
[PROOFSTEP]
rw [Nat.sInf_def hp] at hn
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
hn : n ≤ Nat.find hp
⊢ Nat.find (_ : ∃ x, x ∈ {m | p (m + n)}) + n = Nat.find hp
[PROOFSTEP]
exact find_add hn
[GOAL]
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}
[PROOFSTEP]
suffices h₁ : n ≤ sInf {m | p (m - n)}
[GOAL]
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}
case h₁ n : ℕ p : ℕ → Prop h : 0 < sInf {m | p m} ⊢ n ≤ sInf {m | p (m - n)}
[PROOFSTEP]
convert sInf_add h₁
[GOAL]
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
x✝ : ℕ
⊢ x✝ = x✝ + n - n
[PROOFSTEP]
simp_rw [add_tsub_cancel_right]
[GOAL]
case h₁
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ n ≤ sInf {m | p (m - n)}
[PROOFSTEP]
obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h
[GOAL]
case h₁.intro
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ n ≤ sInf {m | p (m - n)}
[PROOFSTEP]
refine'
  le_csInf ⟨m + n, _⟩ fun b hb ↦
    le_of_not_lt fun hbn ↦ ne_of_mem_of_not_mem _ (not_mem_of_lt_sInf h) (tsub_eq_zero_of_le hbn.le)
[GOAL]
case h₁.intro.refine'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ m + n ∈ {m | p (m - n)}
[PROOFSTEP]
dsimp
[GOAL]
case h₁.intro.refine'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ p (m + n - n)
[PROOFSTEP]
rwa [add_tsub_cancel_right]
[GOAL]
case h₁.intro.refine'_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}
[PROOFSTEP]
exact hb
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ) (_ : k < n + 1), u k = (⨆ (k : ℕ) (_ : k < n), u k) ⊔ u n
[PROOFSTEP]
simp [Nat.lt_succ_iff_lt_or_eq, iSup_or, iSup_sup_eq]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ) (_ : k < n + 1), u k = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)
[PROOFSTEP]
rw [← sup_iSup_nat_succ]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ (i : ℕ) (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)
[PROOFSTEP]
simp


[GOAL]
n : ℕ
⊢ pair (unpair n).fst (unpair n).snd = n
[PROOFSTEP]
dsimp only [unpair]
[GOAL]
n : ℕ
⊢ pair
      (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n)
        else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst
      (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n)
        else (sqrt n, n - sqrt n * sqrt n - sqrt n)).snd =
    n
[PROOFSTEP]
let s := sqrt n
[GOAL]
n : ℕ
s : ℕ := sqrt n
⊢ pair
      (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n)
        else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst
      (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n)
        else (sqrt n, n - sqrt n * sqrt n - sqrt n)).snd =
    n
[PROOFSTEP]
have sm : s * s + (n - s * s) = n := add_tsub_cancel_of_le (sqrt_le _)
[GOAL]
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
⊢ pair
      (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n)
        else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst
      (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n)
        else (sqrt n, n - sqrt n * sqrt n - sqrt n)).snd =
    n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : n - sqrt n * sqrt n < sqrt n
⊢ pair (n - sqrt n * sqrt n, sqrt n).fst (n - sqrt n * sqrt n, sqrt n).snd = n
[PROOFSTEP]
simp [pair, h, sm]
[GOAL]
case neg
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ pair (sqrt n, n - sqrt n * sqrt n - sqrt n).fst (sqrt n, n - sqrt n * sqrt n - sqrt n).snd = n
[PROOFSTEP]
have hl : n - s * s - s ≤ s := tsub_le_iff_left.mpr (tsub_le_iff_left.mpr <| by rw [← add_assoc]; apply sqrt_le_add)
[GOAL]
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ n ≤ s * s + (s + s)
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ n ≤ s * s + s + s
[PROOFSTEP]
apply sqrt_le_add
[GOAL]
case neg
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
hl : n - s * s - s ≤ s
⊢ pair (sqrt n, n - sqrt n * sqrt n - sqrt n).fst (sqrt n, n - sqrt n * sqrt n - sqrt n).snd = n
[PROOFSTEP]
simp [pair, hl.not_lt, add_assoc, add_tsub_cancel_of_le (le_of_not_gt h), sm]
[GOAL]
n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n
[PROOFSTEP]
simpa [H] using pair_unpair n
[GOAL]
a b : ℕ
⊢ unpair (pair a b) = (a, b)
[PROOFSTEP]
dsimp only [pair]
[GOAL]
a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)
[PROOFSTEP]
show unpair (b * b + a) = (a, b)
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)
[PROOFSTEP]
have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
[GOAL]
case pos
a b : ℕ
h : a < b
be : sqrt (b * b + a) = b
⊢ unpair (b * b + a) = (a, b)
[PROOFSTEP]
simp [unpair, be, add_tsub_cancel_right, h]
[GOAL]
case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
[PROOFSTEP]
show unpair (a * a + a + b) = (a, b)
[GOAL]
case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
[PROOFSTEP]
have ae : sqrt (a * a + (a + b)) = a := by
  rw [sqrt_add_eq]
  exact add_le_add_left (le_of_not_gt h) _
[GOAL]
a b : ℕ
h : ¬a < b
⊢ sqrt (a * a + (a + b)) = a
[PROOFSTEP]
rw [sqrt_add_eq]
[GOAL]
case h
a b : ℕ
h : ¬a < b
⊢ a + b ≤ a + a
[PROOFSTEP]
exact add_le_add_left (le_of_not_gt h) _
[GOAL]
case neg
a b : ℕ
h : ¬a < b
ae : sqrt (a * a + (a + b)) = a
⊢ unpair (a * a + a + b) = (a, b)
[PROOFSTEP]
simp [unpair, ae, Nat.not_lt_zero, add_assoc]
[GOAL]
n : ℕ
n1 : 1 ≤ n
⊢ (unpair n).fst < n
[PROOFSTEP]
let s := sqrt n
[GOAL]
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
⊢ (unpair n).fst < n
[PROOFSTEP]
simp [unpair]
[GOAL]
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
⊢ (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n) else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst <
    n
[PROOFSTEP]
by_cases h : n - s * s < s
[GOAL]
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : n - s * s < s
⊢ (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n) else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst <
    n
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : ¬n - s * s < s
⊢ (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n) else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst <
    n
[PROOFSTEP]
simp [h]
[GOAL]
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : n - s * s < s
⊢ n - sqrt n * sqrt n < n
[PROOFSTEP]
exact lt_of_lt_of_le h (sqrt_le_self _)
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : ¬n - s * s < s
⊢ sqrt n < n
[PROOFSTEP]
simp at h
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
⊢ sqrt n < n
[PROOFSTEP]
have s0 : 0 < s := sqrt_pos.2 n1
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
s0 : 0 < s
⊢ sqrt n < n
[PROOFSTEP]
exact lt_of_le_of_lt h (tsub_lt_self n1 (mul_pos s0 s0))
[GOAL]
⊢ unpair 0 = 0
[PROOFSTEP]
rw [unpair]
[GOAL]
⊢ (let s := sqrt 0;
    if 0 - s * s < s then (0 - s * s, s) else (s, 0 - s * s - s)) =
    0
[PROOFSTEP]
simp
[GOAL]
⊢ (unpair 0).fst ≤ 0
[PROOFSTEP]
simp
[GOAL]
a b : ℕ
⊢ a ≤ pair a b
[PROOFSTEP]
simpa using unpair_left_le (pair a b)
[GOAL]
a b : ℕ
⊢ b ≤ pair a b
[PROOFSTEP]
by_cases h : a < b
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ b ≤ pair a b
[PROOFSTEP]
simp [pair, h]
[GOAL]
case neg
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b
[PROOFSTEP]
simp [pair, h]
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ b ≤ b * b + a
[PROOFSTEP]
exact le_trans (le_mul_self _) (Nat.le_add_right _ _)
[GOAL]
n : ℕ
⊢ (unpair n).snd ≤ n
[PROOFSTEP]
simpa using right_le_pair n.unpair.1 n.unpair.2
[GOAL]
a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b
[PROOFSTEP]
by_cases h₁ : a₁ < b
[GOAL]
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ pair a₁ b < pair a₂ b
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ pair a₁ b < pair a₂ b
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
by_cases h₂ : a₂ < b
[GOAL]
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp at h₂
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
apply add_lt_add_of_le_of_lt
[GOAL]
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b ≤ a₂ * a₂
case neg.h₂ a₁ a₂ b : ℕ h : a₁ < a₂ h₁ : a₁ < b h₂ : b ≤ a₂ ⊢ a₁ < a₂ + b
[PROOFSTEP]
exact mul_self_le_mul_self h₂
[GOAL]
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b
[PROOFSTEP]
exact Nat.lt_add_right _ _ _ h
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp at h₁
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp [not_lt_of_gt (lt_of_le_of_lt h₁ h)]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
apply add_lt_add
[GOAL]
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂
case neg.h₂ a₁ a₂ b : ℕ h : a₁ < a₂ h₁ : b ≤ a₁ ⊢ a₁ + b < a₂ + b
[PROOFSTEP]
exact mul_self_lt_mul_self h
[GOAL]
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
[PROOFSTEP]
apply add_lt_add_right
[GOAL]
case neg.h₂.bc
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂
[PROOFSTEP]
by_cases h₁ : a < b₁
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ b₁ * b₁ + a < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
simp [pair, lt_trans h₁ h, h]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ b₁ * b₁ < b₂ * b₂
[PROOFSTEP]
exact mul_self_lt_mul_self h
[GOAL]
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
by_cases h₂ : a < b₂
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a
[PROOFSTEP]
simp at h₁
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ a * a + (a + b₁) < b₂ * b₂ + a
[PROOFSTEP]
rw [add_comm, add_comm _ a, add_assoc, add_lt_add_iff_left]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ + a * a < b₂ * b₂
[PROOFSTEP]
rwa [add_comm, ← sqrt_lt, sqrt_add_eq]
[GOAL]
case pos.h
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ ≤ a + a
[PROOFSTEP]
exact le_trans h₁ (Nat.le_add_left _ _)
[GOAL]
m n : ℕ
⊢ pair m n < (max m n + 1) ^ 2
[PROOFSTEP]
rw [pair, add_sq, mul_one, two_mul, sq, add_assoc, add_assoc]
[GOAL]
m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
cases' (lt_or_le m n) with h h
[GOAL]
case inl
m n : ℕ
h : m < n
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
case inr
m n : ℕ
h : n ≤ m
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
rw [if_pos h, max_eq_right h.le, add_lt_add_iff_left, add_assoc]
[GOAL]
case inl
m n : ℕ
h : m < n
⊢ m < n + (n + 1 ^ 2)
case inr
m n : ℕ
h : n ≤ m
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
exact h.trans_le (self_le_add_right n _)
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
rw [if_neg h.not_lt, max_eq_left h, add_lt_add_iff_left, add_assoc, add_lt_add_iff_left]
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ n < m + 1 ^ 2
[PROOFSTEP]
exact lt_succ_of_le h
[GOAL]
m n : ℕ
⊢ max m n ^ 2 + min m n ≤ pair m n
[PROOFSTEP]
rw [pair]
[GOAL]
m n : ℕ
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
[PROOFSTEP]
cases' lt_or_le m n with h h
[GOAL]
case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
case inr m n : ℕ h : n ≤ m ⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
[PROOFSTEP]
rw [if_pos h, max_eq_right h.le, min_eq_left h.le, sq]
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
[PROOFSTEP]
rw [if_neg h.not_lt, max_eq_left h, min_eq_right h, sq, add_assoc, add_le_add_iff_left]
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n
[PROOFSTEP]
exact le_add_self
[GOAL]
m n : ℕ
⊢ m + n ≤ max m n ^ 2 + min m n
[PROOFSTEP]
rw [sq, ← min_add_max, add_comm, add_le_add_iff_right]
[GOAL]
m n : ℕ
⊢ max m n ≤ max m n * max m n
[PROOFSTEP]
exact le_mul_self _
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ (n : ℕ), f (unpair n).fst (unpair n).snd = ⨆ (i : ℕ) (j : ℕ), f i j
[PROOFSTEP]
rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]
[GOAL]
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ (n : ℕ), s (unpair n).fst ×ˢ t (unpair n).snd = (⋃ (n : ℕ), s n) ×ˢ ⋃ (n : ℕ), t n
[PROOFSTEP]
rw [← Set.iUnion_prod]
[GOAL]
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ (n : ℕ), s (unpair n).fst ×ˢ t (unpair n).snd = ⋃ (x : ℕ × ℕ), s x.fst ×ˢ t x.snd
[PROOFSTEP]
exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)


[GOAL]
p✝ p : ℕ → Prop
n : ℕ
⊢ ℕ
[PROOFSTEP]
classical exact
  if h : Set.Finite (setOf p) then (h.toFinset.sort (· ≤ ·)).getD n 0
  else @Nat.Subtype.orderIsoOfNat (setOf p) (Set.Infinite.to_subtype h) n
[GOAL]
p✝ p : ℕ → Prop
n : ℕ
⊢ ℕ
[PROOFSTEP]
exact
  if h : Set.Finite (setOf p) then (h.toFinset.sort (· ≤ ·)).getD n 0
  else @Nat.Subtype.orderIsoOfNat (setOf p) (Set.Infinite.to_subtype h) n
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : card (Set.Finite.toFinset hf) ≤ n
⊢ nth p n = 0
[PROOFSTEP]
rw [nth, dif_pos hf, List.getD_eq_default]
[GOAL]
case hn
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : card (Set.Finite.toFinset hf) ≤ n
⊢ List.length (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)) ≤ n
[PROOFSTEP]
rwa [Finset.length_sort]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
⊢ nth p n =
    ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf)))
      { val := n, isLt := hn }
[PROOFSTEP]
rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_get]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
⊢ List.get (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)) { val := n, isLt := ?hn } =
    List.nthLe (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)) ↑{ val := n, isLt := hn }
      (_ : ↑{ val := n, isLt := hn } < List.length (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)))
case hn
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
⊢ n < List.length (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ StrictMonoOn (nth p) (Set.Iio (card (Set.Finite.toFinset hf)))
[PROOFSTEP]
rintro m (hm : m < _) n (hn : n < _) h
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
m : ℕ
hm : m < card (Set.Finite.toFinset hf)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : m < n
⊢ nth p m < nth p n
[PROOFSTEP]
simp only [nth_eq_orderEmbOfFin, *]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
m : ℕ
hm : m < card (Set.Finite.toFinset hf)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : m < n
⊢ ↑(orderEmbOfFin (Set.Finite.toFinset (_ : Set.Finite (setOf p)))
          (_ :
            card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) =
              card (Set.Finite.toFinset (_ : Set.Finite (setOf p)))))
      { val := m, isLt := (_ : m < card (Set.Finite.toFinset hf)) } <
    ↑(orderEmbOfFin (Set.Finite.toFinset (_ : Set.Finite (setOf p)))
          (_ :
            card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) =
              card (Set.Finite.toFinset (_ : Set.Finite (setOf p)))))
      { val := n, isLt := (_ : n < card (Set.Finite.toFinset hf)) }
[PROOFSTEP]
exact OrderEmbedding.strictMono _ h
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ Set.range (nth p) = insert 0 (setOf p)
[PROOFSTEP]
simpa only [← nth_eq_getD_sort hf, mem_sort, Set.Finite.mem_toFinset] using
  Set.range_list_getD (hf.toFinset.sort (· ≤ ·)) 0
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ nth p '' Set.Iio (card (Set.Finite.toFinset hf)) =
    Set.range
      ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf)))
[PROOFSTEP]
ext x
[GOAL]
case h
p : ℕ → Prop
hf : Set.Finite (setOf p)
x : ℕ
⊢ x ∈ nth p '' Set.Iio (card (Set.Finite.toFinset hf)) ↔
    x ∈
      Set.range
        ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf)))
[PROOFSTEP]
simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf, Set.mem_Iio, exists_prop]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ Set.range
      ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf))) =
    setOf p
[PROOFSTEP]
rw [range_orderEmbOfFin, Set.Finite.coe_toFinset]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
x : ℕ
h : p x
⊢ ∃ n, n < card (Set.Finite.toFinset hf) ∧ nth p n = x
[PROOFSTEP]
rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
n : ℕ
⊢ nth p n = ↑(↑(Subtype.orderIsoOfNat (setOf p)) n)
[PROOFSTEP]
rw [nth, dif_neg hf]
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ StrictMono (nth p)
[PROOFSTEP]
rw [nth_eq_orderIsoOfNat hf]
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ StrictMono (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p)))
[PROOFSTEP]
exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ Set.range (nth p) = setOf p
[PROOFSTEP]
rw [nth_eq_orderIsoOfNat hf]
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ Set.range (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p))) = setOf p
[PROOFSTEP]
haveI := hf.to_subtype
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
this : Infinite ↑(setOf p)
⊢ Set.range (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p))) = setOf p
[PROOFSTEP]
classical exact Nat.Subtype.coe_comp_ofNat_range
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
this : Infinite ↑(setOf p)
⊢ Set.range (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p))) = setOf p
[PROOFSTEP]
exact Nat.Subtype.coe_comp_ofNat_range
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
refine' (setOf p).finite_or_infinite.elim (fun hf => _) fun hf => _
[GOAL]
case refine'_1
p : ℕ → Prop
x : ℕ
h : p x
hf : Set.Finite (setOf p)
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
[GOAL]
case refine'_1.intro.intro
p : ℕ → Prop
x : ℕ
h : p x
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
hx : nth p n = x
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
exact ⟨n, fun _ => hn, hx⟩
[GOAL]
case refine'_2
p : ℕ → Prop
x : ℕ
h : p x
hf : Set.Infinite (setOf p)
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h
[GOAL]
case refine'_2
p : ℕ → Prop
x : ℕ
h : x ∈ Set.range (nth p)
hf : Set.Infinite (setOf p)
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
rcases h with ⟨n, hx⟩
[GOAL]
case refine'_2.intro
p : ℕ → Prop
x : ℕ
hf : Set.Infinite (setOf p)
n : ℕ
hx : nth p n = x
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
exact ⟨n, fun hf' => absurd hf' hf, hx⟩
[GOAL]
p✝ p : ℕ → Prop
n : ℕ
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
by_cases hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card
[GOAL]
case pos
p✝ p : ℕ → Prop
n : ℕ
hn : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
exact (isLeast_nth hn).csInf_eq.symm
[GOAL]
case neg
p✝ p : ℕ → Prop
n : ℕ
hn : ¬∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
push_neg at hn
[GOAL]
case neg
p✝ p : ℕ → Prop
n : ℕ
hn : ∃ h, card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
rcases hn with ⟨hf, hn⟩
[GOAL]
case neg.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
rw [nth_of_card_le _ hn]
[GOAL]
case neg.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
⊢ 0 = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
refine' ((congr_arg sInf <| Set.eq_empty_of_forall_not_mem fun k hk => _).trans sInf_empty).symm
[GOAL]
case neg.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
k : ℕ
hk : k ∈ {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
⊢ False
[PROOFSTEP]
rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
[GOAL]
case neg.intro.intro.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)
hk : nth p k ∈ {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
⊢ False
[PROOFSTEP]
exact (hk.2 _ ((hlt hf).trans_le hn)).false
[GOAL]
p : ℕ → Prop
⊢ nth p 0 = sInf (setOf p)
[PROOFSTEP]
rw [nth_eq_sInf]
[GOAL]
p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ (k : ℕ), k < 0 → nth p k < x} = sInf (setOf p)
[PROOFSTEP]
simp
[GOAL]
p : ℕ → Prop
h : p 0
⊢ nth p 0 = 0
[PROOFSTEP]
simp [nth_zero, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ nth p 0 = Nat.find h
[PROOFSTEP]
rw [nth_zero]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ sInf (setOf p) = Nat.find h
[PROOFSTEP]
convert Nat.sInf_def h
[GOAL]
p : ℕ → Prop
n : ℕ
⊢ nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ hf, card (Set.Finite.toFinset hf) ≤ n
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ p 0 ∧ n = 0 ∨ ∃ hf, card (Set.Finite.toFinset hf) ≤ n
[PROOFSTEP]
simp only [or_iff_not_imp_right, not_exists, not_le]
[GOAL]
case refine'_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ (∀ (x : Set.Finite (setOf p)), n < card (Set.Finite.toFinset x)) → p 0 ∧ n = 0
[PROOFSTEP]
exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩
[GOAL]
case refine'_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ hf, card (Set.Finite.toFinset hf) ≤ n) → nth p n = 0
[PROOFSTEP]
rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
[GOAL]
case refine'_2.inl.intro
p : ℕ → Prop
h₀ : p 0
⊢ nth p 0 = 0
case refine'_2.inr.intro
p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hle : card (Set.Finite.toFinset hf) ≤ n
⊢ nth p n = 0
[PROOFSTEP]
exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]
[GOAL]
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : nth p a = 0
⊢ nth p b = 0
[PROOFSTEP]
simp only [nth_eq_zero, h₀, false_and_iff, false_or_iff] at ha ⊢
[GOAL]
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ hf, card (Set.Finite.toFinset hf) ≤ a
⊢ ∃ hf, card (Set.Finite.toFinset hf) ≤ b
[PROOFSTEP]
exact ha.imp fun hf hle => hle.trans hab
[GOAL]
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
⊢ a ≤ nth p k
[PROOFSTEP]
cases' (setOf p).finite_or_infinite with hf hf
[GOAL]
case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : Set.Finite (setOf p)
⊢ a ≤ nth p k
[PROOFSTEP]
rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
[GOAL]
case inl.intro.intro
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k
[PROOFSTEP]
cases' lt_or_le (k + 1) hf.toFinset.card with hk hk
[GOAL]
case inl.intro.intro.inl
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < card (Set.Finite.toFinset hf)
⊢ nth p n ≤ nth p k
[PROOFSTEP]
rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, lt_succ_iff, ←
  (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h
[GOAL]
case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : card (Set.Finite.toFinset hf) ≤ k + 1
⊢ nth p n ≤ nth p k
[PROOFSTEP]
rw [nth_of_card_le _ hk] at h
[GOAL]
case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < 0
ha : p (nth p n)
hk : card (Set.Finite.toFinset hf) ≤ k + 1
⊢ nth p n ≤ nth p k
[PROOFSTEP]
exact absurd h (zero_le _).not_lt
[GOAL]
case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : Set.Infinite (setOf p)
⊢ a ≤ nth p k
[PROOFSTEP]
rcases subset_range_nth ha with ⟨n, rfl⟩
[GOAL]
case inr.intro
p : ℕ → Prop
k : ℕ
hf : Set.Infinite (setOf p)
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k
[PROOFSTEP]
rwa [nth_lt_nth hf, lt_succ_iff, ← nth_le_nth hf] at h
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p (nth p 0) = 0
[PROOFSTEP]
rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : ℕ), x ∈ range (sInf (setOf p)) → ¬p x
[PROOFSTEP]
exact fun n h₁ h₂ => (mem_range.1 h₁).not_le (Nat.sInf_le h₂)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
⊢ filter p (range (nth p (k + 1))) ⊆ insert (nth p k) (filter p (range (nth p k)))
[PROOFSTEP]
intro a ha
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a ∈ filter p (range (nth p (k + 1)))
⊢ a ∈ insert (nth p k) (filter p (range (nth p k)))
[PROOFSTEP]
simp only [mem_insert, mem_filter, mem_range] at ha ⊢
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a < nth p (k + 1) ∧ p a
⊢ a = nth p k ∨ a < nth p k ∧ p a
[PROOFSTEP]
exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
⊢ filter p (range (nth p (k + 1))) = insert (nth p k) (filter p (range (nth p k)))
[PROOFSTEP]
refine' (filter_range_nth_subset_insert p k).antisymm fun a ha => _
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
a : ℕ
ha : a ∈ insert (nth p k) (filter p (range (nth p k)))
⊢ a ∈ filter p (range (nth p (k + 1)))
[PROOFSTEP]
simp only [mem_insert, mem_filter, mem_range] at ha ⊢
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
⊢ a < nth p (k + 1) ∧ p a
[PROOFSTEP]
have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
this : nth p k < nth p (k + 1)
⊢ a < nth p (k + 1) ∧ p a
[PROOFSTEP]
rcases ha with (rfl | ⟨hlt, hpa⟩)
[GOAL]
case inl
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)
[PROOFSTEP]
exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩
[GOAL]
case inr.intro
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a
[PROOFSTEP]
exact ⟨hlt.trans this, hpa⟩
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ count p (nth p n) = n
[PROOFSTEP]
induction' n with k ihk
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn✝ : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
hn : ∀ (hf : Set.Finite (setOf p)), zero < card (Set.Finite.toFinset hf)
⊢ count p (nth p zero) = zero
[PROOFSTEP]
exact count_nth_zero _
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn✝ : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
k : ℕ
ihk : (∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)) → count p (nth p k) = k
hn : ∀ (hf : Set.Finite (setOf p)), succ k < card (Set.Finite.toFinset hf)
⊢ count p (nth p (succ k)) = succ k
[PROOFSTEP]
rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_not_mem, ← count_eq_card_filter_range,
  ihk fun hf => lt_of_succ_lt (hn hf)]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn✝ : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
k : ℕ
ihk : (∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)) → count p (nth p k) = k
hn : ∀ (hf : Set.Finite (setOf p)), succ k < card (Set.Finite.toFinset hf)
⊢ ¬nth p k ∈ filter p (range (nth p k))
[PROOFSTEP]
simp
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ count p (nth p n + 1) = n + 1
[PROOFSTEP]
rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n
[PROOFSTEP]
refine' (count_monotone p).reflect_lt _
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ count p (nth p k) < count p n
[PROOFSTEP]
rwa [count_nth]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ ∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)
[PROOFSTEP]
exact fun hf => h.trans_le (count_le_card hf n)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ nth p (count p n) = sInf {i | p i ∧ n ≤ i}
[PROOFSTEP]
refine' (nth_eq_sInf _ _).trans (congr_arg sInf _)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ {x | p x ∧ ∀ (k : ℕ), k < count p n → nth p k < x} = {i | p i ∧ n ≤ i}
[PROOFSTEP]
refine' Set.ext fun a => and_congr_right fun hpa => _
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ (k : ℕ), k < count p n → nth p k < a) ↔ n ≤ a
[PROOFSTEP]
refine' ⟨fun h => not_lt.1 fun ha => _, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ (k : ℕ), k < count p n → nth p k < a
ha : a < n
⊢ False
[PROOFSTEP]
have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ (k : ℕ), k < count p n → nth p k < a
ha : a < n
hn : nth p (count p a) < a
⊢ False
[PROOFSTEP]
rwa [nth_count hpa, lt_self_iff_false] at hn


[GOAL]
a : ℕ
⊢ Periodic (gcd a) a
[PROOFSTEP]
simp only [forall_const, gcd_add_self_right, eq_self_iff_true, Periodic]
[GOAL]
a : ℕ
⊢ Periodic (coprime a) a
[PROOFSTEP]
simp only [coprime_add_self_right, forall_const, iff_self_iff, eq_iff_iff, Periodic]
[GOAL]
a : ℕ
⊢ Periodic (fun n => n % a) a
[PROOFSTEP]
simp only [forall_const, eq_self_iff_true, add_mod_right, Periodic]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
⊢ f (n % a) = f n
[PROOFSTEP]
conv_rhs => rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n
[PROOFSTEP]
rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n
[PROOFSTEP]
rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n
[PROOFSTEP]
rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ ↑card (filter p (Ico n (n + a))) = count p a
[PROOFSTEP]
rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ← multiset_Ico_map_mod n, ←
  map_count_True_eq_filter_card, ← map_count_True_eq_filter_card, map_map]
[GOAL]
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) = Multiset.count True (map (p ∘ fun x => x % a) (Ico n (n + a)))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = p ∘ fun x => x % a
[PROOFSTEP]
funext n
[GOAL]
case e_a.e_f.h
n✝ a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
n : ℕ
⊢ p n = (p ∘ fun x => x % a) n
[PROOFSTEP]
exact (Function.Periodic.map_mod_nat pp n).symm


[GOAL]
p : ℕ
h : 1 < p
⊢ 0 < p ^ 0
[PROOFSTEP]
simp [zero_lt_one]
[GOAL]
n : ℕ
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n m : ℕ
h : 0 < m
⊢ 1 ≤ m ^ n
[PROOFSTEP]
rw [← one_pow n]
[GOAL]
n m : ℕ
h : 0 < m
⊢ 1 ^ n ≤ m ^ n
[PROOFSTEP]
exact Nat.pow_le_pow_of_le_left h n
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
n m : ℕ
h₀ : 0 < n
h₁ : 1 < m
⊢ 1 < m ^ n
[PROOFSTEP]
rw [← one_pow n]
[GOAL]
n m : ℕ
h₀ : 0 < n
h₁ : 1 < m
⊢ 1 ^ n < m ^ n
[PROOFSTEP]
exact pow_lt_pow_of_lt_left h₁ h₀
[GOAL]
k n : ℕ
h : 0 ≠ k
⊢ 1 < n ^ k ↔ 1 < n
[PROOFSTEP]
rcases n with (rfl | n)
[GOAL]
case zero
k : ℕ
h : 0 ≠ k
⊢ 1 < zero ^ k ↔ 1 < zero
[PROOFSTEP]
cases k
[GOAL]
case zero.zero
h : 0 ≠ zero
⊢ 1 < zero ^ zero ↔ 1 < zero
[PROOFSTEP]
simp [zero_pow_eq]
[GOAL]
case zero.succ
n✝ : ℕ
h : 0 ≠ succ n✝
⊢ 1 < zero ^ succ n✝ ↔ 1 < zero
[PROOFSTEP]
simp [zero_pow_eq]
[GOAL]
case succ
k : ℕ
h : 0 ≠ k
n : ℕ
⊢ 1 < succ n ^ k ↔ 1 < succ n
[PROOFSTEP]
rcases n with (rfl | n)
[GOAL]
case succ.zero
k : ℕ
h : 0 ≠ k
⊢ 1 < succ zero ^ k ↔ 1 < succ zero
[PROOFSTEP]
rw [← Nat.one_eq_succ_zero, one_pow]
[GOAL]
case succ.succ
k : ℕ
h : 0 ≠ k
n : ℕ
⊢ 1 < succ (succ n) ^ k ↔ 1 < succ (succ n)
[PROOFSTEP]
refine' ⟨fun _ => one_lt_succ_succ n, fun _ => _⟩
[GOAL]
case succ.succ
k : ℕ
h : 0 ≠ k
n : ℕ
x✝ : 1 < succ (succ n)
⊢ 1 < succ (succ n) ^ k
[PROOFSTEP]
induction' k with k hk
[GOAL]
case succ.succ.zero
k : ℕ
h✝ : 0 ≠ k
n : ℕ
x✝ : 1 < succ (succ n)
h : 0 ≠ zero
⊢ 1 < succ (succ n) ^ zero
[PROOFSTEP]
exact absurd rfl h
[GOAL]
case succ.succ.succ
k✝ : ℕ
h✝ : 0 ≠ k✝
n : ℕ
x✝ : 1 < succ (succ n)
k : ℕ
hk : 0 ≠ k → 1 < succ (succ n) ^ k
h : 0 ≠ succ k
⊢ 1 < succ (succ n) ^ succ k
[PROOFSTEP]
rcases k with (rfl | k)
[GOAL]
case succ.succ.succ.zero
k : ℕ
h✝ : 0 ≠ k
n : ℕ
x✝ : 1 < succ (succ n)
hk : 0 ≠ zero → 1 < succ (succ n) ^ zero
h : 0 ≠ succ zero
⊢ 1 < succ (succ n) ^ succ zero
[PROOFSTEP]
simp [← Nat.one_eq_succ_zero]
[GOAL]
case succ.succ.succ.succ
k✝ : ℕ
h✝ : 0 ≠ k✝
n : ℕ
x✝ : 1 < succ (succ n)
k : ℕ
hk : 0 ≠ succ k → 1 < succ (succ n) ^ succ k
h : 0 ≠ succ (succ k)
⊢ 1 < succ (succ n) ^ succ (succ k)
[PROOFSTEP]
rw [pow_succ']
[GOAL]
case succ.succ.succ.succ
k✝ : ℕ
h✝ : 0 ≠ k✝
n : ℕ
x✝ : 1 < succ (succ n)
k : ℕ
hk : 0 ≠ succ k → 1 < succ (succ n) ^ succ k
h : 0 ≠ succ (succ k)
⊢ 1 < succ (succ n) * succ (succ n) ^ (k + 1)
[PROOFSTEP]
exact one_lt_mul (one_lt_succ_succ _).le (hk (succ_ne_zero k).symm)
[GOAL]
n : ℕ
h₀ : 0 < n
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n a q : ℕ
a0 : 0 < a
q1 : 1 < q
⊢ n * q < a * q ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)]
[GOAL]
n a q : ℕ
a0 : 0 < a
q1 : 1 < q
⊢ n < a * q ^ n
[PROOFSTEP]
exact lt_mul_of_one_le_of_lt (Nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n)
[GOAL]
a b : ℕ
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a b : ℕ
⊢ a * a - b * b = (a + b) * (a - b)
[PROOFSTEP]
exact Nat.mul_self_sub_mul_self_eq a b
[GOAL]
a b n : ℕ
⊢ a ^ b % n = (a % n) ^ b % n
[PROOFSTEP]
induction' b with b ih
[GOAL]
case zero
a n : ℕ
⊢ a ^ zero % n = (a % n) ^ zero % n
case succ a n b : ℕ ih : a ^ b % n = (a % n) ^ b % n ⊢ a ^ succ b % n = (a % n) ^ succ b % n
[PROOFSTEP]
rfl
[GOAL]
case succ
a n b : ℕ
ih : a ^ b % n = (a % n) ^ b % n
⊢ a ^ succ b % n = (a % n) ^ succ b % n
[PROOFSTEP]
simp [pow_succ, Nat.mul_mod, ih]
[GOAL]
b w m : ℕ
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
by_cases b_h : b = 0
[GOAL]
case pos
b w m : ℕ
b_h : b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
simp [b_h, pow_succ]
[GOAL]
case neg
b w m : ℕ
b_h : ¬b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
have b_pos := Nat.pos_of_ne_zero b_h
[GOAL]
case neg
b w m : ℕ
b_h : ¬b = 0
b_pos : 0 < b
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
induction m using Nat.strong_induction_on with
| h p IH =>
  cases' lt_or_ge p (b ^ succ w) with h₁ h₁
  ·
    -- base case: p < b^succ w
    have h₂ : p / b < b ^ w := by
      rw [div_lt_iff_lt_mul b_pos]
      simpa [pow_succ] using h₁
    rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
    simp [div_add_mod]
  ·
    -- step: p ≥ b^succ w
            -- Generate condition for induction hypothesis
    have h₂ : p - b ^ succ w < p :=
      tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
        (pow_pos b_pos _)
          -- Apply induction
    rw [mod_eq_sub_mod h₁, IH _ h₂]
      -- Normalize goal and h1
    simp only [pow_succ']
    simp only [GE.ge, pow_succ'] at h₁
    rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
      -- Cancel subtraction inside mod b^w
    have p_b_ge : b ^ w ≤ p / b := by
      rw [le_div_iff_mul_le b_pos, mul_comm]
      exact h₁
    rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
case neg
b w m : ℕ
b_h : ¬b = 0
b_pos : 0 < b
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
induction m using Nat.strong_induction_on with
| h p IH =>
  cases' lt_or_ge p (b ^ succ w) with h₁ h₁
  ·
    -- base case: p < b^succ w
    have h₂ : p / b < b ^ w := by
      rw [div_lt_iff_lt_mul b_pos]
      simpa [pow_succ] using h₁
    rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
    simp [div_add_mod]
  ·
    -- step: p ≥ b^succ w
            -- Generate condition for induction hypothesis
    have h₂ : p - b ^ succ w < p :=
      tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
        (pow_pos b_pos _)
          -- Apply induction
    rw [mod_eq_sub_mod h₁, IH _ h₂]
      -- Normalize goal and h1
    simp only [pow_succ']
    simp only [GE.ge, pow_succ'] at h₁
    rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
      -- Cancel subtraction inside mod b^w
    have p_b_ge : b ^ w ≤ p / b := by
      rw [le_div_iff_mul_le b_pos, mul_comm]
      exact h₁
    rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
case neg.h
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]

| h p IH =>
  cases' lt_or_ge p (b ^ succ w) with h₁ h₁
  ·
    -- base case: p < b^succ w
    have h₂ : p / b < b ^ w := by
      rw [div_lt_iff_lt_mul b_pos]
      simpa [pow_succ] using h₁
    rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
    simp [div_add_mod]
  ·
    -- step: p ≥ b^succ w
            -- Generate condition for induction hypothesis
    have h₂ : p - b ^ succ w < p :=
      tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
        (pow_pos b_pos _)
          -- Apply induction
    rw [mod_eq_sub_mod h₁, IH _ h₂]
      -- Normalize goal and h1
    simp only [pow_succ']
    simp only [GE.ge, pow_succ'] at h₁
    rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
      -- Cancel subtraction inside mod b^w
    have p_b_ge : b ^ w ≤ p / b := by
      rw [le_div_iff_mul_le b_pos, mul_comm]
      exact h₁
    rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
case neg.h
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
cases' lt_or_ge p (b ^ succ w) with h₁ h₁
[GOAL]
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
have h₂ : p / b < b ^ w := by
  rw [div_lt_iff_lt_mul b_pos]
  simpa [pow_succ] using h₁
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p / b < b ^ w
[PROOFSTEP]
rw [div_lt_iff_lt_mul b_pos]
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p < b ^ w * b
[PROOFSTEP]
simpa [pow_succ] using h₁
[GOAL]
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
[GOAL]
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p = b * (p / b) + p % b
[PROOFSTEP]
simp [div_add_mod]
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
have h₂ : p - b ^ succ w < p :=
  tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
    (pow_pos b_pos _)
      -- Apply induction
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [mod_eq_sub_mod h₁, IH _ h₂]
  -- Normalize goal and h1
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b ^ succ w) / b % b ^ w) + (p - b ^ succ w) % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
simp only [pow_succ']
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
simp only [GE.ge, pow_succ'] at h₁
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
  -- Cancel subtraction inside mod b^w
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
have p_b_ge : b ^ w ≤ p / b := by
  rw [le_div_iff_mul_le b_pos, mul_comm]
  exact h₁
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b ^ w ≤ p / b
[PROOFSTEP]
rw [le_div_iff_mul_le b_pos, mul_comm]
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * b ^ w ≤ p
[PROOFSTEP]
exact h₁
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
p_b_ge : b ^ w ≤ p / b
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l ↔ (x + 1) ^ k ≤ (x + 1) ^ l
[PROOFSTEP]
constructor
[GOAL]
case mp
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l → (x + 1) ^ k ≤ (x + 1) ^ l
[PROOFSTEP]
intro a
[GOAL]
case mp
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ∣ (x + 1) ^ l
⊢ (x + 1) ^ k ≤ (x + 1) ^ l
[PROOFSTEP]
exact le_of_dvd (pow_pos (succ_pos x) l) a
[GOAL]
case mpr
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ≤ (x + 1) ^ l → (x + 1) ^ k ∣ (x + 1) ^ l
[PROOFSTEP]
intro a
[GOAL]
case mpr
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ≤ (x + 1) ^ l
⊢ (x + 1) ^ k ∣ (x + 1) ^ l
[PROOFSTEP]
cases' x with x
[GOAL]
case mpr.zero
k l : ℕ
w : 0 < zero + 1
a : (zero + 1) ^ k ≤ (zero + 1) ^ l
⊢ (zero + 1) ^ k ∣ (zero + 1) ^ l
[PROOFSTEP]
simp
[GOAL]
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
[PROOFSTEP]
have le := (pow_le_iff_le_right (Nat.le_add_left _ _)).mp a
[GOAL]
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
[PROOFSTEP]
use(x + 2) ^ (l - k)
[GOAL]
case h
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ l = (succ x + 1) ^ k * (x + 2) ^ (l - k)
[PROOFSTEP]
rw [← pow_add, add_comm k, tsub_add_cancel_of_le le]
[GOAL]
x k l : ℕ
w : 1 < x
⊢ x ^ k ∣ x ^ l ↔ k ≤ l
[PROOFSTEP]
rw [pow_dvd_pow_iff_pow_le_pow (lt_of_succ_lt w), pow_le_iff_le_right w]
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
⊢ succ p * succ p ^ k ∣ succ p * 1
[PROOFSTEP]
simpa [pow_succ'] using h
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝¹ : succ p * succ p ^ k ∣ succ p * 1
this✝ : succ p ^ k ∣ 1
he : succ p ^ k = 1
this : k < succ p ^ k
⊢ k < 1
[PROOFSTEP]
rwa [he] at this
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝³ : succ p * succ p ^ k ∣ succ p * 1
this✝² : succ p ^ k ∣ 1
he : succ p ^ k = 1
this✝¹ : k < succ p ^ k
this✝ : k < 1
this : k = 0
⊢ 1 < 1
[PROOFSTEP]
rwa [this] at hk
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝⁴ : succ p * succ p ^ k ∣ succ p * 1
this✝³ : succ p ^ k ∣ 1
he : succ p ^ k = 1
this✝² : k < succ p ^ k
this✝¹ : k < 1
this✝ : k = 0
this : 1 < 1
⊢ ¬1 < 1
[PROOFSTEP]
decide
[GOAL]
p k m : ℕ
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ∣ m
[PROOFSTEP]
rw [← pow_one p]
[GOAL]
p k m : ℕ
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ^ 1 ∣ m
[PROOFSTEP]
exact pow_dvd_of_le_of_pow_dvd hk hpk
[GOAL]
x m n : ℕ
h : n ≤ m
hx : 0 < x
⊢ x ^ m / x ^ n = x ^ (m - n)
[PROOFSTEP]
rw [Nat.div_eq_iff_eq_mul_left (pow_pos hx n) (pow_dvd_pow _ h), pow_sub_mul_pow _ h]
[GOAL]
p i n : ℕ
hn : n ≠ 0
hp : 2 ≤ p
h : p ^ i ∣ n
⊢ i < n
[PROOFSTEP]
rw [← pow_lt_iff_lt_right hp]
[GOAL]
p i n : ℕ
hn : n ≠ 0
hp : 2 ≤ p
h : p ^ i ∣ n
⊢ p ^ i < p ^ n
[PROOFSTEP]
exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n)