internlm/Lean-Github huggingface dataset:
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
hh : a < u ∧ u ≤ t
⊢ (a < u ∧ u ≤ b ∨ b < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = b)
Tactic:
push_neg at hu ⊢
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ (a < u ∧ u ≤ b ∨ b < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ b
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ (a < u ∧ u ≤ b ∨ b < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ b
Tactic:
refine ⟨Or.inl ⟨hh.1, hh.2.trans ht.2⟩, hu.2.1, ?_⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ u ≠ b
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ u ≠ b
Tactic:
intro hub
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
hub : u = b
⊢ False
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
hub : u = b
⊢ False
Tactic:
subst_vars
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
h : ContDiffOn ℝ 1 f (Icc a u)
hab : a ≤ u
ht : t ∈ Icc a u
l1 : Icc a t ⊆ Icc a u
⊢ False
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
h : ContDiffOn ℝ 1 f (Icc a u)
hab : a ≤ u
ht : t ∈ Icc a u
l1 : Icc a t ⊆ Icc a u
⊢ False
Tactic:
cases hu.2.2 (le_antisymm hh.2 ht.2)
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
hh : t < u ∧ u ≤ a
⊢ u ∈ Ι a b \ {a, b}
Tactic:
case inr hh => linarith [ht.1]
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
hh : t < u ∧ u ≤ a
⊢ u ∈ Ι a b \ {a, b}
Tactic:
linarith [ht.1]
Proof state after:
no goals
Theorem: List.Sorted.toFinset_sort
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
α : Type u_4
inst✝ : LinearOrder α
l l1 l2 : List α
s : Finset α
hl : Sorted (fun x x_1 => x < x_1) l
⊢ ∀ (x : α), x ∈ Finset.sort (fun x x_1 => x ≤ x_1) (toFinset l) ↔ x ∈ l
Tactic:
simp
Proof state after:
no goals
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ EqOn f 0 U
Tactic:
apply (hf.analyticOn hU).eqOn_zero_of_preconnected_of_eventuallyEq_zero hU' hz₀
Proof state after:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ f =ᶠ[𝓝 z₀] 0
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ f =ᶠ[𝓝 z₀] 0
Tactic:
obtain ⟨r, hr, hrU⟩ := nhds_basis_ball.mem_iff.1 (hU.mem_nhds hz₀)
Proof state after:
case intro.intro
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
⊢ f =ᶠ[𝓝 z₀] 0
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
⊢ f =ᶠ[𝓝 z₀] 0
Tactic:
refine eventually_nhds_iff.2 ⟨r, hr, λ z hz => ?_⟩
Proof state after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = 0 z
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = 0 z
Tactic:
rw [Pi.zero_apply, ← hfz₀]
Proof state after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = f z₀
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = f z₀
Tactic:
suffices h : ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
  by exact (convex_ball z₀ r).is_const_of_fderivWithin_eq_zero (hf.mono hrU) h hz (mem_ball_self hr)
Proof state after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
Tactic:
rintro w hw
Proof state after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
⊢ fderivWithin ℂ f (ball z₀ r) w = 0
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
⊢ fderivWithin ℂ f (ball z₀ r) w = 0
Tactic:
have : UniqueDiffWithinAt ℂ (ball z₀ r) w := isOpen_ball.uniqueDiffWithinAt hw
Proof state after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderivWithin ℂ f (ball z₀ r) w = 0
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderivWithin ℂ f (ball z₀ r) w = 0
Tactic:
rw [fderivWithin_eq_fderiv this (hf.differentiableAt (hU.mem_nhds (hrU hw)))]
Proof state after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderiv ℂ f w = 0
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderiv ℂ f w = 0
Tactic:
ext1
Proof state after:
case intro.intro.h
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ (fderiv ℂ f w) 1 = 0 1
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
case intro.intro.h
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ (fderiv ℂ f w) 1 = 0 1
Tactic:
simpa [fderiv_deriv] using hf' (hrU hw)
Proof state after:
no goals
Theorem: EqOn_zero_of_deriv_eq_zero
Proof state before:
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
h : ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
⊢ f z = f z₀
Tactic:
exact (convex_ball z₀ r).is_const_of_fderivWithin_eq_zero (hf.mono hrU) h hz (mem_ball_self hr)
Proof state after:
no goals
Theorem: EqOn_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
⊢ EqOn f (fun x => f z₀) U
Tactic:
set g := λ z => f z - f z₀
Proof state after:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
⊢ EqOn f (fun x => f z₀) U
Theorem: EqOn_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
⊢ EqOn f (fun x => f z₀) U
Tactic:
have h2 : EqOn (deriv g) 0 U := λ z hz => by rw [deriv_sub_const, hf' hz]
Proof state after:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
⊢ EqOn f (fun x => f z₀) U
Theorem: EqOn_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
⊢ EqOn f (fun x => f z₀) U
Tactic:
have h3 : g z₀ = 0 := by simp [g]
Proof state after:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
⊢ EqOn f (fun x => f z₀) U
Theorem: EqOn_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
⊢ EqOn f (fun x => f z₀) U
Tactic:
have := EqOn_zero_of_deriv_eq_zero hU hU' (hf.sub_const _) h2 hz₀ h3
Proof state after:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
this : EqOn (fun y => f y - f z₀) 0 U
⊢ EqOn f (fun x => f z₀) U
Theorem: EqOn_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
this : EqOn (fun y => f y - f z₀) 0 U
⊢ EqOn f (fun x => f z₀) U
Tactic:
exact λ z hz => sub_eq_zero.1 (this hz)
Proof state after:
no goals
Theorem: EqOn_of_deriv_eq_zero
Proof state before:
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
z : ℂ
hz : z ∈ U
⊢ deriv g z = 0 z
Tactic:
rw [deriv_sub_const, hf' hz]
Proof state after:
no goals
Theorem: EqOn_of_deriv_eq_zero
Proof state before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
⊢ g z₀ = 0
Tactic:
simp [g]
Proof state after:
no goals
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
⊢ EqOn f g U
Tactic:
refine λ z hz => sub_eq_zero.1 ?_
Proof state after:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
⊢ f z - g z = 0
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
⊢ f z - g z = 0
Tactic:
have h2 : EqOn (deriv (λ y => f y - g y)) 0 U := by
  rintro z hz
  have e1 : U ∈ 𝓝 z := hU.mem_nhds hz
  rw [deriv_sub (hf.differentiableAt e1) (hg.differentiableAt e1), hfg hz, sub_self]
  rfl
Proof state after:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
h2 : EqOn (deriv fun y => f y - g y) 0 U
⊢ f z - g z = 0
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
h2 : EqOn (deriv fun y => f y - g y) 0 U
⊢ f z - g z = 0
Tactic:
exact EqOn_zero_of_deriv_eq_zero hU hU' (hf.sub hg) h2 hz₀ (by simp [hfgz₀]) hz
Proof state after:
no goals
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
⊢ EqOn (deriv fun y => f y - g y) 0 U
Tactic:
rintro z hz
Proof state after:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
⊢ deriv (fun y => f y - g y) z = 0 z
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
⊢ deriv (fun y => f y - g y) z = 0 z
Tactic:
have e1 : U ∈ 𝓝 z := hU.mem_nhds hz
Proof state after:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ deriv (fun y => f y - g y) z = 0 z
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ deriv (fun y => f y - g y) z = 0 z
Tactic:
rw [deriv_sub (hf.differentiableAt e1) (hg.differentiableAt e1), hfg hz, sub_self]
Proof state after:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ 0 = 0 z
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ 0 = 0 z
Tactic:
rfl
Proof state after:
no goals
Theorem: EqOn_of_EqOn_deriv
Proof state before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
h2 : EqOn (deriv fun y => f y - g y) 0 U
⊢ f z₀ - g z₀ = 0
Tactic:
simp [hfgz₀]
Proof state after:
no goals
Theorem: has_logs.has_sqrt
Proof state before:
z z₀ : ℂ
U : Set ℂ
h : has_logs U
⊢ _root_.has_sqrt U
Tactic:
rintro f hfz hf
Proof state after:
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U
Theorem: has_logs.has_sqrt
Proof state before:
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U
Tactic:
obtain ⟨l, hl, hlf⟩ := h f hf hfz
Proof state after:
case intro.intro
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U
Theorem: has_logs.has_sqrt
Proof state before:
case intro.intro
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U
Tactic:
refine ⟨λ z => exp (l z / 2), differentiable_exp.comp_differentiableOn (hl.div_const _), λ z hz => ?_⟩
Proof state after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
z : ℂ
hz : z ∈ U
⊢ f z = ((fun z => cexp (l z / 2)) ^ 2) z
Theorem: has_logs.has_sqrt
Proof state before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
z : ℂ
hz : z ∈ U
⊢ f z = ((fun z => cexp (l z / 2)) ^ 2) z
Tactic:
simpa [pow_two, ← exp_add] using hlf hz
Proof state after:
no goals
Theorem: has_primitives.has_logs
Proof state before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
⊢ _root_.has_logs U
Tactic:
by_cases h : U = ∅
Proof state after:
case pos
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
⊢ _root_.has_logs U

case neg
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U
Theorem: has_primitives.has_logs
Proof state before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
⊢ _root_.has_logs U
Tactic:
case pos => exact λ f => by simp [h, DifferentiableOn]
Proof state after:
no goals
Theorem: has_primitives.has_logs
Proof state before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U
Tactic:
case neg =>
  obtain ⟨z₀, hz₀⟩ := nonempty_iff_ne_empty.2 h
  rintro f hf hfz
  obtain ⟨lf, hlf1, hlf2⟩ := hp (deriv f / f) ((hf.deriv hU).div hf hfz)
  let g : ℂ → ℂ := λ z => lf z + (log (f z₀) - lf z₀)
  set h : ℂ → ℂ := f / (exp ∘ g)
  have h3 : DifferentiableOn ℂ g U := hlf1.add (differentiableOn_const _)
  have e4 : DifferentiableOn ℂ (exp ∘ g) U := differentiable_exp.comp_differentiableOn h3
  have e1 : DifferentiableOn ℂ h U := hf.div e4 (λ z _ => exp_ne_zero _)
  refine ⟨g, h3, ?_⟩
  suffices h : EqOn h (λ _ => 1) U
    by exact λ z hz => eq_of_div_eq_one (h hz)
  have : 1 = h z₀ := by unfold_let ; simp [exp_log, hfz z₀ hz₀]
  rw [this]
  refine EqOn_of_deriv_eq_zero hU hU' e1 (λ z hz => ?_) hz₀
  have f0 : U ∈ 𝓝 z := hU.mem_nhds hz
  dsimp
  unfold_let
  rw [Pi.div_def, deriv_div (hf.differentiableAt f0) (e4.differentiableAt f0) (exp_ne_zero _)]
  rw [deriv.scomp z differentiableAt_exp (h3.differentiableAt f0)]
  have e5 : deriv g z = deriv lf z := by unfold_let ; simp
  field_simp [exp_ne_zero, hlf2 hz, hfz z hz, e5]
  ring
Proof state after:
no goals
Theorem: has_primitives.has_logs
Proof state before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
⊢ _root_.has_logs U
Tactic:
exact λ f => by simp [h, DifferentiableOn]
Proof state after:
no goals
Theorem: has_primitives.has_logs
Proof state before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
f : ℂ → ℂ
⊢ DifferentiableOn ℂ f U → (∀ z ∈ U, f z ≠ 0) → ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
simp [h, DifferentiableOn]
Proof state after:
no goals