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

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ IsOpen u
Tactic:
have e : u = Prod.fst '' t := by
  ext c; simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
  exact ⟨fun m ↦ ⟨0, (s.s m).t0⟩, fun h ↦ Exists.elim h fun z m ↦ s.tc m⟩
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen u

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen u
Tactic:
rw [e]
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen (Prod.fst '' t)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen (Prod.fst '' t)
Tactic:
exact isOpenMap_fst _ s.o
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ u = Prod.fst '' t
Tactic:
ext c
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ c ∈ Prod.fst '' t

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ c ∈ Prod.fst '' t
Tactic:
simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ ∃ x, (c, x) ∈ t

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ ∃ x, (c, x) ∈ t
Tactic:
exact ⟨fun m ↦ ⟨0, (s.s m).t0⟩, fun h ↦ Exists.elim h fun z m ↦ s.tc m⟩
State after:
no goals