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

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ ∀ {c : ℂ}, c ∈ u → SuperAt (f c) d
Tactic:
intro c m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ SuperAt (f c) d

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ SuperAt (f c) d
Tactic:
have s := s.s m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s✝ : SuperNearC f d u t
c : ℂ
m : c ∈ u
s : SuperNear (f c) d {z | (c, z) ∈ t}
⊢ SuperAt (f c) d

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s✝ : SuperNearC f d u t
c : ℂ
m : c ∈ u
s : SuperNear (f c) d {z | (c, z) ∈ t}
⊢ SuperAt (f c) d
Tactic:
exact
  { d2 := s.d2
    fa0 := s.fa0
    fd := s.fd
    fc := s.fc }
State after:
no goals