internlm/Lean-Github huggingface dataset:
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ 3 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ 1 < Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
h : |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
p0 : 0 < s.potential c ↑z
⊢ 2 < Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
⊢ (-p.log).log ∈ t
Tactic:
simp only [abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right, add_comm r] at h
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
h : (Complex.abs z).log.log ≤ (-p.log).log + r ∧ (-p.log).log ≤ (Complex.abs z).log.log + r
⊢ (-p.log).log ∈ t
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
h : (Complex.abs z).log.log ≤ (-p.log).log + r ∧ (-p.log).log ≤ (Complex.abs z).log.log + r
⊢ (-p.log).log ∈ t
Tactic:
simp only [mem_Ici, tsub_le_iff_right, h, t]
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
⊢ (Complex.abs z).log.log ∈ t
Tactic:
simp only [mem_Ici, tsub_le_iff_right, le_add_iff_nonneg_right, r0, t]
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
⊢ 0 ≤ b
Tactic:
rw [←hb]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
⊢ 0 ≤ dene ((Complex.abs z).log.log - r)
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
⊢ 0 ≤ dene ((Complex.abs z).log.log - r)
Tactic:
exact dene_nonneg
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
⊢ ∀ x ∈ t, ‖deriv ene x‖ ≤ b
Tactic:
intro x m
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
x : ℝ
m : x ∈ t
⊢ ‖deriv ene x‖ ≤ b
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
x : ℝ
m : x ∈ t
⊢ ‖deriv ene x‖ ≤ b
Tactic:
simp only [Real.dist_eq, mem_Ici, ←hr, t] at m
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
x : ℝ
m : (Complex.abs z).log.log - iter_error d c z ≤ x
⊢ ‖deriv ene x‖ ≤ b
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
x : ℝ
m : (Complex.abs z).log.log - iter_error d c z ≤ x
⊢ ‖deriv ene x‖ ≤ b
Tactic:
simp only [deriv_ene, norm_neg, Real.norm_of_nonneg dene_nonneg, ←hb, ←hr]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
x : ℝ
m : (Complex.abs z).log.log - iter_error d c z ≤ x
⊢ dene x ≤ dene ((Complex.abs z).log.log - iter_error d c z)
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
x : ℝ
m : (Complex.abs z).log.log - iter_error d c z ≤ x
⊢ dene x ≤ dene ((Complex.abs z).log.log - iter_error d c z)
Tactic:
apply dene_anti (sub_nonneg.mpr (iter_error_le_log_log_abs d z4 cz)) m
Proof state after:
no goals
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |ene (-p.log).log - ene (Complex.abs z).log.log| ≤ b * |(-p.log).log - (Complex.abs z).log.log|
⊢ 0 ≤ b
Tactic:
bound
Proof state after:
no goals
Theorem: RiemannSphere.coe_eq_zero
Proof state before:
z : ℂ
⊢ ↑z = 0 ↔ z = 0
Tactic:
simp only [← coe_zero, coe_eq_coe]
Proof state after:
no goals
Theorem: RiemannSphere.map_rec
Proof state before:
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
z : 𝕊
⊢ g (OnePoint.rec i f z) = OnePoint.rec (g i) (g ∘ f) z
Tactic:
induction z using OnePoint.rec
Proof state after:
case h₁
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
⊢ g (OnePoint.rec i f ∞) = OnePoint.rec (g i) (g ∘ f) ∞

