-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
UVl :
  4 / 5 * ε * (4 / 5 * ε) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
      ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts)
nlinarith : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
nlinarith₁ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 1 5 = 5
nlinarith₂ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 1 = 5
nlinarith₃ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
nlinarith₄ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 1 5 = 5
nlinarith₅ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 1 = 5
nlinarith₆ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 5 = 25
nlinarith₇ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 16 / 16 = 1
nlinarith₈ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 1 16 = 16
nlinarith₉ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    3 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 3
nlinarith₁₀ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 16 3 = 48
nlinarith₁₁ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 25 48 = 1200
nlinarith₁₂ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    400 * HPow.hPow (α := ℝ) (β := ℕ) 1 4 = 400
nlinarith₁₃ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 3 / 3 = 1
nlinarith₁₄ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 400 3 = 1200
nlinarith₁₅ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → GT.gt (α := ℝ) 1200 0
nlinarith₁₆ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
nlinarith₁₇ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 1 5 = 5
nlinarith₁₈ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 1 = 5
nlinarith₁₉ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
nlinarith₂₀ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 1 5 = 5
nlinarith₂₁ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 1 = 5
nlinarith₂₂ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 5 = 25
nlinarith₂₃ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 1 25 = 25
nlinarith₂₄ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → GT.gt (α := ℝ) 25 0
nlinarith₂₅ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
nlinarith₂₆ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 1 5 = 5
nlinarith₂₇ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 1 = 5
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2)
have nlinarith₂₈ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → GT.gt (α := ℝ) 5 0
Tactic: nlinarith