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

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
⊢ ∀ z ∈ closedBall c r, ‖g z‖ ≤ b
Tactic:
rcases e.gh.maximum_principle (isCompact_closedBall _ _) (Metric.nonempty_closedBall.mpr rp.le)
  with ⟨w, wf, wh⟩
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ frontier (closedBall c r)
wh : ∀ z ∈ closedBall c r, ‖g z‖ ≤ ‖g w‖
⊢ ∀ z ∈ closedBall c r, ‖g z‖ ≤ b

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ frontier (closedBall c r)
wh : ∀ z ∈ closedBall c r, ‖g z‖ ≤ ‖g w‖
⊢ ∀ z ∈ closedBall c r, ‖g z‖ ≤ b
Tactic:
intro z zs
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ frontier (closedBall c r)
wh : ∀ z ∈ closedBall c r, ‖g z‖ ≤ ‖g w‖
z : ℂ
zs : z ∈ closedBall c r
⊢ ‖g z‖ ≤ b

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ frontier (closedBall c r)
wh : ∀ z ∈ closedBall c r, ‖g z‖ ≤ ‖g w‖
z : ℂ
zs : z ∈ closedBall c r
⊢ ‖g z‖ ≤ b
Tactic:
specialize wh z zs
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ frontier (closedBall c r)
z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
⊢ ‖g z‖ ≤ b

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ frontier (closedBall c r)
z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
⊢ ‖g z‖ ≤ b
Tactic:
rw [frontier_closedBall _ rp.ne'] at wf
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ sphere c r
z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
⊢ ‖g z‖ ≤ b

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w : ℂ
wf : w ∈ sphere c r
z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
⊢ ‖g z‖ ≤ b
Tactic:
simp at wf
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
⊢ ‖g z‖ ≤ b

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
⊢ ‖g z‖ ≤ b
Tactic:
generalize hw' : (↑r)⁻¹ * (w - c) = w'
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ ‖g z‖ ≤ b

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ ‖g z‖ ≤ b
Tactic:
have wf' : abs w' = 1 := by
  simp only [wf, abs_of_pos rp, AbsoluteValue.map_mul, map_inv₀, Complex.abs_ofReal, ← hw']
  field_simp [rp.ne']
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
⊢ ‖g z‖ ≤ b

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
⊢ ‖g z‖ ≤ b
Tactic:
rcases mem_addCircle_iff_abs.mp wf' with ⟨t, tw⟩
State after:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
tw : w' = ↑t.toCircle
⊢ ‖g z‖ ≤ b

State before:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
tw : w' = ↑t.toCircle
⊢ ‖g z‖ ≤ b
Tactic:
have b := e.b t
State after:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
tw : w' = ↑t.toCircle
b : f t = g (c + ↑r * ↑t.toCircle)
⊢ ‖g z‖ ≤ b✝

State before:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
tw : w' = ↑t.toCircle
b : f t = g (c + ↑r * ↑t.toCircle)
⊢ ‖g z‖ ≤ b✝
Tactic:
simp only [← tw, rri rp, ← hw'] at b
State after:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
tw : w' = ↑t.toCircle
b : f t = g w
⊢ ‖g z‖ ≤ b✝

State before:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
tw : w' = ↑t.toCircle
b : f t = g w
⊢ ‖g z‖ ≤ b✝
Tactic:
rw [← b] at wh
State after:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
wh : ‖g z‖ ≤ ‖f t‖
tw : w' = ↑t.toCircle
b : f t = g w
⊢ ‖g z‖ ≤ b✝

State before:
case 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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b✝ : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b✝
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
wf' : Complex.abs w' = 1
t : AddCircle (2 * π)
wh : ‖g z‖ ≤ ‖f t‖
tw : w' = ↑t.toCircle
b : f t = g w
⊢ ‖g z‖ ≤ b✝
Tactic:
exact le_trans wh (fb _)
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ Complex.abs w' = 1
Tactic:
simp only [wf, abs_of_pos rp, AbsoluteValue.map_mul, map_inv₀, Complex.abs_ofReal, ← hw']
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ r⁻¹ * r = 1

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
g : ℂ → ℂ
e : HasExtension f g c r
b : ℝ
fb : ∀ (z : Real.Angle), ‖f z‖ ≤ b
rp : 0 < r
w z : ℂ
zs : z ∈ closedBall c r
wh : ‖g z‖ ≤ ‖g w‖
wf : Complex.abs (w - c) = r
w' : ℂ
hw' : (↑r)⁻¹ * (w - c) = w'
⊢ r⁻¹ * r = 1
Tactic:
field_simp [rp.ne']
State after:
no goals