internlm/Lean-Github huggingface dataset:
Theorem: mem_addCircle_iff_abs
Proof state before:
case mp.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 : ℝ
z : ℂ
az : Complex.abs z = 1
t : ℝ
h : (↑t * I).exp = z
⊢ ∃ t, z = ↑t.toCircle
Tactic:
use t
Proof 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
c : ℂ
r : ℝ
z : ℂ
az : Complex.abs z = 1
t : ℝ
h : (↑t * I).exp = z
⊢ z = ↑(AddCircle.toCircle ↑t)
Theorem: mem_addCircle_iff_abs
Proof 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
c : ℂ
r : ℝ
z : ℂ
az : Complex.abs z = 1
t : ℝ
h : (↑t * I).exp = z
⊢ z = ↑(AddCircle.toCircle ↑t)
Tactic:
simp only [← h, AddCircle.toCircle, Function.Periodic.lift_coe, expMapCircle_apply,
  Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_one]
Proof 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
c : ℂ
r : ℝ
z : ℂ
az : Complex.abs z = 1
t : ℝ
h : (↑t * I).exp = z
⊢ (↑t * I).exp = (↑2 * ↑π / (↑2 * ↑π) * ↑t * I).exp
Theorem: mem_addCircle_iff_abs
Proof 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
c : ℂ
r : ℝ
z : ℂ
az : Complex.abs z = 1
t : ℝ
h : (↑t * I).exp = z
⊢ (↑t * I).exp = (↑2 * ↑π / (↑2 * ↑π) * ↑t * I).exp
Tactic:
field_simp [Real.pi_pos.ne']
Proof state after:
no goals
Theorem: mem_addCircle_iff_abs
Proof state before:
case mpr
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace 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 : ℝ
z : ℂ
⊢ (∃ t, z = ↑t.toCircle) → Complex.abs z = 1
Tactic:
intro h
Proof state after:
case mpr
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace 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 : ℝ
z : ℂ
h : ∃ t, z = ↑t.toCircle
⊢ Complex.abs z = 1
Theorem: mem_addCircle_iff_abs
Proof state before:
case mpr
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace 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 : ℝ
z : ℂ
h : ∃ t, z = ↑t.toCircle
⊢ Complex.abs z = 1
Tactic:
rcases h with ⟨t, h⟩
Proof state after:
case mpr.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 : ℝ
z : ℂ
t : AddCircle (2 * π)
h : z = ↑t.toCircle
⊢ Complex.abs z = 1
Theorem: mem_addCircle_iff_abs
Proof state before:
case mpr.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 : ℝ
z : ℂ
t : AddCircle (2 * π)
h : z = ↑t.toCircle
⊢ Complex.abs z = 1
Tactic:
simp only [h, abs_coe_circle]
Proof state after:
no goals
Theorem: Extension.maximum_principle
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
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⟩
Proof 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
Theorem: Extension.maximum_principle
Proof 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
Proof 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
Theorem: Extension.maximum_principle
Proof 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
Proof 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
Theorem: Extension.maximum_principle
Proof 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
Proof 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
Theorem: Extension.maximum_principle
Proof 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
Proof 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
Theorem: Extension.maximum_principle
Proof 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'
Proof 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
Theorem: Extension.maximum_principle
Proof 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']
Proof 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
Theorem: Extension.maximum_principle
Proof 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⟩
Proof 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
Theorem: Extension.maximum_principle
Proof 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
Proof 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✝
Theorem: Extension.maximum_principle
Proof 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
Proof 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✝