awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ∀ x ∈ sphere z r, _root_.id x - z ≠ 0

Tactic:
exact fun ζ hζ => sub_ne_zero.2 (ne_of_mem_sphere hζ hr.ne')

Premises used: Iff.mpr, Metric.ne_of_mem_sphere, sub_ne_zero, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
ζ : ℂ
hζ : ζ ∈ sphere z r
refine_2 : ‖f ζ‖ ≤ ‖f z‖
⊢ ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r

Tactic:
rw [le_div_iff₀ hr, norm_smul, norm_inv, mem_sphere_iff_norm.1 hζ, mul_comm,
      mul_inv_cancel_left₀ hr.ne']

Premises used: mul_inv_cancel_left₀, norm_smul, norm_inv, LT.lt.ne', mem_sphere_iff_norm, Iff.mp, mul_comm, le_div_iff₀
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
ζ : ℂ
hζ : ζ ∈ sphere z r
⊢ ‖f ζ‖ ≤ ‖f z‖

Tactic:
hz (hsub hζ)

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
ζ : ℂ
hζ : ζ ∈ sphere z r
⊢ ‖f ζ‖ ≤ ‖f z‖

Tactic:
exact hz (hsub hζ)
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
refine_3 : ‖f w‖ / dist w z < ‖f z‖ / r
⊢ ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r

Tactic:
rw [norm_smul, norm_inv, ← div_eq_inv_mul, ← dist_eq_norm]

Premises used: dist_eq_norm, norm_smul, norm_inv, div_eq_inv_mul
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖f w‖ / dist w z < ‖f z‖ / r

Tactic:
(div_lt_div_iff_of_pos_right hr).2 hw_lt

Premises used: Iff.mpr, div_lt_div_iff_of_pos_right
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖f w‖ / dist w z < ‖f z‖ / r

Tactic:
exact (div_lt_div_iff_of_pos_right hr).2 hw_lt

Premises used: Iff.mpr, div_lt_div_iff_of_pos_right
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ∀ (x : F), norm (E := F̂) ((e : (a : F) → F̂) x : F̂) = ‖x‖

Tactic:
have he : ∀ x, ‖e x‖ = ‖x‖ := UniformSpace.Completion.norm_coe
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), norm (E := F̂) ((e : (a : F) → F̂) x : F̂) = ‖x‖
⊢ IsMaxOn (Function.comp (β := F̂) norm ((⇑e : (a : F) → F̂) ∘ f)) (closedBall z (dist w z)) z

Tactic:
simpa only [IsMaxOn, Function.comp_def, he] using hz

Premises used: IsMaxOn, Function.comp_def
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), norm (E := F̂) ((e : (a : F) → F̂) x : F̂) = ‖x‖
⊢ IsMaxOn (Function.comp (β := F̂) norm ((⇑e : (a : F) → F̂) ∘ f)) (closedBall z (dist w z)) z

Tactic:
replace hz : IsMaxOn (norm ∘ e ∘ f) (closedBall z (dist w z)) z := by
    simpa only [IsMaxOn, Function.comp_def, he] using hz
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), norm (E := F̂) ((e : (a : F) → F̂) x : F̂) = ‖x‖
hz : IsMaxOn (Function.comp (β := F̂) norm ((⇑e : (a : F) → F̂) ∘ f)) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
simpa only [he, Function.comp_def]
    using norm_max_aux₁ (e.differentiable.comp_diffContOnCl hd) hz

Premises used: ContinuousLinearMap.differentiable, Function.comp_def, Complex.norm_max_aux₁, Differentiable.comp_diffContOnCl
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
r : ℝ
hr : dist w z = r
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ DiffContOnCl ℂ f (ball z (dist w z))

Tactic:
subst r
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
r : ℝ
hr : dist w z = r
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hd₁ : DiffContOnCl ℂ f (ball z (dist w z))
⊢ IsMaxOn (norm ∘ f) (ball z (dist w z)) z

Tactic:
subst r
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
inl : ∀ (hd : DiffContOnCl ℂ f (ball w (dist w w))) (hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w), ‖f w‖ = ‖f w‖
inr : ∀ (hne : w ≠ z), ‖f w‖ = ‖f z‖
⊢ ‖f w‖ = ‖f z‖

Tactic:
rcases eq_or_ne w z with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
w : ℂ
hd : DiffContOnCl ℂ f (ball w (dist w w))
hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w
⊢ ‖f w‖ = ‖f w‖

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ dist w z ≠ 0

Tactic:
rw [← dist_ne_zero] at hne

Premises used: dist_ne_zero
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : dist w z ≠ 0
⊢ ‖f w‖ = ‖f z‖

