Theorem: SuperNearC.union (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
⊢ SuperNearC f d (⋃ i, u i) (⋃ i, t i)
Tactic:
set tu := ⋃ i, t i
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
⊢ SuperNearC f d (⋃ i, u i) tu

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
⊢ SuperNearC f d (⋃ i, u i) tu
Tactic:
have o : IsOpen tu := isOpen_iUnion fun i ↦ (s i).o
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
⊢ SuperNearC f d (⋃ i, u i) tu

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
⊢ SuperNearC f d (⋃ i, u i) tu
Tactic:
exact
  { o
    tc := by
      intro p m; rcases Set.mem_iUnion.mp m with ⟨i, m⟩
      exact Set.subset_iUnion _ i ((s i).tc m)
    fa := by intro p m; rcases Set.mem_iUnion.mp m with ⟨i, m⟩; exact (s i).fa _ m
    s := by
      intro c m; rcases Set.mem_iUnion.mp m with ⟨i, m⟩; have s := (s i).s m
      exact
        { d2 := s.d2
          fa0 := s.fa0
          fd := s.fd
          fc := s.fc
          o := o.snd_preimage c
          t0 := Set.subset_iUnion _ i s.t0
          t2 := by intro z m; rcases sm m with ⟨u, m, _, s⟩; exact s.t2 m
          fa := by intro z m; rcases sm m with ⟨u, m, _, s⟩; exact s.fa _ m
          ft := by intro z m; rcases sm m with ⟨u, m, us, s⟩; exact us (s.ft m)
          gs' := by intro z z0 m; rcases sm m with ⟨u, m, _, s⟩; exact s.gs' z0 m } }
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
⊢ ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
Tactic:
intro c z m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m : (c, z) ∈ tu
⊢ ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m : (c, z) ∈ tu
⊢ ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
Tactic:
rcases Set.mem_iUnion.mp m with ⟨i, m⟩
State after:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u

State before:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
Tactic:
use{z | (c, z) ∈ t i}
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ z ∈ {z | (c, z) ∈ t i} ∧ {z | (c, z) ∈ t i} ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d {z | (c, z) ∈ t i}

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ z ∈ {z | (c, z) ∈ t i} ∧ {z | (c, z) ∈ t i} ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d {z | (c, z) ∈ t i}
Tactic:
simp only [Set.mem_setOf_eq, m, Set.mem_iUnion, Set.setOf_subset_setOf, true_and, tu]
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ (∀ (a : ℂ), (c, a) ∈ t i → ∃ i, (c, a) ∈ t i) ∧ SuperNear (f c) d {z | (c, z) ∈ t i}

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ (∀ (a : ℂ), (c, a) ∈ t i → ∃ i, (c, a) ∈ t i) ∧ SuperNear (f c) d {z | (c, z) ∈ t i}
Tactic:
constructor
State after:
case h.left
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ ∀ (a : ℂ), (c, a) ∈ t i → ∃ i, (c, a) ∈ t i

case h.right
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ SuperNear (f c) d {z | (c, z) ∈ t i}

State before:
case h.left
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ ∀ (a : ℂ), (c, a) ∈ t i → ∃ i, (c, a) ∈ t i
Tactic:
exact fun z m ↦ ⟨i, m⟩
State after:
no goals

State before:
case h.right
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
c z : ℂ
m✝ : (c, z) ∈ tu
i : I
m : (c, z) ∈ t i
⊢ SuperNear (f c) d {z | (c, z) ∈ t i}
Tactic:
exact (s i).s ((s i).tc m)
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
⊢ ∀ {p : ℂ × ℂ}, p ∈ tu → p.1 ∈ ⋃ i, u i
Tactic:
intro p m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m : p ∈ tu
⊢ p.1 ∈ ⋃ i, u i

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m : p ∈ tu
⊢ p.1 ∈ ⋃ i, u i
Tactic:
rcases Set.mem_iUnion.mp m with ⟨i, m⟩
State after:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m✝ : p ∈ tu
i : I
m : p ∈ t i
⊢ p.1 ∈ ⋃ i, u i

State before:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m✝ : p ∈ tu
i : I
m : p ∈ t i
⊢ p.1 ∈ ⋃ i, u i
Tactic:
exact Set.subset_iUnion _ i ((s i).tc m)
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
⊢ AnalyticOn ℂ (uncurry f) tu
Tactic:
intro p m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m : p ∈ tu
⊢ AnalyticAt ℂ (uncurry f) p

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m : p ∈ tu
⊢ AnalyticAt ℂ (uncurry f) p
Tactic:
rcases Set.mem_iUnion.mp m with ⟨i, m⟩
State after:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m✝ : p ∈ tu
i : I
m : p ∈ t i
⊢ AnalyticAt ℂ (uncurry f) p

State before:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
p : ℂ × ℂ
m✝ : p ∈ tu
i : I
m : p ∈ t i
⊢ AnalyticAt ℂ (uncurry f) p
Tactic:
exact (s i).fa _ m
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
⊢ ∀ {c : ℂ}, c ∈ ⋃ i, u i → SuperNear (f c) d {z | (c, z) ∈ tu}
Tactic:
intro c m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m : c ∈ ⋃ i, u i
⊢ SuperNear (f c) d {z | (c, z) ∈ tu}

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m : c ∈ ⋃ i, u i
⊢ SuperNear (f c) d {z | (c, z) ∈ tu}
Tactic:
rcases Set.mem_iUnion.mp m with ⟨i, m⟩
State after:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
⊢ SuperNear (f c) d {z | (c, z) ∈ tu}

State before:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
⊢ SuperNear (f c) d {z | (c, z) ∈ tu}
Tactic:
have s := (s i).s m
State after:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
⊢ SuperNear (f c) d {z | (c, z) ∈ tu}

State before:
case intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
⊢ SuperNear (f c) d {z | (c, z) ∈ tu}
Tactic:
exact
  { d2 := s.d2
    fa0 := s.fa0
    fd := s.fd
    fc := s.fc
    o := o.snd_preimage c
    t0 := Set.subset_iUnion _ i s.t0
    t2 := by intro z m; rcases sm m with ⟨u, m, _, s⟩; exact s.t2 m
    fa := by intro z m; rcases sm m with ⟨u, m, _, s⟩; exact s.fa _ m
    ft := by intro z m; rcases sm m with ⟨u, m, us, s⟩; exact us (s.ft m)
    gs' := by intro z z0 m; rcases sm m with ⟨u, m, _, s⟩; exact s.gs' z0 m }
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
⊢ ∀ {z : ℂ}, z ∈ {z | (c, z) ∈ tu} → Complex.abs z ≤ 1 / 2
Tactic:
intro z m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m : z ∈ {z | (c, z) ∈ tu}
⊢ Complex.abs z ≤ 1 / 2

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m : z ∈ {z | (c, z) ∈ tu}
⊢ Complex.abs z ≤ 1 / 2
Tactic:
rcases sm m with ⟨u, m, _, s⟩
State after:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ Complex.abs z ≤ 1 / 2

State before:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ Complex.abs z ≤ 1 / 2
Tactic:
exact s.t2 m
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
⊢ AnalyticOn ℂ (f c) {z | (c, z) ∈ tu}
Tactic:
intro z m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m : z ∈ {z | (c, z) ∈ tu}
⊢ AnalyticAt ℂ (f c) z

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m : z ∈ {z | (c, z) ∈ tu}
⊢ AnalyticAt ℂ (f c) z
Tactic:
rcases sm m with ⟨u, m, _, s⟩
State after:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ AnalyticAt ℂ (f c) z

State before:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ AnalyticAt ℂ (f c) z
Tactic:
exact s.fa _ m
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
⊢ MapsTo (f c) {z | (c, z) ∈ tu} {z | (c, z) ∈ tu}
Tactic:
intro z m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m : z ∈ {z | (c, z) ∈ tu}
⊢ f c z ∈ {z | (c, z) ∈ tu}

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m : z ∈ {z | (c, z) ∈ tu}
⊢ f c z ∈ {z | (c, z) ∈ tu}
Tactic:
rcases sm m with ⟨u, m, us, s⟩
State after:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
us : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ f c z ∈ {z | (c, z) ∈ tu}

State before:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
us : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ f c z ∈ {z | (c, z) ∈ tu}
Tactic:
exact us (s.ft m)
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
⊢ ∀ {z : ℂ}, z ≠ 0 → z ∈ {z | (c, z) ∈ tu} → Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Tactic:
intro z z0 m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m : z ∈ {z | (c, z) ∈ tu}
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m : z ∈ {z | (c, z) ∈ tu}
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Tactic:
rcases sm m with ⟨u, m, _, s⟩
State after:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4

State before:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Tactic:
exact s.gs' z0 m
State after:
no goals