internlm/Lean-Github huggingface dataset:
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ ↑(extChartAt I z).symm x ∈ (extChartAt I z).source
Tactic:
exact PartialEquiv.map_target _ m
Proof state after:
no goals
Theorem: IsPreconnected.open_diff_line
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ IsPreconnected (s \ {p | p.2 = a})
Tactic:
apply IsPreconnected.open_diff sc so
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ Nonseparating {p | p.2 = a}
Theorem: IsPreconnected.open_diff_line
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ Nonseparating {p | p.2 = a}
Tactic:
have e : {p : ℂ × S | p.2 = a} = univ ×ˢ {a} := by
  apply Set.ext; intro ⟨c, z⟩
  simp only [mem_prod_eq, mem_setOf, mem_univ, true_and_iff, mem_singleton_iff]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating {p | p.2 = a}
Theorem: IsPreconnected.open_diff_line
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating {p | p.2 = a}
Tactic:
rw [e]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating (univ ×ˢ {a})
Theorem: IsPreconnected.open_diff_line
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
e : {p | p.2 = a} = univ ×ˢ {a}
⊢ Nonseparating (univ ×ˢ {a})
Tactic:
exact Nonseparating.univ_prod (AnalyticManifold.nonseparating_singleton _)
Proof state after:
no goals
Theorem: IsPreconnected.open_diff_line
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ {p | p.2 = a} = univ ×ˢ {a}
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ ∀ (x : ℂ × S), x ∈ {p | p.2 = a} ↔ x ∈ univ ×ˢ {a}
Theorem: IsPreconnected.open_diff_line
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
⊢ ∀ (x : ℂ × S), x ∈ {p | p.2 = a} ↔ x ∈ univ ×ˢ {a}
Tactic:
intro ⟨c, z⟩
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
c : ℂ
z : S
⊢ (c, z) ∈ {p | p.2 = a} ↔ (c, z) ∈ univ ×ˢ {a}
Theorem: IsPreconnected.open_diff_line
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s : Set (ℂ × S)
sc : IsPreconnected s
so : IsOpen s
a : S
c : ℂ
z : S
⊢ (c, z) ∈ {p | p.2 = a} ↔ (c, z) ∈ univ ×ˢ {a}
Tactic:
simp only [mem_prod_eq, mem_setOf, mem_univ, true_and_iff, mem_singleton_iff]
Proof state after:
no goals
Theorem: realCircleMap_eq_circleMap
Proof state before:
c : ℂ
x : ℝ × ℝ
⊢ realCircleMap c x = Complex.equivRealProd (circleMap c x.1 x.2)
Tactic:
simp only [realCircleMap, circleMap, Complex.equivRealProd_apply, Complex.add_re, Complex.mul_re,
  Complex.ofReal_re, Complex.exp_ofReal_mul_I_re, Complex.ofReal_im, Complex.exp_ofReal_mul_I_im,
  zero_mul, sub_zero, Complex.add_im, Complex.mul_im, add_zero]
Proof state after:
no goals
Theorem: realCircleMap.fderiv
Proof state before:
c : ℂ
x : ℝ × ℝ
⊢ HasFDerivAt (fun x => realCircleMap c x) (rcmDeriv x) x
Tactic:
simp_rw [realCircleMap]
Proof state after:
c : ℂ
x : ℝ × ℝ
⊢ HasFDerivAt (fun x => (c.re + x.1 * x.2.cos, c.im + x.1 * x.2.sin)) (rcmDeriv x) x
Theorem: realCircleMap.fderiv
Proof state before:
c : ℂ
x : ℝ × ℝ
⊢ HasFDerivAt (fun x => (c.re + x.1 * x.2.cos, c.im + x.1 * x.2.sin)) (rcmDeriv x) x
Tactic:
apply_rules [hasFDerivAt_const, hasFDerivAt_fst, hasFDerivAt_snd, HasFDerivAt.cos,
  HasFDerivAt.sin, HasFDerivAt.add, HasFDerivAt.mul, HasFDerivAt.prod]