Tactic:
norm_max_aux₂ hd (closure_ball z hne ▸ hz.closure hd.continuousOn.norm)

Premises used: Complex.norm_max_aux₂, Eq.rec, IsMaxOn.closure, DiffContOnCl.continuousOn, ContinuousOn.norm, closure_ball
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : dist w z ≠ 0
⊢ ‖f w‖ = ‖f z‖

Tactic:
exact norm_max_aux₂ hd (closure_ball z hne ▸ hz.closure hd.continuousOn.norm)

Premises used: Complex.norm_max_aux₂, Eq.rec, IsMaxOn.closure, DiffContOnCl.continuousOn, ContinuousOn.norm, closure_ball
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : w ∈ closedBall z r
⊢ dist z w ≤ r

Tactic:
rw [mem_closedBall, dist_comm] at hw

Premises used: dist_comm, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
inl : ∀ (hw : dist z z ≤ r), (norm ∘ f) z = Function.const E ‖f z‖ z
inr : ∀ (hne : z ≠ w), (norm ∘ f) w = Function.const E ‖f z‖ w
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
rcases eq_or_ne z w with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hw : dist z z ≤ r
⊢ (norm ∘ f) z = Function.const E ‖f z‖ z

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
⊢ Differentiable ℂ e

Tactic:
have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
this : ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
simpa [e]
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
inr : ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
suffices ‖(f ∘ e) (1 : ℂ)‖ = ‖(f ∘ e) (0 : ℂ)‖ by simpa [e]
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
⊢ dist (α := ℂ) 1 0 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
⊢ dist (α := ℂ) 1 0 = 1

Tactic:
have hr : dist (1 : ℂ) 0 = 1 := by simp
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hr : dist (α := ℂ) 1 0 = 1
⊢ MapsTo e (ball 0 1) (ball z r)