case h₂
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
x✝ : ℂ
⊢ g (OnePoint.rec i f ↑x✝) = OnePoint.rec (g i) (g ∘ f) ↑x✝
Theorem: RiemannSphere.map_rec
Proof state before:
case h₁
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
⊢ g (OnePoint.rec i f ∞) = OnePoint.rec (g i) (g ∘ f) ∞
Tactic:
simp only [rec_inf]
Proof state after:
no goals
Theorem: RiemannSphere.map_rec
Proof state before:
case h₂
A : Sort u_1
B : Sort u_2
g : A → B
f : ℂ → A
i : A
x✝ : ℂ
⊢ g (OnePoint.rec i f ↑x✝) = OnePoint.rec (g i) (g ∘ f) ↑x✝
Tactic:
simp only [rec_coe, Function.comp]
Proof state after:
no goals
Theorem: RiemannSphere.inf_ne_coe
Proof state before:
z : ℂ
⊢ ∞ ≠ ↑z
Tactic:
simp only [Ne, OnePoint.infty_ne_coe, not_false_iff]
Proof state after:
no goals
Theorem: RiemannSphere.inf_ne_zero
Proof state before:
⊢ ∞ ≠ 0
Tactic:
have e : (0 : 𝕊) = ((0 : ℂ) : 𝕊) := rfl
Proof state after:
e : 0 = ↑0
⊢ ∞ ≠ 0
Theorem: RiemannSphere.inf_ne_zero
Proof state before:
e : 0 = ↑0
⊢ ∞ ≠ 0
Tactic:
rw [e]
Proof state after:
e : 0 = ↑0
⊢ ∞ ≠ ↑0
Theorem: RiemannSphere.inf_ne_zero
Proof state before:
e : 0 = ↑0
⊢ ∞ ≠ ↑0
Tactic:
exact inf_ne_coe
Proof state after:
no goals
Theorem: RiemannSphere.coe_toComplex
Proof state before:
z : 𝕊
h : z ≠ ∞
⊢ ↑z.toComplex = z
Tactic:
induction z using OnePoint.rec
Proof state after:
case h₁
h : ∞ ≠ ∞
⊢ ↑∞.toComplex = ∞

case h₂
x✝ : ℂ
h : ↑x✝ ≠ ∞
⊢ ↑(↑x✝).toComplex = ↑x✝
Theorem: RiemannSphere.coe_toComplex
Proof state before:
case h₁
h : ∞ ≠ ∞
⊢ ↑∞.toComplex = ∞
Tactic:
simp only [ne_eq, not_true_eq_false] at h
Proof state after:
no goals
Theorem: RiemannSphere.coe_toComplex
Proof state before:
case h₂
x✝ : ℂ
h : ↑x✝ ≠ ∞
⊢ ↑(↑x✝).toComplex = ↑x✝
Tactic:
simp only [toComplex_coe]
Proof state after:
no goals
Theorem: RiemannSphere.toComplex_zero
Proof state before:
⊢ OnePoint.toComplex 0 = 0
Tactic:
rw [← coe_zero, toComplex_coe]
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_toComplex
Proof state before:
z : ℂ
⊢ ContinuousAt OnePoint.toComplex ↑z
Tactic:
simp only [OnePoint.continuousAt_coe, Function.comp, toComplex_coe]
Proof state after:
z : ℂ
⊢ ContinuousAt (fun x => x) z
Theorem: RiemannSphere.continuousAt_toComplex
Proof state before:
z : ℂ
⊢ ContinuousAt (fun x => x) z
Tactic:
exact continuousAt_id
Proof state after:
no goals
Theorem: RiemannSphere.continuousOn_toComplex
Proof state before:
⊢ ContinuousOn OnePoint.toComplex {∞}ᶜ
Tactic:
intro z m
Proof state after:
z : 𝕊
m : z ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ z
Theorem: RiemannSphere.continuousOn_toComplex
Proof state before:
z : 𝕊
m : z ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ z
Tactic:
induction z using OnePoint.rec
Proof state after:
case h₁
m : ∞ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ∞

