internlm/Lean-Github huggingface dataset:
Theorem: SuperAtC.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z / z ^ d) c
Tactic:
refine AnalyticAt.div ?_ analyticAt_const (pow_ne_zero _ zero)
Proof state after:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z) c
Theorem: SuperAtC.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z) c
Tactic:
refine (fa _ ?_).comp₂ (analyticAt_id _ _) analyticAt_const
Proof state after:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ (c, z) ∈ t
Theorem: SuperAtC.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ (c, z) ∈ t
Tactic:
exact m
Proof state after:
no goals
Theorem: SuperAtC.ga_of_fa
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z1 => g2 f d (c0, z1)) c1
Tactic:
intro c z m
Proof state after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => g2 f d (c, z1)) z
Theorem: SuperAtC.ga_of_fa
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => g2 f d (c, z1)) z
Tactic:
apply (s.s (tc m)).ga_of_fa
Proof state after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (f (c, z).1) z
Theorem: SuperAtC.ga_of_fa
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (f (c, z).1) z
Tactic:
refine (fa _ ?_).comp₂ analyticAt_const (analyticAt_id _ _)
Proof state after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ (c, id z) ∈ t
Theorem: SuperAtC.ga_of_fa
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ (c, id z) ∈ t
Tactic:
exact m
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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
Theorem: SuperNearC.union
Proof 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
Proof 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
Theorem: SuperNearC.union
Proof 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 } }
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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
Theorem: SuperNearC.union
Proof 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⟩
Proof 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
Theorem: SuperNearC.union
Proof 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}
Proof 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}
Theorem: SuperNearC.union
Proof 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]
Proof 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}
Theorem: SuperNearC.union
Proof 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
Proof 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}
Theorem: SuperNearC.union
Proof 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⟩
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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)
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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
Theorem: SuperNearC.union
Proof 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⟩
Proof 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
Theorem: SuperNearC.union
Proof 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)
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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
Theorem: SuperNearC.union
Proof 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⟩
Proof 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
Theorem: SuperNearC.union
Proof 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
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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}
Theorem: SuperNearC.union
Proof 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⟩
Proof 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}
Theorem: SuperNearC.union
Proof 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
Proof 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}
Theorem: SuperNearC.union
Proof 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 }
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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
Theorem: SuperNearC.union
Proof 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⟩
Proof 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
Theorem: SuperNearC.union
Proof 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
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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
Theorem: SuperNearC.union
Proof 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⟩
Proof 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
Theorem: SuperNearC.union
Proof 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
Proof state after:
no goals
Theorem: SuperNearC.union
Proof 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
Proof 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}
Theorem: SuperNearC.union
Proof 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⟩
Proof 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}