Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
r2p : r2 > 0
r1p : r1 > 0
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
have rde : d = e * (ENNReal.ofReal (π * r1 ^ 2) * ENNReal.ofReal (π * r2 ^ 2)⁻¹) := by
  rw [← ENNReal.ofReal_mul (by bound : π * r1 ^ 2 ≥ 0), ← hr1, mul_pow, Real.sq_sqrt dep.le]
  have smash : π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹ = d.toReal / e.toReal := by
    calc π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹
      _ = π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π⁻¹ * (r2 ^ 2)⁻¹) := by simp_rw [mul_inv]
      _ = d.toReal / e.toReal * (π * π⁻¹) * (r2 ^ 2 * (r2 ^ 2)⁻¹) := by ring_nf
      _ = d.toReal / e.toReal := by simp only [mul_inv_cancel Real.pi_pos.ne',
          mul_inv_cancel (pow_ne_zero _ r2p.ne'), mul_one]
  rw [smash, ENNReal.ofReal_div_of_pos erp, ENNReal.ofReal_toReal df, ENNReal.ofReal_toReal ef]
  rw [ENNReal.mul_div_cancel' ez ef]
Proof state after:
case neg.intro.intro.hnhds.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
r2p : r2 > 0
r1p : r1 > 0
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
rde : d = e * (ENNReal.ofReal (π * r1 ^ 2) * ENNReal.ofReal (π * r2 ^ 2)⁻¹)
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d