case h₂
x✝ : ℂ
m : ↑x✝ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ↑x✝
Theorem: RiemannSphere.continuousOn_toComplex
Proof state before:
case h₁
m : ∞ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ∞
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, not_true] at m
Proof state after:
no goals
Theorem: RiemannSphere.continuousOn_toComplex
Proof state before:
case h₂
x✝ : ℂ
m : ↑x✝ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ↑x✝
Tactic:
exact continuousAt_toComplex.continuousWithinAt
Proof state after:
no goals
Theorem: RiemannSphere.inv_zero'
Proof state before:
⊢ 0⁻¹ = ∞
Tactic:
simp only [inv_def, inv, eq_self_iff_true, if_true]
Proof state after:
no goals
Theorem: RiemannSphere.inv_inf
Proof state before:
⊢ ∞⁻¹ = 0
Tactic:
simp [inv_def, inv, inf_ne_zero]
Proof state after:
no goals
Theorem: RiemannSphere.inv_coe
Proof state before:
z : ℂ
z0 : z ≠ 0
⊢ (↑z)⁻¹ = ↑z⁻¹
Tactic:
simp only [inv_def, inv, z0, WithTop.coe_eq_zero, toComplex_coe, if_false, coe_eq_zero]
Proof state after:
no goals
Theorem: RiemannSphere.inv_eq_inf
Proof state before:
z : 𝕊
⊢ z⁻¹ = ∞ ↔ z = 0
Tactic:
induction z using OnePoint.rec
Proof state after:
case h₁

⊢ ∞⁻¹ = ∞ ↔ ∞ = 0

case h₂
x✝ : ℂ
⊢ (↑x✝)⁻¹ = ∞ ↔ ↑x✝ = 0
Theorem: RiemannSphere.inv_eq_inf
Proof state before:
case h₁

⊢ ∞⁻¹ = ∞ ↔ ∞ = 0
Tactic:
simp only [inv_inf]
Proof state after:
case h₁

⊢ 0 = ∞ ↔ ∞ = 0
Theorem: RiemannSphere.inv_eq_inf
Proof state before:
case h₁

⊢ 0 = ∞ ↔ ∞ = 0
Tactic:
exact ⟨Eq.symm, Eq.symm⟩
Proof state after:
no goals
Theorem: RiemannSphere.inv_eq_inf
Proof state before:
case h₂
x✝ : ℂ
⊢ (↑x✝)⁻¹ = ∞ ↔ ↑x✝ = 0
Tactic:
simp only [inv_def, inv, not_not, imp_false, ite_eq_left_iff, OnePoint.coe_ne_infty]
Proof state after:
no goals
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
z : 𝕊
⊢ z⁻¹ = 0 ↔ z = ∞
Tactic:
induction' z using OnePoint.rec with z
Proof state after:
case h₁

⊢ ∞⁻¹ = 0 ↔ ∞ = ∞

case h₂
z : ℂ
⊢ (↑z)⁻¹ = 0 ↔ ↑z = ∞
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
case h₁

⊢ ∞⁻¹ = 0 ↔ ∞ = ∞
Tactic:
simp only [inv_inf, eq_self_iff_true]
Proof state after:
no goals
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
case h₂
z : ℂ
⊢ (↑z)⁻¹ = 0 ↔ ↑z = ∞
Tactic:
simp only [inv_def, inv, toComplex_coe]
Proof state after:
case h₂
z : ℂ
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
case h₂
z : ℂ
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Tactic:
by_cases z0 : (z : 𝕊) = 0
Proof state after:
case pos
z : ℂ
z0 : ↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞

case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
case pos
z : ℂ
z0 : ↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞

case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Tactic:
simp only [if_pos, z0, inf_ne_zero, inf_ne_zero.symm]
Proof state after:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Tactic:
simp only [if_neg z0, coe_ne_inf, iff_false_iff]
Proof state after:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬↑z⁻¹ = 0
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬↑z⁻¹ = 0
Tactic:
rw [coe_eq_zero, _root_.inv_eq_zero]
Proof state after:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬z = 0
Theorem: RiemannSphere.inv_eq_zero
Proof state before:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬z = 0
Tactic:
simpa only [coe_eq_zero] using z0
Proof state after:
no goals
Theorem: RiemannSphere.toComplex_inv
Proof state before:
z : 𝕊
⊢ z⁻¹.toComplex = z.toComplex⁻¹
Tactic:
induction' z using OnePoint.rec with z
Proof state after:
case h₁

