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]
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]
obtain ⟨⟨hpq, -⟩, hqr⟩ : (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]
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]
simpa using hs
no goals
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]
exact admissible_of_one_lt_sumInv_aux' hpq hqr H