internlm/Lean-Github huggingface dataset:
Theorem: HarmonicOn.subsingleton
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
cm : c ∈ s
rm : c + ↑r ∈ s
e : c = c + ↑r
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
simp [rp.ne'] at e
Proof state after:
no goals
Theorem: HarmonicOn.subsingleton
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: HarmonicOn.subsingleton
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
cm : c ∈ s
⊢ c + ↑r ∈ closedBall c r
Tactic:
simp only [abs_of_pos rp, Metric.mem_closedBall, dist_self_add_left,
  Complex.norm_eq_abs, Complex.abs_ofReal, le_refl]
Proof state after:
no goals
Theorem: continuous_to_harmonic_complex
Proof 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
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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'
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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⟩
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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'
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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']
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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⟩
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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 _
Proof 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
Theorem: continuous_to_harmonic_complex
Proof 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]
Proof 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)
Theorem: continuous_to_harmonic_complex
Proof 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]
Proof 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