pqr : Multiset ℕ+
⊢ (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr → 1 < sumInv pqr
pqr : Multiset ℕ+
⊢ Admissible pqr → 1 < sumInv pqr
rw [Admissible]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr

case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr

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
pqr : Multiset ℕ+
⊢ (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr → 1 < sumInv pqr
rintro (⟨p', q', H⟩ | ⟨n, H⟩ | H | H | H)
no goals
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
all_goals
  rw [← H, E', sumInv_pqr]
  conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr
rw [← H, A', sumInv_pqr, add_assoc]
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹ + (↑↑q')⁻¹
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)
simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
no goals
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹ + (↑↑q')⁻¹
apply add_pos <;> simp only [PNat.pos, Nat.cast_pos, inv_pos]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr
rw [← H, D', sumInv_pqr]
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑(1 + 1))⁻¹ + (↑(1 + 1))⁻¹ + (↑↑n)⁻¹
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
no goals
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑(1 + 1))⁻¹ + (↑(1 + 1))⁻¹ + (↑↑n)⁻¹
norm_num
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr
rw [← H, E', sumInv_pqr]
no goals
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]