r : ℕ+
H : 1 < sumInv {2, 3, r}
h6 : 0 < 6
⊢ r < 6
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ r < 6
have h6 : (0 : ℚ) < 6 := by norm_num
r : ℕ+
h6 : 0 < 6
H : ¬r < 6
⊢ sumInv {2, 3, r} ≤ 1
r : ℕ+
H : 1 < sumInv {2, 3, r}
h6 : 0 < 6
⊢ r < 6
contrapose! H
r : ℕ+
h6 : 0 < 6
H : ¬r < 6
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
r : ℕ+
h6 : 0 < 6
H : ¬r < 6
⊢ sumInv {2, 3, r} ≤ 1
rw [sumInv_pqr]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
r : ℕ+
h6 : 0 < 6
H : ¬r < 6
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
simp at H
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
have hr: (r : ℚ)⁻¹ ≤ 6⁻¹ := by
  rw [inv_le_inv _ h6]
  assumption_mod_cast
  norm_num
no goals
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
calc
  (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
  _ = 1 := by norm_num
no goals
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ 0 < 6
norm_num
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 6 ≤ ↑↑r

r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑r)⁻¹ ≤ 6⁻¹
rw [inv_le_inv _ h6]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 6 ≤ ↑↑r

r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r
assumption_mod_cast
no goals
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r
norm_num
no goals
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ 2⁻¹ + 3⁻¹ + 6⁻¹ = 1
norm_num