Theorem: SubharmonicOn.maximum_principle (Ray/Hartogs/Subharmonic.lean)

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
⊢ ∃ w ∈ frontier s, IsMaxOn f s w
Tactic:
rcases sc.exists_isMaxOn sn fs.cont with ⟨x, xs, xm⟩
State after:
case 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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
⊢ ∃ w ∈ frontier s, IsMaxOn f s w

State before:
case 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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
⊢ ∃ w ∈ frontier s, IsMaxOn f s w
Tactic:
rcases exists_mem_frontier_infDist_compl_eq_dist xs sc.ne_univ with ⟨w, wb, h⟩
State after:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
⊢ ∃ w ∈ frontier s, IsMaxOn f s w

State before:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
⊢ ∃ w ∈ frontier s, IsMaxOn f s w
Tactic:
exists w, wb
State after:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
⊢ IsMaxOn f s w

State before:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
⊢ IsMaxOn f s w
Tactic:
generalize hr : abs (w - x) = r
State after:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
⊢ IsMaxOn f s w

State before:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
⊢ IsMaxOn f s w
Tactic:
by_cases wx : w = x
State after:
case pos
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : w = x
⊢ IsMaxOn f s w

case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ IsMaxOn f s w

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ IsMaxOn f s w
Tactic:
have rp : r > 0 := by
  simp only [← hr, AbsoluteValue.pos_iff, Ne]; exact sub_ne_zero.mpr wx
State after:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w
Tactic:
rw [dist_comm, Complex.dist_eq, hr] at h
State after:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w
Tactic:
have rs : closedBall x r ⊆ s := by
  rw [← closure_ball x rp.ne', ← sc.isClosed.closure_eq]; apply closure_mono
  rw [← h]; apply Metric.ball_infDist_compl_subset
State after:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
⊢ IsMaxOn f s w

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
⊢ IsMaxOn f s w
Tactic:
have rm : IsMaxOn f (closedBall x r) x := by intro y ys; exact xm (rs ys)
State after:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ IsMaxOn f s w

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ IsMaxOn f s w
Tactic:
have wx : f x = f w := by
  apply SubharmonicOn.maximum_principle_ball (fs.mono rs) rp rm
  simp only [Complex.dist_eq, Metric.mem_closedBall, hr, le_refl]
State after:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
⊢ IsMaxOn f s w

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
⊢ IsMaxOn f s w
Tactic:
intro y ys
State after:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x | (fun x => f x ≤ f w) x}

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x | (fun x => f x ≤ f w) x}
Tactic:
rw [← wx]
State after:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}

State before:
case neg
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}
Tactic:
exact xm ys
State after:
no goals

State before:
case pos
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : w = x
⊢ IsMaxOn f s w
Tactic:
rwa [wx]
State after:
no goals

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ r > 0
Tactic:
simp only [← hr, AbsoluteValue.pos_iff, Ne]
State after:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ ¬w - x = 0

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ ¬w - x = 0
Tactic:
exact sub_ne_zero.mpr wx
State after:
no goals

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ closedBall x r ⊆ s
Tactic:
rw [← closure_ball x rp.ne', ← sc.isClosed.closure_eq]
State after:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ closure (ball x r) ⊆ closure s

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ closure (ball x r) ⊆ closure s
Tactic:
apply closure_mono
State after:
case h
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x r ⊆ s

State before:
case h
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x r ⊆ s
Tactic:
rw [← h]
State after:
case h
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x (Metric.infDist x sᶜ) ⊆ s

State before:
case h
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x (Metric.infDist x sᶜ) ⊆ s
Tactic:
apply Metric.ball_infDist_compl_subset
State after:
no goals

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
⊢ IsMaxOn f (closedBall x r) x
Tactic:
intro y ys
State after:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
y : ℂ
ys : y ∈ closedBall x r
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
y : ℂ
ys : y ∈ closedBall x r
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}
Tactic:
exact xm (rs ys)
State after:
no goals

State before:
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ f x = f w
Tactic:
apply SubharmonicOn.maximum_principle_ball (fs.mono rs) rp rm
State after:
case a
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ w ∈ closedBall x r

State before:
case a
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ w ∈ closedBall x r
Tactic:
simp only [Complex.dist_eq, Metric.mem_closedBall, hr, le_refl]
State after:
no goals