internlm/Lean-Github huggingface dataset:
Theorem: IsClosed.extendable
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ TendstoUniformlyOn g G atTop (closedBall c r)
Tactic:
apply UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto cauchy
Proof 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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ ∀ x ∈ closedBall c r, Tendsto (fun n => g n x) atTop (𝓝 (G x))
Theorem: IsClosed.extendable
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ ∀ x ∈ closedBall c r, Tendsto (fun n => g n x) atTop (𝓝 (G x))
Tactic:
intro z zs
Proof 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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
z : ℂ
zs : z ∈ closedBall c r
⊢ Tendsto (fun n => g n z) atTop (𝓝 (G z))
Theorem: IsClosed.extendable
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
z : ℂ
zs : z ∈ closedBall c r
⊢ Tendsto (fun n => g n z) atTop (𝓝 (G z))
Tactic:
exact (cauchy.cauchySeq zs).tendsto_limUnder
Proof state after:
no goals
Theorem: IsClosed.extendable
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ ∀ (t : Real.Angle), F t = G (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
intro z
Proof 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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ F z = G (c + ↑r * ↑(AddCircle.toCircle z))
Theorem: IsClosed.extendable
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ F z = G (c + ↑r * ↑(AddCircle.toCircle z))
Tactic:
refine (Filter.Tendsto.limUnder_eq ?_).symm
Proof 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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => g n (c + ↑r * ↑(AddCircle.toCircle z))) atTop (𝓝 (F z))
Theorem: IsClosed.extendable
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => g n (c + ↑r * ↑(AddCircle.toCircle z))) atTop (𝓝 (F z))
Tactic:
simp_rw [← (gs _).b]
Proof 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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => (f n) z) atTop (𝓝 (F z))
Theorem: IsClosed.extendable
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => (f n) z) atTop (𝓝 (F z))
Tactic:
exact fF.tendsto_at z
Proof state after:
no goals
Theorem: toCircle_neg
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 T : ℝ
x : AddCircle T
⊢ (-x).toCircle = x.toCircle⁻¹
Tactic:
induction x using QuotientAddGroup.induction_on'
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 T z✝ : ℝ
⊢ (-↑z✝).toCircle = (AddCircle.toCircle ↑z✝)⁻¹
Theorem: toCircle_neg
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 T z✝ : ℝ
⊢ (-↑z✝).toCircle = (AddCircle.toCircle ↑z✝)⁻¹
Tactic:
rw [←AddCircle.coe_neg]
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 T z✝ : ℝ
⊢ AddCircle.toCircle ↑(-z✝) = (AddCircle.toCircle ↑z✝)⁻¹
Theorem: toCircle_neg
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 T z✝ : ℝ
⊢ AddCircle.toCircle ↑(-z✝) = (AddCircle.toCircle ↑z✝)⁻¹
Tactic:
simp only [← AddCircle.coe_neg, AddCircle.toCircle, Function.Periodic.lift_coe, mul_neg,
  expMapCircle_neg]
Proof state after:
no goals
Theorem: toCircle_smul
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 T : ℝ
n : ℕ
x : AddCircle T
⊢ (n • x).toCircle = x.toCircle ^ n
Tactic:
induction' x using QuotientAddGroup.induction_on' with z
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 T : ℝ
n : ℕ
z : ℝ
⊢ (n • ↑z).toCircle = AddCircle.toCircle ↑z ^ n
Theorem: toCircle_smul
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 T : ℝ
n : ℕ
z : ℝ
⊢ (n • ↑z).toCircle = AddCircle.toCircle ↑z ^ n
Tactic:
rw [←AddCircle.coe_nsmul]
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 T : ℝ
n : ℕ
z : ℝ
⊢ AddCircle.toCircle ↑(n • z) = AddCircle.toCircle ↑z ^ n
Theorem: toCircle_smul
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 T : ℝ
n : ℕ
z : ℝ
⊢ AddCircle.toCircle ↑(n • z) = AddCircle.toCircle ↑z ^ n
Tactic:
simp only [AddCircle.toCircle, Function.Periodic.lift_coe]
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 T : ℝ
n : ℕ
z : ℝ
⊢ expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n
Theorem: toCircle_smul
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 T : ℝ
n : ℕ
z : ℝ
⊢ expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n
Tactic:
induction' n with n h
Proof state after:
case H.zero
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace 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 T z : ℝ
⊢ expMapCircle (2 * π / T * 0 • z) = expMapCircle (2 * π / T * z) ^ 0

case H.succ
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace 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 T z : ℝ
n : ℕ
h : expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n
⊢ expMapCircle (2 * π / T * (n + 1) • z) = expMapCircle (2 * π / T * z) ^ (n + 1)
Theorem: toCircle_smul
Proof state before:
case H.zero
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace 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 T z : ℝ
⊢ expMapCircle (2 * π / T * 0 • z) = expMapCircle (2 * π / T * z) ^ 0
Tactic:
simp only [expMapCircle_zero, nsmul_eq_mul, algebraMap.coe_zero, MulZeroClass.zero_mul,
  MulZeroClass.mul_zero, pow_zero, Nat.zero_eq, zero_smul, Function.Periodic.lift_coe]
Proof state after:
no goals
Theorem: toCircle_smul
Proof state before:
case H.succ
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace 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 T z : ℝ
n : ℕ
h : expMapCircle (2 * π / T * n • z) = expMapCircle (2 * π / T * z) ^ n
⊢ expMapCircle (2 * π / T * (n + 1) • z) = expMapCircle (2 * π / T * z) ^ (n + 1)
Tactic:
simp only [succ_nsmul, left_distrib, expMapCircle_add, h, pow_succ]
Proof state after:
no goals