Theorem: SubharmonicOn.maximum_principle_ball (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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ IsMaxOn f (closedBall c r) c → ∀ z ∈ closedBall c r, f c = f z
Tactic:
intro cm g gs
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
⊢ f c = f g
Tactic:
by_cases gc : g = c
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : g = c
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
⊢ f c = f g
Tactic:
generalize hu : Complex.abs (g - c) = u
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
⊢ f c = f g
Tactic:
have u0 : u > 0 := by
  simp only [← hu, gt_iff_lt, AbsoluteValue.pos_iff, Ne]
  contrapose gc; simp only [not_not, sub_eq_zero] at gc ⊢; exact gc
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
⊢ f c = f g
Tactic:
have ur : u ≤ r := by
  simp only [Complex.dist_eq, Metric.mem_closedBall] at gs; simp only [←hu, gs]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
⊢ f c = f g
Tactic:
generalize hy : (g - c) / u = y
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
⊢ f c = f g
Tactic:
have y1 : abs y = 1 := by
  simp only [← hy, ← hu, map_div₀, Complex.abs_ofReal, Complex.abs_abs, ne_eq,
    Complex.abs.map_sub_eq_zero_iff, div_self (Complex.abs.ne_zero_iff.mpr (sub_ne_zero.mpr gc))]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
⊢ f c = f g
Tactic:
generalize hs : (fun t : ℝ ↦ f (c + t * y)) ⁻¹' {f c} = s
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
⊢ f c = f g
Tactic:
have s0 : (0 : ℝ) ∈ s := by
  simp only [← hs, Set.mem_preimage, Complex.ofReal_zero, MulZeroClass.zero_mul, add_zero,
    Set.mem_singleton]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
us : u ∈ s
⊢ f c = f g
Tactic:
simp only [← hs, ← hy, Set.mem_preimage, Set.mem_singleton_iff] at us
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
us : f (c + ↑u * ((g - c) / ↑u)) = f c
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
us : f (c + ↑u * ((g - c) / ↑u)) = f c
⊢ f c = f g
Tactic:
have unz : (u : ℂ) ≠ 0 := by
  simp only [u0.ne', Ne, Complex.ofReal_eq_zero, not_false_iff]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
us : f (c + ↑u * ((g - c) / ↑u)) = f c
unz : ↑u ≠ 0
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
us : f (c + ↑u * ((g - c) / ↑u)) = f c
unz : ↑u ≠ 0
⊢ f c = f g
Tactic:
field_simp [unz] at us
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
unz : ↑u ≠ 0
us : f g = f c
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
unz : ↑u ≠ 0
us : f g = f c
⊢ f c = f g
Tactic:
exact us.symm
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : g = c
⊢ f c = f g
Tactic:
rw [gc]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
⊢ u > 0
Tactic:
simp only [← hu, gt_iff_lt, 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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
⊢ ¬g - c = 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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
⊢ ¬g - c = 0
Tactic:
contrapose gc
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
u : ℝ
hu : Complex.abs (g - c) = u
gc : ¬¬g - c = 0
⊢ ¬¬g = c

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
u : ℝ
hu : Complex.abs (g - c) = u
gc : ¬¬g - c = 0
⊢ ¬¬g = c
Tactic:
simp only [not_not, sub_eq_zero] at gc ⊢
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
u : ℝ
hu : Complex.abs (g - c) = u
gc : g = c
⊢ g = c

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
u : ℝ
hu : Complex.abs (g - c) = u
gc : g = c
⊢ g = c
Tactic:
exact gc
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
⊢ u ≤ r
Tactic:
simp only [Complex.dist_eq, Metric.mem_closedBall] at gs
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
gs : Complex.abs (g - c) ≤ r
⊢ u ≤ r

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
gs : Complex.abs (g - c) ≤ r
⊢ u ≤ r
Tactic:
simp only [←hu, gs]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
⊢ Complex.abs y = 1
Tactic:
simp only [← hy, ← hu, map_div₀, Complex.abs_ofReal, Complex.abs_abs, ne_eq,
  Complex.abs.map_sub_eq_zero_iff, div_self (Complex.abs.ne_zero_iff.mpr (sub_ne_zero.mpr gc))]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
⊢ 0 ∈ s
Tactic:
simp only [← hs, Set.mem_preimage, Complex.ofReal_zero, MulZeroClass.zero_mul, add_zero,
  Set.mem_singleton]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ u ∈ s
Tactic:
refine IsClosed.mem_of_ge_of_forall_exists_gt ?_ s0 u0.le ?_
State after:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ IsClosed (s ∩ Icc 0 u)

case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ ∀ x ∈ s ∩ Set.Ico 0 u, (s ∩ Ioc x u).Nonempty

State before:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ IsClosed (s ∩ Icc 0 u)
Tactic:
rw [← hs]
State after:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ IsClosed ((fun t => f (c + ↑t * y)) ⁻¹' {f c} ∩ Icc 0 u)

State before:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ IsClosed ((fun t => f (c + ↑t * y)) ⁻¹' {f c} ∩ Icc 0 u)
Tactic:
rw [Set.inter_comm]
State after:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ IsClosed (Icc 0 u ∩ (fun t => f (c + ↑t * y)) ⁻¹' {f c})

State before:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ IsClosed (Icc 0 u ∩ (fun t => f (c + ↑t * y)) ⁻¹' {f c})
Tactic:
refine ContinuousOn.preimage_isClosed_of_isClosed ?_ isClosed_Icc isClosed_singleton
State after:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ ContinuousOn (fun t => f (c + ↑t * y)) (Icc 0 u)

State before:
case refine_1
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ ContinuousOn (fun t => f (c + ↑t * y)) (Icc 0 u)
Tactic:
apply fs.cont.comp (Continuous.continuousOn _) _
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ Continuous fun t => c + ↑t * y

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ Set.MapsTo (fun t => c + ↑t * y) (Icc 0 u) (closedBall c r)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ Continuous fun t => c + ↑t * y
Tactic:
exact continuous_const.add (Continuous.mul Complex.continuous_ofReal continuous_const)
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ Set.MapsTo (fun t => c + ↑t * y) (Icc 0 u) (closedBall c r)
Tactic:
intro t ts
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : t ∈ Icc 0 u
⊢ (fun t => c + ↑t * y) t ∈ closedBall c r

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : t ∈ Icc 0 u
⊢ (fun t => c + ↑t * y) t ∈ closedBall c r
Tactic:
simp only [Set.mem_Icc] at ts
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : 0 ≤ t ∧ t ≤ u
⊢ (fun t => c + ↑t * y) t ∈ closedBall c r

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : 0 ≤ t ∧ t ≤ u
⊢ (fun t => c + ↑t * y) t ∈ closedBall c r
Tactic:
simp only [y1, abs_of_nonneg ts.1, _root_.trans ts.2 ur, Metric.mem_closedBall,
  dist_self_add_left, Complex.norm_eq_abs, AbsoluteValue.map_mul, Complex.abs_ofReal,
  mul_one]
State after:
no goals

State before:
case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
⊢ ∀ x ∈ s ∩ Set.Ico 0 u, (s ∩ Ioc x u).Nonempty
Tactic:
intro t ts
State after:
case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : t ∈ s ∩ Set.Ico 0 u
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : t ∈ s ∩ Set.Ico 0 u
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
simp only [← hs, Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff,
  Set.mem_Ico] at ts
State after:
case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : f (c + ↑t * y) = f c ∧ 0 ≤ t ∧ t < u
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : f (c + ↑t * y) = f c ∧ 0 ≤ t ∧ t < u
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
generalize hz : c + t * y = z
State after:
case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : f (c + ↑t * y) = f c ∧ 0 ≤ t ∧ t < u
z : ℂ
hz : c + ↑t * y = z
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
ts : f (c + ↑t * y) = f c ∧ 0 ≤ t ∧ t < u
z : ℂ
hz : c + ↑t * y = z
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rcases ts with ⟨fz, tp, tu⟩
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have tz : abs (z - c) = t := by
  simp only [y1, abs_of_nonneg tp, add_sub_cancel_left, AbsoluteValue.map_mul,
    Complex.abs_ofReal, mul_one, ← hz]
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have zs : z ∈ ball c r := by
  simp only [y1, abs_of_nonneg tp, Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs,
    AbsoluteValue.map_mul, Complex.abs_ofReal, mul_one, ← hz]
  exact lt_of_lt_of_le tu ur
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ ball c r
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ ball c r
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rw [← interior_closedBall _ rp.ne'] at zs
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rcases fs.submean' z zs with ⟨e, ep, lo⟩
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
generalize he' : min (e / 2) (u - t) = e'
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have e'p : e' > 0 := by rw [←he']; exact lt_min (half_pos ep) (by linarith)
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have e's : e' < e := by rw [← he']; exact lt_of_le_of_lt (min_le_left _ _) (half_lt_self ep)
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
specialize lo e' e'p e's
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rw [← hz, fz] at lo
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have ss : closedBall z e' ⊆ closedBall c r := by
  apply Metric.closedBall_subset_closedBall'; rw [Complex.dist_eq, tz]; linarith
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have hi : ∀ x, x ∈ itau → f (circleMap z e' x) ≤ f c := by
  intro x _; apply isMaxOn_iff.mp cm; apply ss
  simp only [Complex.dist_eq, Metric.mem_closedBall, circleMap_sub_center, abs_circleMap_zero,
    abs_of_pos e'p, le_refl]
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have fcc : ContinuousOn (fun a ↦ f (circleMap z e' a)) itau := by
  apply (fs.cont.mono ss).comp (continuous_circleMap _ _).continuousOn; intro a _
  simp only [Complex.dist_eq, abs_of_pos e'p, Metric.mem_closedBall, circleMap_sub_center,
    abs_circleMap_zero, le_refl]
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rw [hz] at lo
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have fw := mean_squeeze NiceVolume.itau LocalVolume.itau fcc
  ((fs.cont.mono ss).integrableOn_sphere e'p) lo hi
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have eys : z + e' * y ∈ sphere z e' := by
  simp only [abs_of_pos e'p, y1, mem_sphere_iff_norm, add_sub_cancel_left,
    Complex.norm_eq_abs, AbsoluteValue.map_mul, Complex.abs_ofReal, mul_one]
State after:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
eys : z + ↑e' * y ∈ sphere z e'
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
eys : z + ↑e' * y ∈ sphere z e'
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rcases circleMap_Ioc eys with ⟨a, as, aey⟩
State after:
case refine_2.intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
specialize fw a as
State after:
case refine_2.intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (circleMap z e' a) = f c
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (circleMap z e' a) = f c
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
simp only [← aey] at fw
State after:
case refine_2.intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ (s ∩ Ioc t u).Nonempty

State before:
case refine_2.intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
use t + e'
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∩ Ioc t u

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∩ Ioc t u
Tactic:
simp only [Set.mem_inter_iff, Set.mem_Ioc, lt_add_iff_pos_right]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∧ 0 < e' ∧ t + e' ≤ u

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∧ 0 < e' ∧ t + e' ≤ u
Tactic:
refine ⟨?_, e'p, teu⟩
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ 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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s
Tactic:
simp only [← hs, right_distrib, Set.mem_preimage, Complex.ofReal_add, Set.mem_singleton_iff]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ f (c + (↑t * y + ↑e' * y)) = f c

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ f (c + (↑t * y + ↑e' * y)) = f c
Tactic:
rw [← add_assoc, hz]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ f (z + ↑e' * y) = f c

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ f (z + ↑e' * y) = f c
Tactic:
exact fw
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
⊢ Complex.abs (z - c) = t
Tactic:
simp only [y1, abs_of_nonneg tp, add_sub_cancel_left, AbsoluteValue.map_mul,
  Complex.abs_ofReal, mul_one, ← hz]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
⊢ z ∈ ball c r
Tactic:
simp only [y1, abs_of_nonneg tp, Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs,
  AbsoluteValue.map_mul, Complex.abs_ofReal, mul_one, ← hz]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
⊢ t < r

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
⊢ t < r
Tactic:
exact lt_of_lt_of_le tu ur
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
⊢ e' > 0
Tactic:
rw [←he']
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
⊢ min (e / 2) (u - t) > 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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
⊢ min (e / 2) (u - t) > 0
Tactic:
exact lt_min (half_pos ep) (by linarith)
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
⊢ 0 < u - t
Tactic:
linarith
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + e' ≤ u
Tactic:
rw [← he']
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + min (e / 2) (u - t) ≤ u

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + min (e / 2) (u - t) ≤ u
Tactic:
trans t + (u - t)
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + min (e / 2) (u - t) ≤ t + (u - t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + (u - t) ≤ u

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + min (e / 2) (u - t) ≤ t + (u - t)
Tactic:
exact add_le_add_left (min_le_right _ _) _
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + (u - t) ≤ u
Tactic:
simp only [add_sub_cancel, le_refl]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
⊢ e' < e
Tactic:
rw [← he']
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
⊢ min (e / 2) (u - t) < e

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
⊢ min (e / 2) (u - t) < e
Tactic:
exact lt_of_le_of_lt (min_le_left _ _) (half_lt_self ep)
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ closedBall z e' ⊆ closedBall c r
Tactic:
apply Metric.closedBall_subset_closedBall'
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ e' + dist z c ≤ r

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ e' + dist z c ≤ r
Tactic:
rw [Complex.dist_eq, tz]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ e' + t ≤ r

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ e' + t ≤ r
Tactic:
linarith
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
⊢ ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
Tactic:
intro x _
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ f (circleMap z e' x) ≤ f c

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ f (circleMap z e' x) ≤ f c
Tactic:
apply isMaxOn_iff.mp cm
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall c 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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall c r
Tactic:
apply ss
State after:
case a.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall z e'

State before:
case a.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall z e'
Tactic:
simp only [Complex.dist_eq, Metric.mem_closedBall, circleMap_sub_center, abs_circleMap_zero,
  abs_of_pos e'p, le_refl]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ ContinuousOn (fun a => f (circleMap z e' a)) itau
Tactic:
apply (fs.cont.mono ss).comp (continuous_circleMap _ _).continuousOn
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ Set.MapsTo (circleMap z e') itau (closedBall z e')

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ Set.MapsTo (circleMap z e') itau (closedBall z e')
Tactic:
intro a _
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
a : ℝ
a✝ : a ∈ itau
⊢ circleMap z e' a ∈ closedBall z e'

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
a : ℝ
a✝ : a ∈ itau
⊢ circleMap z e' a ∈ closedBall z e'
Tactic:
simp only [Complex.dist_eq, abs_of_pos e'p, Metric.mem_closedBall, circleMap_sub_center,
  abs_circleMap_zero, le_refl]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
⊢ z + ↑e' * y ∈ sphere z e'
Tactic:
simp only [abs_of_pos e'p, y1, mem_sphere_iff_norm, add_sub_cancel_left,
  Complex.norm_eq_abs, AbsoluteValue.map_mul, Complex.abs_ofReal, mul_one]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
us : f (c + ↑u * ((g - c) / ↑u)) = f c
⊢ ↑u ≠ 0
Tactic:
simp only [u0.ne', Ne, Complex.ofReal_eq_zero, not_false_iff]
State after:
no goals