Proof state after:
no goals
Theorem: rcm00
Proof state before:
x : ℝ × ℝ
⊢ rcmMatrix x 0 0 = x.2.cos
Tactic:
simp [rcmMatrix, rcmDeriv, toMatrix_apply, d1, d2]
Proof state after:
no goals
Theorem: rcm01
Proof state before:
x : ℝ × ℝ
⊢ rcmMatrix x 0 1 = -x.1 * x.2.sin
Tactic:
simp [rcmMatrix, rcmDeriv, toMatrix_apply, d1, d2]
Proof state after:
no goals
Theorem: rcm10
Proof state before:
x : ℝ × ℝ
⊢ rcmMatrix x 1 0 = x.2.sin
Tactic:
simp [rcmMatrix, rcmDeriv, toMatrix_apply, d1, d2]
Proof state after:
no goals
Theorem: rcm11
Proof state before:
x : ℝ × ℝ
⊢ rcmMatrix x 1 1 = x.1 * x.2.cos
Tactic:
simp [rcmMatrix, rcmDeriv, toMatrix_apply, d1, d2]
Proof state after:
no goals
Theorem: rcmDeriv.det
Proof state before:
x : ℝ × ℝ
⊢ (rcmDeriv x).det = x.1
Tactic:
rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (Basis.finTwoProd ℝ), ←rcmMatrix]
Proof state after:
x : ℝ × ℝ
⊢ (rcmMatrix x).det = x.1
Theorem: rcmDeriv.det
Proof state before:
x : ℝ × ℝ
⊢ (rcmMatrix x).det = x.1
Tactic:
rw [Matrix.det_fin_two, rcm00, rcm01, rcm10, rcm11]
Proof state after:
x : ℝ × ℝ
⊢ x.2.cos * (x.1 * x.2.cos) - -x.1 * x.2.sin * x.2.sin = x.1
Theorem: rcmDeriv.det
Proof state before:
x : ℝ × ℝ
⊢ x.2.cos * (x.1 * x.2.cos) - -x.1 * x.2.sin * x.2.sin = x.1
Tactic:
ring_nf
Proof state after:
x : ℝ × ℝ
⊢ x.2.cos ^ 2 * x.1 + x.1 * x.2.sin ^ 2 = x.1
Theorem: rcmDeriv.det
Proof state before:
x : ℝ × ℝ
⊢ x.2.cos ^ 2 * x.1 + x.1 * x.2.sin ^ 2 = x.1
Tactic:
calc cos x.2 ^ 2 * x.1 + x.1 * sin x.2 ^ 2
  _ = x.1 * (cos x.2 ^ 2 + sin x.2 ^ 2) := by ring
  _ = x.1 := by simp only [Real.cos_sq_add_sin_sq, mul_one]