⊢ ∞⁻¹.toComplex = ∞.toComplex⁻¹

case h₂
z : ℂ
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Theorem: RiemannSphere.toComplex_inv
Proof state before:
case h₁

⊢ ∞⁻¹.toComplex = ∞.toComplex⁻¹
Tactic:
simp only [inv_inf, toComplex_zero, toComplex_inf, inv_zero', inv_zero, eq_self_iff_true]
Proof state after:
no goals
Theorem: RiemannSphere.toComplex_inv
Proof state before:
case h₂
z : ℂ
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
z : ℂ
z0 : z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹

case neg
z : ℂ
z0 : ¬z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Theorem: RiemannSphere.toComplex_inv
Proof state before:
case pos
z : ℂ
z0 : z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Tactic:
simp only [z0, coe_zero, inv_zero', toComplex_inf, toComplex_zero, inv_zero]
Proof state after:
no goals
Theorem: RiemannSphere.toComplex_inv
Proof state before:
case neg
z : ℂ
z0 : ¬z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Tactic:
simp only [z0, inv_coe, Ne, not_false_iff, toComplex_coe]
Proof state after:
no goals
Theorem: RiemannSphere.coe_tendsto_inf
Proof state before:
⊢ Tendsto (fun z => ↑z) atInf (𝓝 ∞)
Tactic:
rw [Filter.tendsto_iff_comap, OnePoint.comap_coe_nhds_infty, Filter.coclosedCompact_eq_cocompact]
Proof state after:
⊢ atInf ≤ Filter.cocompact ℂ
Theorem: RiemannSphere.coe_tendsto_inf
Proof state before:
⊢ atInf ≤ Filter.cocompact ℂ
Tactic:
exact atInf_le_cocompact
Proof state after:
no goals
Theorem: RiemannSphere.coe_tendsto_inf'
Proof state before:
e : {∞}ᶜ = range fun z => ↑z
⊢ Tendsto (fun z => ↑z) atInf (𝓝[≠] ∞)
Tactic:
simp only [e, tendsto_nhdsWithin_range, coe_tendsto_inf]
Proof state after:
no goals
Theorem: RiemannSphere.coe_tendsto_inf'
Proof state before:
⊢ {∞}ᶜ = range fun z => ↑z
Tactic:
ext z
Proof state after:
case h
z : 𝕊
⊢ z ∈ {∞}ᶜ ↔ z ∈ range fun z => ↑z
Theorem: RiemannSphere.coe_tendsto_inf'
Proof state before:
case h
z : 𝕊
⊢ z ∈ {∞}ᶜ ↔ z ∈ range fun z => ↑z
Tactic:
induction' z using OnePoint.rec with z
Proof state after:
case h.h₁

⊢ ∞ ∈ {∞}ᶜ ↔ ∞ ∈ range fun z => ↑z

case h.h₂
z : ℂ
⊢ ↑z ∈ {∞}ᶜ ↔ ↑z ∈ range fun z => ↑z
Theorem: RiemannSphere.coe_tendsto_inf'
Proof state before:
case h.h₁

⊢ ∞ ∈ {∞}ᶜ ↔ ∞ ∈ range fun z => ↑z
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, not_true, mem_range, OnePoint.coe_ne_infty,
  exists_false]
Proof state after:
no goals
Theorem: RiemannSphere.coe_tendsto_inf'
Proof state before:
case h.h₂
z : ℂ
⊢ ↑z ∈ {∞}ᶜ ↔ ↑z ∈ range fun z => ↑z
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, OnePoint.coe_ne_infty, not_false_eq_true,
  mem_range, coe_eq_coe, exists_eq]
