Theorem: continuous_to_harmonic_complex (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 : ℝ
fc : ContinuousOn f (sphere c r)
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
by_cases rp : r ≤ 0
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z

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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : ¬r ≤ 0
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z

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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : ¬r ≤ 0
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
simp only [not_le] at rp
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z

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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
generalize hf' : (fun t : Real.Angle ↦ f (c + r * t.toCircle)) = f'
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z

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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
rcases continuousExtend ⟨f', fc'⟩ c rp with ⟨g, e⟩
State after:
case neg.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z

State before:
case neg.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
use g, e.gh
State after:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
⊢ ∀ z ∈ sphere c r, f z = g z

State before:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
⊢ ∀ z ∈ sphere c r, f z = g z
Tactic:
intro z zs
State after:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
⊢ f z = g z

State before:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
⊢ f z = g z
Tactic:
generalize hz' : (↑r)⁻¹ * (z - c) = z'
State after:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
⊢ f z = g z

State before:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
⊢ f z = g z
Tactic:
have za' : abs z' = 1 := by
  simp only [mem_sphere_iff_norm, Complex.norm_eq_abs] at zs
  simp only [zs, abs_of_pos rp, inv_mul_cancel rp.ne', AbsoluteValue.map_mul, map_inv₀,
    Complex.abs_ofReal, ← hz']
State after:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
⊢ f z = g z

State before:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
⊢ f z = g z
Tactic:
rcases mem_addCircle_iff_abs.mp za' with ⟨t, tz⟩
State after:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ f z = g z

State before:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ f z = g z
Tactic:
have rr : c + r * t.toCircle = z := by rw [← tz, ← hz']; exact rri rp _
State after:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
rr : c + ↑r * ↑t.toCircle = z
⊢ f z = g z

State before:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
rr : c + ↑r * ↑t.toCircle = z
⊢ f z = g z
Tactic:
nth_rw 2 [← rr]
State after:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
rr : c + ↑r * ↑t.toCircle = z
⊢ f z = g (c + ↑r * ↑t.toCircle)

State before:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
rr : c + ↑r * ↑t.toCircle = z
⊢ f z = g (c + ↑r * ↑t.toCircle)
Tactic:
rw [← e.b t]
State after:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
rr : c + ↑r * ↑t.toCircle = z
⊢ f z = { toFun := f', continuous_toFun := fc' } t

State before:
case right.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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
rr : c + ↑r * ↑t.toCircle = z
⊢ f z = { toFun := f', continuous_toFun := fc' } t
Tactic:
simp only [← hf', rr, ContinuousMap.coe_mk]
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
use f
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ HarmonicOn f (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = f z

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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ HarmonicOn f (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = f z
Tactic:
use HarmonicOn.subsingleton (Metric.subsingleton_closedBall _ rp)
State after:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ ∀ z ∈ sphere c r, f z = f z

State before:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ ∀ z ∈ sphere c r, f z = f z
Tactic:
intros
State after:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
z✝ : ℂ
a✝ : z✝ ∈ sphere c r
⊢ f z✝ = f z✝

State before:
case right
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
z✝ : ℂ
a✝ : z✝ ∈ sphere c r
⊢ f z✝ = f z✝
Tactic:
rfl
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous f'
Tactic:
rw [← hf']
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => f (c + ↑r * ↑(AddCircle.toCircle t))

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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => f (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
apply fc.comp_continuous
State after:
case hf
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => c + ↑r * ↑(AddCircle.toCircle t)

case hs
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ ∀ (x : Real.Angle), c + ↑r * ↑(AddCircle.toCircle x) ∈ sphere c r

State before:
case hf
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => c + ↑r * ↑(AddCircle.toCircle t)
Tactic:
exact continuous_const.add
  (continuous_const.mul (continuous_subtype_val.comp AddCircle.continuous_toCircle))
State after:
no goals

State before:
case hs
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ ∀ (x : Real.Angle), c + ↑r * ↑(AddCircle.toCircle x) ∈ sphere c r
Tactic:
simp only [mem_sphere_iff_norm, add_sub_cancel_left, Complex.norm_eq_abs,
  AbsoluteValue.map_mul, Complex.abs_ofReal, abs_coe_circle, mul_one, abs_eq_self]
State after:
case hs
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Real.Angle → 0 ≤ r

State before:
case hs
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Real.Angle → 0 ≤ r
Tactic:
intro _
State after:
case hs
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
x✝ : Real.Angle
⊢ 0 ≤ r

State before:
case hs
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
x✝ : Real.Angle
⊢ 0 ≤ r
Tactic:
bound
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
⊢ Complex.abs z' = 1
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs] at zs
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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
zs : Complex.abs (z - c) = r
⊢ Complex.abs z' = 1

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
zs : Complex.abs (z - c) = r
⊢ Complex.abs z' = 1
Tactic:
simp only [zs, abs_of_pos rp, inv_mul_cancel rp.ne', AbsoluteValue.map_mul, map_inv₀,
  Complex.abs_ofReal, ← 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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ c + ↑r * ↑t.toCircle = z
Tactic:
rw [← tz, ← 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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ c + ↑r * ((↑r)⁻¹ * (z - c)) = z

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 : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ c + ↑r * ((↑r)⁻¹ * (z - c)) = z
Tactic:
exact rri rp _
State after:
no goals