[GOAL]
p q r : ℕ+
⊢ sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹
[PROOFSTEP]
simp only [sumInv, add_zero, insert_eq_cons, add_assoc, map_cons, sum_cons, map_singleton, sum_singleton]
[GOAL]
pqr : Multiset ℕ+
⊢ Admissible pqr → 1 < sumInv pqr
[PROOFSTEP]
rw [Admissible]
[GOAL]
pqr : Multiset ℕ+
⊢ (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr → 1 < sumInv pqr
[PROOFSTEP]
rintro (⟨p', q', H⟩ | ⟨n, H⟩ | H | H | H)
[GOAL]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, A', sumInv_pqr, add_assoc]
[GOAL]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)
[PROOFSTEP]
simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
[GOAL]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹ + (↑↑q')⁻¹
[PROOFSTEP]
apply add_pos
[GOAL]
case inl.intro.intro.ha
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹
[PROOFSTEP]
simp only [PNat.pos, Nat.cast_pos, inv_pos]
[GOAL]
case inl.intro.intro.hb
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑q')⁻¹
[PROOFSTEP]
simp only [PNat.pos, Nat.cast_pos, inv_pos]
[GOAL]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, D', sumInv_pqr]
[GOAL]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
| (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
| (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
| (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑(1 + 1))⁻¹ + (↑(1 + 1))⁻¹ + (↑↑n)⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr
case inr.inr.inr.inr pqr : Multiset ℕ+ H : E' 5 = pqr ⊢ 1 < sumInv pqr
[PROOFSTEP]
all_goals
  rw [← H, E', sumInv_pqr]
  conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, E', sumInv_pqr]
[GOAL]
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 3 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 3 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 3 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, E', sumInv_pqr]
[GOAL]
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 4 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 4 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 4 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr
[PROOFSTEP]
rw [← H, E', sumInv_pqr]
[GOAL]
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 5 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 5 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
pqr : Multiset ℕ+
H : E' 5 = pqr
| (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
[PROOFSTEP]
simp only [OfNat.ofNat, PNat.mk_coe]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ p < 3
[PROOFSTEP]
have h3 : (0 : ℚ) < 3 := by norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ 0 < 3
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
h3 : 0 < 3
⊢ p < 3
[PROOFSTEP]
contrapose! H
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
⊢ sumInv {p, q, r} ≤ 1
[PROOFSTEP]
rw [sumInv_pqr]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have h3q := H.trans hpq
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have h3r := h3q.trans hqr
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := by
  rw [inv_le_inv _ h3]
  assumption_mod_cast
  norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ (↑↑p)⁻¹ ≤ 3⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h3]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ 3 ≤ ↑↑p
p q r : ℕ+ hpq : p ≤ q hqr : q ≤ r h3 : 0 < 3 H : 3 ≤ p h3q : 3 ≤ q h3r : 3 ≤ r ⊢ 0 < ↑↑p
[PROOFSTEP]
assumption_mod_cast
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ 0 < ↑↑p
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := by
  rw [inv_le_inv _ h3]
  assumption_mod_cast
  norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ (↑↑q)⁻¹ ≤ 3⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h3]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑q
p q r : ℕ+ hpq : p ≤ q hqr : q ≤ r h3 : 0 < 3 H : 3 ≤ p h3q : 3 ≤ q h3r : 3 ≤ r hp : (↑↑p)⁻¹ ≤ 3⁻¹ ⊢ 0 < ↑↑q
[PROOFSTEP]
assumption_mod_cast
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑q
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := by
  rw [inv_le_inv _ h3]
  assumption_mod_cast
  norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ (↑↑r)⁻¹ ≤ 3⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h3]
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑r
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
[PROOFSTEP]
assumption_mod_cast
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < ↑↑r
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
hr : (↑↑r)⁻¹ ≤ 3⁻¹
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
calc
  (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
  _ = 1 := by norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
h3 : 0 < 3
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
hr : (↑↑r)⁻¹ ≤ 3⁻¹
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ q < 4
[PROOFSTEP]
have h4 : (0 : ℚ) < 4 := by norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
h4 : 0 < 4
⊢ q < 4
[PROOFSTEP]
contrapose! H
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ sumInv {2, q, r} ≤ 1
[PROOFSTEP]
rw [sumInv_pqr]
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have h4r := H.trans hqr
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hq : (q : ℚ)⁻¹ ≤ 4⁻¹ := by
  rw [inv_le_inv _ h4]
  assumption_mod_cast
  norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ (↑↑q)⁻¹ ≤ 4⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h4]
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 4 ≤ ↑↑q
q r : ℕ+ hqr : q ≤ r h4 : 0 < 4 H : 4 ≤ q h4r : 4 ≤ r ⊢ 0 < ↑↑q
[PROOFSTEP]
assumption_mod_cast
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 0 < ↑↑q
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hr : (r : ℚ)⁻¹ ≤ 4⁻¹ := by
  rw [inv_le_inv _ h4]
  assumption_mod_cast
  norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑r)⁻¹ ≤ 4⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h4]
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 4 ≤ ↑↑r
q r : ℕ+ hqr : q ≤ r h4 : 0 < 4 H : 4 ≤ q h4r : 4 ≤ r hq : (↑↑q)⁻¹ ≤ 4⁻¹ ⊢ 0 < ↑↑r
[PROOFSTEP]
assumption_mod_cast
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r
[PROOFSTEP]
norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
calc
  (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
  _ = 1 := by norm_num
[GOAL]
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ 2⁻¹ + 4⁻¹ + 4⁻¹ = 1
[PROOFSTEP]
norm_num
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ r < 6
[PROOFSTEP]
have h6 : (0 : ℚ) < 6 := by norm_num
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ 0 < 6
[PROOFSTEP]
norm_num
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
h6 : 0 < 6
⊢ r < 6
[PROOFSTEP]
contrapose! H
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ sumInv {2, 3, r} ≤ 1
[PROOFSTEP]
rw [sumInv_pqr]
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
have hr : (r : ℚ)⁻¹ ≤ 6⁻¹ := by
  rw [inv_le_inv _ h6]
  assumption_mod_cast
  norm_num
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ (↑↑r)⁻¹ ≤ 6⁻¹
[PROOFSTEP]
rw [inv_le_inv _ h6]
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 6 ≤ ↑↑r
r : ℕ+ h6 : 0 < 6 H : 6 ≤ r ⊢ 0 < ↑↑r
[PROOFSTEP]
assumption_mod_cast
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
⊢ 0 < ↑↑r
[PROOFSTEP]
norm_num
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
[PROOFSTEP]
calc
  (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
  _ = 1 := by norm_num
[GOAL]
r : ℕ+
h6 : 0 < 6
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ 2⁻¹ + 3⁻¹ + 6⁻¹ = 1
[PROOFSTEP]
norm_num
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ Admissible {p, q, r}
[PROOFSTEP]
have hp3 : p < 3 := lt_three hpq hqr H
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p < 3
⊢ Admissible {p, q, r}
[PROOFSTEP]
replace hp3 := Finset.mem_Iio.mpr hp3
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
⊢ Admissible {p, q, r}
[PROOFSTEP]
conv at hp3 => change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ Finset.Iio 3
[PROOFSTEP]
change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ Finset.Iio 3
[PROOFSTEP]
change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
| p ∈ Finset.Iio 3
[PROOFSTEP]
change p ∈ ({1, 2} : Multiset ℕ+)
[GOAL]
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ {1, 2}
⊢ Admissible {p, q, r}
[PROOFSTEP]
fin_cases hp3
[GOAL]
case head
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}
[PROOFSTEP]
exact admissible_A' q r
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}
[PROOFSTEP]
have hq4 : q < 4 := lt_four hqr H
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q < 4
⊢ Admissible {2, q, r}
[PROOFSTEP]
replace hq4 := Finset.mem_Ico.mpr ⟨hpq, hq4⟩
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}
[PROOFSTEP]
clear hpq
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}
[PROOFSTEP]
conv at hq4 => change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ Finset.Ico 2 4
[PROOFSTEP]
change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ Finset.Ico 2 4
[PROOFSTEP]
change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
| q ∈ Finset.Ico 2 4
[PROOFSTEP]
change q ∈ ({2, 3} : Multiset ℕ+)
[GOAL]
case tail.head
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ {2, 3}
⊢ Admissible {2, q, r}
[PROOFSTEP]
fin_cases hq4
[GOAL]
case tail.head.head
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}
[PROOFSTEP]
exact admissible_D' r
[GOAL]
case tail.head.tail.head
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}
[PROOFSTEP]
have hr6 : r < 6 := lt_six H
[GOAL]
case tail.head.tail.head
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r < 6
⊢ Admissible {2, 3, r}
[PROOFSTEP]
replace hr6 := Finset.mem_Ico.mpr ⟨hqr, hr6⟩
[GOAL]
case tail.head.tail.head
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}
[PROOFSTEP]
clear hqr
[GOAL]
case tail.head.tail.head
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}
[PROOFSTEP]
conv at hr6 => change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ Finset.Ico 3 6
[PROOFSTEP]
change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ Finset.Ico 3 6
[PROOFSTEP]
change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
| r ∈ Finset.Ico 3 6
[PROOFSTEP]
change r ∈ ({3, 4, 5} : Multiset ℕ+)
[GOAL]
case tail.head.tail.head
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ {3, 4, 5}
⊢ Admissible {2, 3, r}
[PROOFSTEP]
fin_cases hr6
[GOAL]
case tail.head.tail.head.head
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}
[PROOFSTEP]
exact admissible_E6
[GOAL]
case tail.head.tail.head.tail.head
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}
[PROOFSTEP]
exact admissible_E7
[GOAL]
case tail.head.tail.head.tail.tail.head
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}
[PROOFSTEP]
exact admissible_E8
[GOAL]
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
⊢ Admissible ↑[p, q, r]
[PROOFSTEP]
obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r
[GOAL]
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
⊢ (p ≤ q ∧ p ≤ r) ∧ q ≤ r
case intro.intro
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible ↑[p, q, r]
[PROOFSTEP]
simpa using hs
[GOAL]
case intro.intro
p q r : ℕ+
hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]
x✝ : List.length [p, q, r] = 3
H : 1 < sumInv ↑[p, q, r]
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible ↑[p, q, r]
[PROOFSTEP]
exact admissible_of_one_lt_sumInv_aux' hpq hqr H
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
⊢ Admissible {p, q, r}
[PROOFSTEP]
simp only [Admissible]
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
let S := sort ((· ≤ ·) : ℕ+ → ℕ+ → Prop) { p, q, r }
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
have hS : S.Sorted (· ≤ ·) := sort_sorted _ _
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
have hpqr : ({ p, q, r } : Multiset ℕ+) = S := (sort_eq LE.le { p, q, r }).symm
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
[PROOFSTEP]
rw [hpqr]
[GOAL]
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S
[PROOFSTEP]
rw [hpqr] at H 
[GOAL]
p q r : ℕ+
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S
[PROOFSTEP]
apply admissible_of_one_lt_sumInv_aux hS _ H
[GOAL]
p q r : ℕ+
S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x x_1 => x ≤ x_1) S
hpqr : {p, q, r} = ↑S
⊢ List.length S = 3
[PROOFSTEP]
simp only [ge_iff_le, insert_eq_cons, length_sort, card_cons, card_singleton]
