-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) :
    (∀ᶠ x in atTop, 0 ≤ f x) ∨ (∀ᶠ x in atTop, f x ≤ 0)

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ x ∈ Set.Ico (n₀ ⊔ 2) (2 * (n₀ ⊔ 2)), f x = f (n₀ ⊔ 2)

Tactic:
intro x ⟨hxlb, hxub⟩

Result:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
x : ℝ
hxlb : n₀ ⊔ 2 ≤ x
hxub : x < 2 * (n₀ ⊔ 2)
⊢ f x = f (n₀ ⊔ 2)

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 3 / 4 * x ≤ x

Tactic:
linarith

Result:
no goals

Proof state:
case intro.intro.intro.intro
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
match lt_trichotomy c₁ c₂ with
| .inl hlt => left
  filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
  have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
    rw [Set.mem_Icc]
    exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
  have hu := hx (3/4 * x) h'
  have hu := Set.nonempty_of_mem hu
  rw [Set.nonempty_Icc] at hu
  have hu' : 0 ≤ (c₂ - c₁) * f x := by linarith
  exact nonneg_of_mul_nonneg_right hu' (by linarith)
| .inr (.inr hgt) => right
  filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
  have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
    rw [Set.mem_Icc]
    exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
  have hu := hx (3/4 * x) h'
  have hu := Set.nonempty_of_mem hu
  rw [Set.nonempty_Icc] at hu
  have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith
  exact nonpos_of_mul_nonpos_right hu' (by linarith)
| .inr (.inl heq) => have hmain : ∃ c, ∀ᶠ x in atTop, f x = c := by
    simp only [heq, Set.Icc_self, Set.mem_singleton_iff, one_mul] at h
    rw [eventually_atTop] at h
    obtain ⟨n₀, hn₀⟩ := h
    refine ⟨f (max n₀ 2), ?_⟩
    rw [eventually_atTop]
    refine ⟨max n₀ 2, ?_⟩
    refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
    case base =>
      intro x ⟨hxlb, hxub⟩
      have h₁ := calc n₀ ≤ 1 * max n₀ 2 := by simp
                      _ ≤ 2 * max n₀ 2 := by gcongr; norm_num
      have h₂ := hn₀ (2 * max n₀ 2) h₁ (max n₀ 2) ⟨by simp [hxlb], by linarith⟩
      rw [h₂]
      exact hn₀ (2 * max n₀ 2) h₁ x ⟨by simp [hxlb], le_of_lt hxub⟩
    case step =>
      intro n hn hyp_ind z hz
      have z_nonneg : 0 ≤ z := by
        calc (0 : ℝ) ≤ (2 : ℝ)^n * max n₀ 2 := by
                      exact mul_nonneg (pow_nonneg (by norm_num) _) (by norm_num)
                _ ≤ z := by exact_mod_cast hz.1
      have le_2n : max n₀ 2 ≤ (2 : ℝ)^n * max n₀ 2 := by
        nth_rewrite 1 [← one_mul (max n₀ 2)]
        gcongr
        exact one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)
      have n₀_le_z : n₀ ≤ z := by
        calc n₀ ≤ max n₀ 2 := by simp
              _ ≤ (2 : ℝ)^n * max n₀ 2 := le_2n
              _ ≤ _ := by exact_mod_cast hz.1
      have fz_eq_c₂fz : f z = c₂ * f z := hn₀ z n₀_le_z z ⟨by linarith, le_rfl⟩
      have z_to_half_z' : f (1/2 * z) = c₂ * f z := hn₀ z n₀_le_z (1/2 * z) ⟨le_rfl, by linarith⟩
      have z_to_half_z : f (1/2 * z) = f z := by rwa [← fz_eq_c₂fz] at z_to_half_z'
      have half_z_to_base : f (1/2 * z) = f (max n₀ 2) := by
        refine hyp_ind (1/2 * z) ⟨?lb, ?ub⟩
        case lb =>
          calc max n₀ 2 ≤ ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ) ^ 1 * max n₀ 2 := by simp
                      _ ≤ ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
                      _ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1
        case ub =>
          have h₁ : (2 : ℝ)^n = ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ)^(n+1) := by
            rw [one_div, pow_add, pow_one]
            ring
          rw [h₁, mul_assoc]
          gcongr
          exact_mod_cast hz.2
      rw [← z_to_half_z, half_z_to_base]
  obtain ⟨c, hc⟩ := hmain
  cases le_or_lt 0 c with
  | inl hpos =>
    exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
  | inr hneg =>
    right
    filter_upwards [hc] with x hc
    exact le_of_lt <| by simpa only [hc]

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
z_nonneg : 0 ≤ z
le_2n : n₀ ⊔ 2 ≤ 2 ^ n * (n₀ ⊔ 2)
n₀_le_z : n₀ ≤ z
⊢ f z = f (n₀ ⊔ 2)

Tactic:
have fz_eq_c₂fz : f z = c₂ * f z := hn₀ z n₀_le_z z ⟨by linarith, le_rfl⟩

Result:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
z_nonneg : 0 ≤ z
le_2n : n₀ ⊔ 2 ≤ 2 ^ n * (n₀ ⊔ 2)
n₀_le_z : n₀ ≤ z
fz_eq_c₂fz : f z = c₂ * f z
⊢ f z = f (n₀ ⊔ 2)

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : (c₁ - c₂) * f x ≤ 0
⊢ 0 < c₁ - c₂

Tactic:
linarith

Result:
no goals

Proof state:
case ub
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
z_nonneg : 0 ≤ z
le_2n : n₀ ⊔ 2 ≤ 2 ^ n * (n₀ ⊔ 2)
n₀_le_z : n₀ ≤ z
fz_eq_c₂fz : f z = c₂ * f z
z_to_half_z' : f (1 / 2 * z) = c₂ * f z
z_to_half_z : f (1 / 2 * z) = f z
⊢ 1 / 2 * z < 2 ^ n * (n₀ ⊔ 2)

Tactic:
case ub =>
  have h₁ : (2 : ℝ)^n = ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ)^(n+1) := by
    rw [one_div, pow_add, pow_one]
    ring
  rw [h₁, mul_assoc]
  gcongr
  exact_mod_cast hz.2

Result:
no goals