Proof state after:
no goals
Theorem: rcmDeriv.det
Proof state before:
x : ℝ × ℝ
⊢ x.2.cos ^ 2 * x.1 + x.1 * x.2.sin ^ 2 = x.1 * (x.2.cos ^ 2 + x.2.sin ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: rcmDeriv.det
Proof state before:
x : ℝ × ℝ
⊢ x.1 * (x.2.cos ^ 2 + x.2.sin ^ 2) = x.1
Tactic:
simp only [Real.cos_sq_add_sin_sq, mul_one]
Proof state after:
no goals
Theorem: Metric.sphere_eq_empty
Proof state before:
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ sphere c r = ∅ ↔ r < 0
Tactic:
constructor
Proof state after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ sphere c r = ∅ → r < 0

case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ r < 0 → sphere c r = ∅
Theorem: Metric.sphere_eq_empty
Proof state before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ sphere c r = ∅ → r < 0
Tactic:
intro rp
Proof state after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : sphere c r = ∅
⊢ r < 0
Theorem: Metric.sphere_eq_empty
Proof state before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : sphere c r = ∅
⊢ r < 0
Tactic:
contrapose rp
Proof state after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : ¬r < 0
⊢ ¬sphere c r = ∅
Theorem: Metric.sphere_eq_empty
Proof state before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : ¬r < 0
⊢ ¬sphere c r = ∅
Tactic:
simp at rp
Proof state after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ ¬sphere c r = ∅
Theorem: Metric.sphere_eq_empty
Proof state before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ ¬sphere c r = ∅
Tactic:
refine Nonempty.ne_empty ⟨c + r, ?_⟩
Proof state after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ c + ↑r ∈ sphere c r
Theorem: Metric.sphere_eq_empty
Proof state before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ c + ↑r ∈ sphere c r
Tactic:
simpa only [mem_sphere_iff_norm, add_sub_cancel_left, RCLike.norm_ofReal, abs_eq_self]
Proof state after:
no goals
Theorem: Metric.sphere_eq_empty
Proof state before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ r < 0 → sphere c r = ∅
Tactic:
intro n
Proof state after:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : r < 0
⊢ sphere c r = ∅
Theorem: Metric.sphere_eq_empty
Proof state before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : r < 0
⊢ sphere c r = ∅
Tactic:
contrapose n
Proof state after:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬sphere c r = ∅
⊢ ¬r < 0
Theorem: Metric.sphere_eq_empty
Proof state before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬sphere c r = ∅
⊢ ¬r < 0
Tactic:
rw [← not_nonempty_iff_eq_empty] at n
Proof state after:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬¬(sphere c r).Nonempty
⊢ ¬r < 0
Theorem: Metric.sphere_eq_empty
Proof state before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬¬(sphere c r).Nonempty
⊢ ¬r < 0
Tactic:
simpa only [not_lt, NormedSpace.sphere_nonempty, not_le] using n
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
by_cases rp : r < 0
Proof state after:
case pos
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t

case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : ¬r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Theorem: circleMap_Ioc
Proof state before:
case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : ¬r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
simp only [not_lt] at rp
Proof state after:
case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Theorem: circleMap_Ioc
Proof state before:
case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
rw [←abs_of_nonneg rp, ← range_circleMap, mem_range] at zs
Proof state after:
case neg
c z : ℂ
r : ℝ
zs : ∃ y, circleMap c r y = z
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Theorem: circleMap_Ioc
Proof state before:
case neg
c z : ℂ
r : ℝ
zs : ∃ y, circleMap c r y = z
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
rcases zs with ⟨t, ht⟩
Proof state after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Theorem: circleMap_Ioc
Proof state before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
generalize ha : 2 * π = a
Proof state after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Theorem: circleMap_Ioc
Proof state before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Tactic:
have ap : a > 0 := by rw [←ha]; bound
Proof state after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Theorem: circleMap_Ioc
Proof state before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Tactic:
generalize hs : t + a - a * ⌈t / a⌉ = s
Proof state after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Theorem: circleMap_Ioc
Proof state before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Tactic:
use s
Proof state after:
case h
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a ∧ z = circleMap c r s
Theorem: circleMap_Ioc
Proof state before:
case h
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a ∧ z = circleMap c r s
Tactic:
constructor
Proof state after:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a

case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ z = circleMap c r s
Theorem: circleMap_Ioc
Proof state before:
case pos
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
simp only [Metric.sphere_eq_empty.mpr rp, mem_empty_iff_false] at zs
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ a > 0
Tactic:
rw [←ha]
Proof state after:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ 2 * π > 0
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ 2 * π > 0
Tactic:
bound
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a
Tactic:
simp only [mem_Ioc, sub_pos, tsub_le_iff_right, ← hs]
Proof state after:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a ∧ t + a ≤ a + a * ↑⌈t / a⌉
Theorem: circleMap_Ioc
Proof state before:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a ∧ t + a ≤ a + a * ↑⌈t / a⌉
Tactic:
constructor
Proof state after:
case h.left.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a

case h.left.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ t + a ≤ a + a * ↑⌈t / a⌉
Theorem: circleMap_Ioc
Proof state before:
case h.left.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a
Tactic:
calc a * ⌈t / a⌉
  _ < a * (t / a + 1) := by bound
  _ = a / a * t + a := by ring
  _ = t + a := by field_simp [ap.ne']
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < a * (t / a + 1)
Tactic:
bound
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * (t / a + 1) = a / a * t + a
Tactic:
ring
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a / a * t + a = t + a
Tactic:
field_simp [ap.ne']
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
case h.left.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ t + a ≤ a + a * ↑⌈t / a⌉
Tactic:
calc a + a * ⌈t / a⌉
  _ ≥ a + a * (t / a) := by bound
  _ = a / a * t + a := by ring
  _ = t + a := by field_simp [ap.ne']
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a + a * ↑⌈t / a⌉ ≥ a + a * (t / a)
Tactic:
bound
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a + a * (t / a) = a / a * t + a
Tactic:
ring
Proof state after:
no goals
Theorem: circleMap_Ioc
Proof state before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ z = circleMap c r s
Tactic:
simp only [←ht, circleMap, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_mul,
  Complex.ofReal_intCast, add_right_inj, mul_eq_mul_left_iff, Complex.ofReal_eq_zero, ← hs]
Proof state after:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = ((↑t + ↑a - ↑a * ↑⌈t / a⌉) * I).exp ∨ r = 0
Theorem: circleMap_Ioc
Proof state before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = ((↑t + ↑a - ↑a * ↑⌈t / a⌉) * I).exp ∨ r = 0
Tactic:
rw [mul_sub_right_distrib, right_distrib, Complex.exp_sub, Complex.exp_add]
Proof state after:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑a * I).exp / (↑a * ↑⌈t / a⌉ * I).exp ∨ r = 0
Theorem: circleMap_Ioc
Proof state before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑a * I).exp / (↑a * ↑⌈t / a⌉ * I).exp ∨ r = 0
Tactic:
rw [mul_comm _ (⌈_⌉:ℂ), mul_assoc, Complex.exp_int_mul, ← ha]
Proof state after:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑(2 * π) * I).exp / (↑(2 * π) * I).exp ^ ⌈t / (2 * π)⌉ ∨ r = 0
Theorem: circleMap_Ioc
Proof state before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑(2 * π) * I).exp / (↑(2 * π) * I).exp ^ ⌈t / (2 * π)⌉ ∨ r = 0
Tactic:
simp only [Complex.ofReal_mul, Complex.ofReal_ofNat, Complex.exp_two_pi_mul_I, mul_one,
  one_zpow, div_one, true_or]
