internlm/Lean-Github huggingface dataset:
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    x ∈ t →
      Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) →
        (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
apply Filter.eventually_of_forall
Proof state after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Theorem: df_ne_zero
Proof state before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
clear small
Proof state after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Theorem: df_ne_zero
Proof state before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
intro ⟨e, w⟩ m' small
Proof state after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs ((e, w).2 * deriv (g (f (e, w).1) d) (e, w).2) < Complex.abs (↑d * g (f (e, w).1) d (e, w).2)
⊢ deriv (f (e, w).1) (e, w).2 = 0 ↔ (e, w).2 = 0
Theorem: df_ne_zero
Proof state before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs ((e, w).2 * deriv (g (f (e, w).1) d) (e, w).2) < Complex.abs (↑d * g (f (e, w).1) d (e, w).2)
⊢ deriv (f (e, w).1) (e, w).2 = 0 ↔ (e, w).2 = 0
Tactic:
simp only [df _ _ m'] at small ⊢
Proof state after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ d * deriv (g (f e) d) w = 0 ↔ w = 0
Theorem: df_ne_zero
Proof state before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ d * deriv (g (f e) d) w = 0 ↔ w = 0
Tactic:
nth_rw 4 [← Nat.sub_add_cancel (Nat.succ_le_of_lt (s.s m).dp)]
Proof state after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ (d - Nat.succ 0 + Nat.succ 0) * deriv (g (f e) d) w = 0 ↔ w = 0
Theorem: df_ne_zero
Proof state before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ (d - Nat.succ 0 + Nat.succ 0) * deriv (g (f e) d) w = 0 ↔ w = 0
Tactic:
simp only [pow_add, pow_one, mul_comm _ (w ^ (d - 1)), mul_assoc (w ^ (d - 1)) _ _, ←
  left_distrib, mul_eq_zero, pow_eq_zero_iff (Nat.sub_pos_of_lt (s.s m).d2).ne']
Proof state after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ w = 0 ∨ ↑d * g (f e) d w + w * deriv (g (f e) d) w = 0 ↔ w = 0
Theorem: df_ne_zero
Proof state before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ w = 0 ∨ ↑d * g (f e) d w + w * deriv (g (f e) d) w = 0 ↔ w = 0
Tactic:
exact or_iff_left (add_ne_zero_of_abs_lt small)
Proof state after:
no goals
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
Tactic:
intro e z m
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
Tactic:
apply HasDerivAt.deriv
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Theorem: df_ne_zero
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Tactic:
have fg : f e = fun z ↦ z ^ d * g (f e) d z := by funext; rw [(s.ts m).fg]
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Theorem: df_ne_zero
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Tactic:
nth_rw 1 [fg]
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun z => z ^ d * g (f e) d z) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Theorem: df_ne_zero
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun z => z ^ d * g (f e) d z) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Tactic:
apply HasDerivAt.mul
Proof state after:
case h.hc
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => y ^ d) (↑d * z ^ (d - 1)) z

case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z
Theorem: df_ne_zero
Proof state before:
case h.hc
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => y ^ d) (↑d * z ^ (d - 1)) z

case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z
Tactic:
apply hasDerivAt_pow
Proof state after:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z
Theorem: df_ne_zero
Proof state before:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z
Tactic:
rw [hasDerivAt_deriv_iff]
Proof state after:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ DifferentiableAt ℂ (fun y => g (f e) d y) z
Theorem: df_ne_zero
Proof state before:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ DifferentiableAt ℂ (fun y => g (f e) d y) z
Tactic:
exact ((s.ts m).ga _ m).differentiableAt
Proof state after:
no goals
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ f e = fun z => z ^ d * g (f e) d z
Tactic:
funext
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
x✝ : ℂ
⊢ f e x✝ = x✝ ^ d * g (f e) d x✝
Theorem: df_ne_zero
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
x✝ : ℂ
⊢ f e x✝ = x✝ ^ d * g (f e) d x✝
Tactic:
rw [(s.ts m).fg]
Proof state after:
no goals
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
Tactic:
have ga : AnalyticAt ℂ (uncurry fun c z ↦ g (f c) d z) (c, 0) := s.ga _ (s.s m).t0
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
Tactic:
apply ContinuousAt.eventually_lt
Proof state after:
case hf
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (x.2 * deriv (g (f x.1) d) x.2)) (c, 0)

