-- Mathlib/NumberTheory/ADEInequality.lean
theorem admissible_of_one_lt_sumInv_aux' {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r)
    (H : 1 < sumInv {p, q, r}) : Admissible {p, q, r}

Proof state:
case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
exact admissible_E8

Result:
no goals

Proof state:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}

Tactic:
clear hqr

Result:
case «1».«1»
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}

Proof state:
case «1».«0»
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}

Tactic:
exact admissible_D' r

Result:
no goals

Proof state:
case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q < 4
⊢ Admissible {2, q, r}

Tactic:
replace hq4 := Finset.mem_Ico.mpr ⟨hpq, hq4⟩

Result:
case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}

Proof state:
case «1».«1».«0»
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}

Tactic:
exact admissible_E6

Result:
no goals

Proof state:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ {1, 2}
⊢ Admissible {p, q, r}

Tactic:
fin_cases hp3

Result:
case «0»
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}

case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}

Proof state:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}

Tactic:
have hr6 : r < 6 := lt_six H

Result:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r < 6
⊢ Admissible {2, 3, r}

Proof state:
case «1».«1»
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}

Tactic:
conv at hr6 => change r ∈ ({3, 4, 5} : Multiset ℕ+)

Result:
case «1».«1»
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ {3, 4, 5}
⊢ Admissible {2, 3, r}

Proof state:
case «0»
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}

Tactic:
exact admissible_A' q r

Result:
no goals

Proof state:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r < 6
⊢ Admissible {2, 3, r}

Tactic:
replace hr6 := Finset.mem_Ico.mpr ⟨hqr, hr6⟩

Result:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}

Proof state:
case «1»
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}

Tactic:
conv at hq4 => change q ∈ ({2, 3} : Multiset ℕ+)

Result:
case «1»
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ {2, 3}
⊢ Admissible {2, q, r}

Proof state:
case «1»
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ {2, 3}
⊢ Admissible {2, q, r}

Tactic:
fin_cases hq4

Result:
case «1».«0»
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}

case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}

Proof state:
case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}

Tactic:
clear hpq

Result:
case «1»
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}

Proof state:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p < 3
⊢ Admissible {p, q, r}

Tactic:
replace hp3 := Finset.mem_Iio.mpr hp3

Result:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
⊢ Admissible {p, q, r}

Proof state:
case «1».«1»
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ {3, 4, 5}
⊢ Admissible {2, 3, r}

Tactic:
fin_cases hr6

Result:
case «1».«1».«0»
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}

case «1».«1».«1»
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Proof state:
case «1».«1».«1»
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

Tactic:
exact admissible_E7

Result:
no goals

Proof state:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ Finset.Iio 3
⊢ Admissible {p, q, r}

Tactic:
conv at hp3 => change p ∈ ({1, 2} : Multiset ℕ+)

Result:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p ∈ {1, 2}
⊢ Admissible {p, q, r}

Proof state:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ Admissible {p, q, r}

Tactic:
have hp3 : p < 3 := lt_three hpq hqr H

Result:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p < 3
⊢ Admissible {p, q, r}

Proof state:
case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}

Tactic:
have hq4 : q < 4 := lt_four hqr H

Result:
case «1»
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q < 4
⊢ Admissible {2, q, r}