Proof state after:
no goals
Theorem: RiemannSphere.continuous_inv
Proof state before:
⊢ Continuous fun z => z⁻¹
Tactic:
rw [continuous_iff_continuousOn_univ]
Proof state after:
⊢ ContinuousOn (fun z => z⁻¹) univ
Theorem: RiemannSphere.continuous_inv
Proof state before:
⊢ ContinuousOn (fun z => z⁻¹) univ
Tactic:
intro z _
Proof state after:
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousWithinAt (fun z => z⁻¹) univ z
Theorem: RiemannSphere.continuous_inv
Proof state before:
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousWithinAt (fun z => z⁻¹) univ z
Tactic:
apply ContinuousAt.continuousWithinAt
Proof state after:
case h
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) z
Theorem: RiemannSphere.continuous_inv
Proof state before:
case h
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) z
Tactic:
induction' z using OnePoint.rec with z
Proof state after:
case h.h₁
a✝ : ∞ ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ∞

case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ↑z
Theorem: RiemannSphere.continuous_inv
Proof state before:
case h.h₁
a✝ : ∞ ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ∞
Tactic:
simp only [OnePoint.continuousAt_infty', Function.comp, Filter.coclosedCompact_eq_cocompact,
  inv_inf, ← atInf_eq_cocompact]
Proof state after:
case h.h₁
a✝ : ∞ ∈ univ
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)
Theorem: RiemannSphere.continuous_inv
Proof state before:
case h.h₁
a✝ : ∞ ∈ univ
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)
Tactic:
have e : ∀ᶠ z : ℂ in atInf, ↑z⁻¹ = (↑z : 𝕊)⁻¹ := by
  refine (eventually_atInf 0).mp (eventually_of_forall fun z z0 ↦ ?_)
  simp only [gt_iff_lt, Complex.norm_eq_abs, AbsoluteValue.pos_iff] at z0; rw [inv_coe z0]
Proof state after:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)
Theorem: RiemannSphere.continuous_inv
Proof state before:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)
Tactic:
apply Filter.Tendsto.congr' e
Proof state after:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => ↑x⁻¹) atInf (𝓝 0)
Theorem: RiemannSphere.continuous_inv
Proof state before:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => ↑x⁻¹) atInf (𝓝 0)
Tactic:
exact Filter.Tendsto.comp continuous_coe.continuousAt inv_tendsto_atInf'
Proof state after:
no goals
Theorem: RiemannSphere.continuous_inv
Proof state before:
a✝ : ∞ ∈ univ
⊢ ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
Tactic:
refine (eventually_atInf 0).mp (eventually_of_forall fun z z0 ↦ ?_)
Proof state after:
a✝ : ∞ ∈ univ
z : ℂ
z0 : ‖z‖ > 0
⊢ ↑z⁻¹ = (↑z)⁻¹
Theorem: RiemannSphere.continuous_inv
Proof state before:
a✝ : ∞ ∈ univ
z : ℂ
z0 : ‖z‖ > 0
⊢ ↑z⁻¹ = (↑z)⁻¹
Tactic:
simp only [gt_iff_lt, Complex.norm_eq_abs, AbsoluteValue.pos_iff] at z0
Proof state after:
a✝ : ∞ ∈ univ
z : ℂ
z0 : z ≠ 0
⊢ ↑z⁻¹ = (↑z)⁻¹
Theorem: RiemannSphere.continuous_inv
Proof state before:
a✝ : ∞ ∈ univ
z : ℂ
z0 : z ≠ 0
⊢ ↑z⁻¹ = (↑z)⁻¹
Tactic:
rw [inv_coe z0]
Proof state after:
no goals
Theorem: RiemannSphere.continuous_inv
Proof state before:
case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ↑z
Tactic:
simp only [OnePoint.continuousAt_coe, Function.comp, inv_def, inv, WithTop.coe_eq_zero,
  toComplex_coe]
Proof state after:
case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z
Theorem: RiemannSphere.continuous_inv
Proof state before:
case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z

case neg
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z