case hg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (↑d * g (f x.1) d x.2)) (c, 0)

case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ Complex.abs ((c, 0).2 * deriv (g (f (c, 0).1) d) (c, 0).2) < Complex.abs (↑d * g (f (c, 0).1) d (c, 0).2)
Theorem: df_ne_zero
Proof state before:
case hf
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (x.2 * deriv (g (f x.1) d) x.2)) (c, 0)
Tactic:
exact Complex.continuous_abs.continuousAt.comp (continuousAt_snd.mul ga.deriv2.continuousAt)
Proof state after:
no goals
Theorem: df_ne_zero
Proof state before:
case hg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (↑d * g (f x.1) d x.2)) (c, 0)
Tactic:
exact Complex.continuous_abs.continuousAt.comp (continuousAt_const.mul ga.continuousAt)
Proof state after:
no goals
Theorem: df_ne_zero
Proof state before:
case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ Complex.abs ((c, 0).2 * deriv (g (f (c, 0).1) d) (c, 0).2) < Complex.abs (↑d * g (f (c, 0).1) d (c, 0).2)
Tactic:
simp only [g0, MulZeroClass.zero_mul, Complex.abs.map_zero, Complex.abs.map_mul,
  Complex.abs_natCast, Complex.abs.map_one, mul_one, Nat.cast_pos]
Proof state after:
case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ 0 < d
Theorem: df_ne_zero
Proof state before:
case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ 0 < d
Tactic:
exact (s.s m).dp
Proof state after:
no goals
Theorem: mem_analyticGroupoid
Proof state before:
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E A : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : TopologicalSpace A
I : ModelWithCorners 𝕜 E A
f : PartialHomeomorph A A
⊢ f ∈ analyticGroupoid I ↔
    f ∈ contDiffGroupoid ⊤ I ∧
      (AnalyticOn 𝕜 (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
          ↑I ∘ ↑f ∘ ↑I.symm '' (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ⊆ interior (range ↑I)) ∧
        AnalyticOn 𝕜 (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
          ↑I ∘ ↑f.symm ∘ ↑I.symm '' (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ⊆ interior (range ↑I)
Tactic:
rfl
Proof state after:
no goals
Theorem: analyticGroupoid_prod
Proof state before:
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Tactic:
have er : (range fun x : A × B ↦ (I x.1, J x.2)) = range I ×ˢ range J := range_prod_map
Proof state after:
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Theorem: analyticGroupoid_prod
Proof state before:
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Tactic:
have ei : interior (range fun x : A × B ↦ (I x.1, J x.2)) =
    interior (range I) ×ˢ interior (range J) := by rw [er, interior_prod_eq]
Proof state after:
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Theorem: analyticGroupoid_prod
Proof state before:
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Tactic:
simp only [mem_analyticGroupoid, Function.comp, image_subset_iff] at fa ga ⊢
Proof state after:
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
⊢ f.prod g ∈ contDiffGroupoid ⊤ (I.prod J) ∧
    (AnalyticOn 𝕜 (fun x => ↑(I.prod J) (↑(f.prod g) (↑(I.prod J).symm x)))
          (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J))) ∧
        ↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J)) ⊆
          (fun x => ↑(I.prod J) (↑(f.prod g) (↑(I.prod J).symm x))) ⁻¹' interior (range ↑(I.prod J))) ∧
      AnalyticOn 𝕜 (fun x => ↑(I.prod J) (↑(f.prod g).symm (↑(I.prod J).symm x)))
          (↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ interior (range ↑(I.prod J))) ∧
        ↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ interior (range ↑(I.prod J)) ⊆
          (fun x => ↑(I.prod J) (↑(f.prod g).symm (↑(I.prod J).symm x))) ⁻¹' interior (range ↑(I.prod J))
Theorem: analyticGroupoid_prod
Proof state before:
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
⊢ interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
Tactic:
rw [er, interior_prod_eq]
Proof state after:
no goals
Theorem: analyticGroupoid_prod
Proof state before:
case refine_1.hf
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
x : E × F
m : (↑I.symm x.1 ∈ f.source ∧ ↑J.symm x.2 ∈ g.source) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑I.symm x.1 ∈ f.source ∧ x.1 ∈ interior (range ↑I)
Tactic:
exact ⟨m.1.1, (subset_of_eq ei m.2).1⟩
Proof state after:
no goals