Tactic:
((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono
      Subset.rfl ?_

Premises used: nndist_eq_zero, LipschitzWith.mapsTo_ball, mt, Set.MapsTo.mono, Set.Subset.rfl, Iff.mp, OfNat.ofNat, lipschitzWith_lineMap
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hr : dist (α := ℂ) 1 0 = 1
refine : ball ((lineMap z w : (a : ℂ) → E) 0) ((↑(nndist z w) : ℝ) * 1) ⊆ ball z r
⊢ MapsTo e (ball 0 1) (ball z r)

Tactic:
refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono
      Subset.rfl ?_

Premises used: nndist_eq_zero, LipschitzWith.mapsTo_ball, mt, Set.MapsTo.mono, Set.Subset.rfl, Iff.mp, OfNat.ofNat, lipschitzWith_lineMap
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hr : dist (α := ℂ) 1 0 = 1
⊢ ball ((lineMap z w : (a : ℂ) → E) 0) ((↑(nndist z w) : ℝ) * 1) ⊆ ball z r

Tactic:
simpa only [lineMap_apply_zero, mul_one, coe_nndist] using ball_subset_ball hw

Premises used: coe_nndist, AffineMap.lineMap_apply_zero, Metric.ball_subset_ball, mul_one
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hr : dist (α := ℂ) 1 0 = 1
⊢ MapsTo e (ball 0 1) (ball z r)

Tactic:
have hball : MapsTo e (ball 0 1) (ball z r) := by
    refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono
      Subset.rfl ?_
    simpa only [lineMap_apply_zero, mul_one, coe_nndist] using ball_subset_ball hw
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hr : dist (α := ℂ) 1 0 = 1
hball : MapsTo e (ball 0 1) (ball z r)
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖

Tactic:
norm_max_aux₃ hr (hd.comp hde.diffContOnCl hball)
      (hz.comp_mapsTo hball (lineMap_apply_zero z w))

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, IsMaxOn.comp_mapsTo, Complex.norm_max_aux₃, AffineMap.lineMap_apply_zero
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hr : dist (α := ℂ) 1 0 = 1
hball : MapsTo e (ball 0 1) (ball z r)
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖

Tactic:
exact norm_max_aux₃ hr (hd.comp hde.diffContOnCl hball)
      (hz.comp_mapsTo hball (lineMap_apply_zero z w))

Premises used: Differentiable.diffContOnCl, DiffContOnCl.comp, IsMaxOn.comp_mapsTo, Complex.norm_max_aux₃, AffineMap.lineMap_apply_zero
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
s : Set E
z w : E
hd : DiffContOnCl ℂ f s
hz : IsMaxOn (norm ∘ f) s z
hsub : ball z (dist w z) ⊆ s
⊢ ‖f w‖ = ‖f z‖

Tactic:
norm_eqOn_closedBall_of_isMaxOn (hd.mono hsub) (hz.on_subset hsub) (mem_closedBall.2 le_rfl)

Premises used: Iff.mpr, DiffContOnCl.mono, le_rfl, IsMaxOn.on_subset, Complex.norm_eqOn_closedBall_of_isMaxOn, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
rcases :
  ∀ (r : ℝ) (hr₀ : 0 < r) (hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c),
    ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩

Premises used: Filter.Eventually.and, Iff.mp, Filter.HasBasis.eventually_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
nhds_basis_closedBall.eventually_iff.2
    ⟨r, hr₀, norm_eqOn_closedBall_of_isMaxOn (DifferentiableOn.diffContOnCl fun x hx =>
        (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt) fun x hx =>
      (hr <| ball_subset_closedBall hx).2⟩

Premises used: Iff.mpr, Metric.ball_subset_closedBall, DifferentiableAt.differentiableWithinAt, Metric.closure_ball_subset_closedBall, DifferentiableOn.diffContOnCl, And.right, And.left, And.intro, Exists.intro, Filter.HasBasis.eventually_iff, Complex.norm_eqOn_closedBall_of_isMaxOn, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
exact nhds_basis_closedBall.eventually_iff.2
    ⟨r, hr₀, norm_eqOn_closedBall_of_isMaxOn (DifferentiableOn.diffContOnCl fun x hx =>
        (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt) fun x hx =>
      (hr <| ball_subset_closedBall hx).2⟩

Premises used: Iff.mpr, Metric.ball_subset_closedBall, DifferentiableAt.differentiableWithinAt, Metric.closure_ball_subset_closedBall, DifferentiableOn.diffContOnCl, And.right, And.left, And.intro, Exists.intro, Filter.HasBasis.eventually_iff, Complex.norm_eqOn_closedBall_of_isMaxOn, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {z : E | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}

Tactic:
isOpen_iff_mem_nhds.2 fun z hz => (eventually_eventually_nhds.2 hz.1).and ?_

Premises used: Iff.mpr, Filter.Eventually.and, And.left, isOpen_iff_mem_nhds, eventually_eventually_nhds
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
refine :
  ∀ (z : E) (hz : Membership.mem (γ := Set E) {z : E | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z} z),
    Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {z : E | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}

Tactic:
refine isOpen_iff_mem_nhds.2 fun z hz => (eventually_eventually_nhds.2 hz.1).and ?_

Premises used: Iff.mpr, Filter.Eventually.and, isOpen_iff_mem_nhds, eventually_eventually_nhds
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
s : Set E
hd : DifferentiableOn ℂ f s
z : E
hz : Membership.mem (γ := Set E) {z : E | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z} z
⊢ ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w

Tactic:
replace hd : ∀ᶠ w in 𝓝 z, DifferentiableAt ℂ f w := hd.eventually_differentiableAt hz.1
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
s : Set E
z : E
hz : Membership.mem (γ := Set E) {z : E | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z} z
hd : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
⊢ Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)

Tactic:
(norm_eventually_eq_of_isLocalMax hd <| hz.2.isLocalMax hz.1).mono fun x hx y hy =>
    le_trans (hz.2 hy).out hx.ge

Premises used: Eq.ge, Membership.mem.out, Complex.norm_eventually_eq_of_isLocalMax, IsMaxOn.isLocalMax, Filter.Eventually.mono, And.right, And.left, le_trans
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
s : Set E
z : E
hz : Membership.mem (γ := Set E) {z : E | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z} z
hd : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
⊢ Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)

Tactic:
exact (norm_eventually_eq_of_isLocalMax hd <| hz.2.isLocalMax hz.1).mono fun x hx y hy =>
    le_trans (hz.2 hy).out hx.ge

Premises used: Complex.norm_eventually_eq_of_isLocalMax, IsMaxOn.isLocalMax, Filter.Eventually.mono, And.right, And.left
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z : E | IsMaxOn (norm ∘ f) U z}
⊢ ∀ x ∈ V, ‖f x‖ = ‖f c‖

Tactic:
have hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖ := fun x hx => le_antisymm (hm hx.1) (hx.2 hcU)
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z : E | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
suffices : U ⊆ V
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U

Tactic:
suffices U ⊆ V from fun x hx => hV x (this hx)
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z : E | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V

Tactic:
simpa only [ho.mem_nhds_iff, setOf_and, setOf_mem_eq]
      using isOpen_setOf_mem_nhds_and_isMaxOn_norm hd

Premises used: Set.setOf_and, Set.setOf_mem_eq, IsOpen.mem_nhds_iff, Complex.isOpen_setOf_mem_nhds_and_isMaxOn_norm