/home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/simple_graph/exponential_ramsey/section5.lean:340:2: ambiguous overload, possible interpretations nat.log_pow real.log_pow Additional information: /home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/simple_graph/exponential_ramsey/section5.lean: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available state: 3 goals t : tendsto coe at_top at_top, h : 0 < 3 / 4 + 1, l : ℕ, h₁ : 1 < l, h₃ : ∀ (k : ℕ), l ≤ k → 128 * log 2 < ((λ (x : ℝ), x ^ (3 / 4 + 1)) ∘ coe) k, h₄ : ∀ (k : ℕ), l ≤ k → 1 ≤ 32 * ↑k ^ (1 / 8) - log ↑k, k : ℕ, hlk : l ≤ k, h₂ : 1 ≤ 1 / 128 * ↑l ^ (3 / 4) * log ↑k, h'₁ : 0 < ↑⌊exp (1 / 128 * ↑l ^ (3 / 4) * log ↑k)⌋₊ ⊢ log (↑⌊exp (1 / 128 * ↑l ^ (3 / 4) * log ↑k)⌋₊ ^ k) + -↑k ^ ((-1) / 8 + 2) / 4 < log (1 / 2) t : tendsto coe at_top at_top, h : 0 < 3 / 4 + 1, l : ℕ, h₁ : 1 < l, h₃ : ∀ (k : ℕ), l ≤ k → 128 * log 2 < ((λ (x : ℝ), x ^ (3 / 4 + 1)) ∘ coe) k, h₄ : ∀ (k : ℕ), l ≤ k → 1 ≤ 32 * ↑k ^ (1 / 8) - log ↑k, k : ℕ, hlk : l ≤ k, h₂ : 1 ≤ 1 / 128 * ↑l ^ (3 / 4) * log ↑k, h'₁ : 0 < ↑⌊exp (1 / 128 * ↑l ^ (3 / 4) * log ↑k)⌋₊ ⊢ 0 < 1 / 2 t : tendsto coe at_top at_top, h : 0 < 3 / 4 + 1, l : ℕ, h₁ : 1 < l, h₃ : ∀ (k : ℕ), l ≤ k → 128 * log 2 < ((λ (x : ℝ), x ^ (3 / 4 + 1)) ∘ coe) k, h₄ : ∀ (k : ℕ), l ≤ k → 1 ≤ 32 * ↑k ^ (1 / 8) - log ↑k, k : ℕ, hlk : l ≤ k, h₂ : 1 ≤ 1 / 128 * ↑l ^ (3 / 4) * log ↑k, h'₁ : 0 < ↑⌊exp (1 / 128 * ↑l ^ (3 / 4) * log ↑k)⌋₊ ⊢ 0 < ↑k

Process completed with exit code 1.