all_goals zify [h₁, h₂]; linarith
case intro.intro.refine_1
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ n ≤ 2 * l ^ 2 - 4 * l

case intro.intro.refine_2
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 - 4 * l < 2 * l ^ 2 + 1

case intro.intro.refine_3
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 1 < 2 * l ^ 2 + 4 * l

case intro.intro.refine_4
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 4 * l ≤ 2 * n

case intro.intro.refine_5
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 - 4 * l + (2 * l ^ 2 + 1) = (2 * l - 1) ^ 2

case intro.intro.refine_6
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 4 * l + (2 * l ^ 2 - 4 * l) = (2 * l) ^ 2

case intro.intro.refine_7
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 1 + (2 * l ^ 2 + 4 * l) = (2 * l + 1) ^ 2
no goals