Proof state after:
no goals
Theorem: square.rp
Proof state before:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
⊢ x ∈ square r0 r1 → 0 < x.1
Tactic:
simp only [square, gt_iff_lt, not_lt, ge_iff_le, zero_lt_two, mul_pos_iff_of_pos_left,
  mem_prod, mem_Ioc, and_imp]
Proof state after:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
⊢ r0 < x.1 → x.1 ≤ r1 → 0 < x.2 → x.2 ≤ 2 * π → 0 < x.1
Theorem: square.rp
Proof state before:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
⊢ r0 < x.1 → x.1 ≤ r1 → 0 < x.2 → x.2 ≤ 2 * π → 0 < x.1
Tactic:
intro h _ _ _
Proof state after:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
h : r0 < x.1
a✝² : x.1 ≤ r1
a✝¹ : 0 < x.2
a✝ : x.2 ≤ 2 * π
⊢ 0 < x.1
Theorem: square.rp
Proof state before:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
h : r0 < x.1
a✝² : x.1 ≤ r1
a✝¹ : 0 < x.2
a✝ : x.2 ≤ 2 * π
⊢ 0 < x.1
Tactic:
linarith
Proof state after:
no goals
Theorem: Measurable.square
Proof state before:
r0 r1 : ℝ
⊢ MeasurableSet (_root_.square r0 r1)
Tactic:
apply_rules [MeasurableSet.prod, measurableSet_Ioc]
Proof state after:
no goals
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ ⇑Complex.measurableEquivRealProd.symm ⁻¹' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
rw [← MeasurableEquiv.image_eq_preimage]
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
have e : realCircleMap c =
    fun x : ℝ × ℝ ↦ Complex.measurableEquivRealProd (circleMap c x.1 x.2) := by
  funext
  simp only [realCircleMap_eq_circleMap, Complex.measurableEquivRealProd,
    Complex.equivRealProd_apply, Homeomorph.toMeasurableEquiv_coe,
    ContinuousLinearEquiv.coe_toHomeomorph, Complex.equivRealProdCLM_apply]
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
have im := image_comp Complex.measurableEquivRealProd (fun x : ℝ × ℝ ↦ circleMap c x.1 x.2)
  (square r0 r1)
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (⇑Complex.measurableEquivRealProd ∘ fun x => circleMap c x.1 x.2) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (⇑Complex.measurableEquivRealProd ∘ fun x => circleMap c x.1 x.2) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
simp only [Function.comp] at im
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (fun a => Complex.measurableEquivRealProd (circleMap c a.1 a.2)) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (fun a => Complex.measurableEquivRealProd (circleMap c a.1 a.2)) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
simp only [e, im, i]
Proof state after:
no goals
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
Tactic:
funext
Proof state after:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x✝ : ℝ × ℝ
⊢ realCircleMap c x✝ = Complex.measurableEquivRealProd (circleMap c x✝.1 x✝.2)