awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
have hVo : IsOpen V := by
    simpa only [ho.mem_nhds_iff, setOf_and, setOf_mem_eq]
      using isOpen_setOf_mem_nhds_and_isMaxOn_norm hd
-- 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‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
⊢ (U ∩ V).Nonempty

Tactic:
have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, hm⟩
-- 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‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z : E | ‖f z‖ ≠ ‖f c‖}
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W

Tactic:
have hWo : IsOpen W := hd.continuousOn.norm.isOpen_inter_preimage ho isOpen_ne
-- 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‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z : E | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W
⊢ Disjoint V W

Tactic:
have hdVW : Disjoint V W := disjoint_left.mpr fun x hxV hxW => hxW.2 (hV x hxV)
-- 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‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z : E | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W
hdVW : Disjoint V W
⊢ U ⊆ V ∪ W

Tactic:
have hUVW : U ⊆ V ∪ W := fun x hx =>
    (eq_or_ne ‖f x‖ ‖f c‖).imp (fun h => ⟨hx, fun y hy => (hm hy).out.trans_eq h.symm⟩)
      (And.intro 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‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z : E | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W
hdVW : Disjoint V W
hUVW : U ⊆ V ∪ W
⊢ U ⊆ V

Tactic:
hc.subset_left_of_subset_union hVo hWo hdVW hUVW hVne

Premises used: IsPreconnected.subset_left_of_subset_union
-- 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‖
hVo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z : E | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W
hdVW : Disjoint V W
hUVW : U ⊆ V ∪ W
⊢ U ⊆ V

Tactic:
exact hc.subset_left_of_subset_union hVo hWo hdVW hUVW hVne

Premises used: IsPreconnected.subset_left_of_subset_union
-- 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 : DiffContOnCl ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
(norm_eqOn_of_isPreconnected_of_isMaxOn hc ho hd.differentiableOn hcU hm).of_subset_closure
    hd.continuousOn.norm continuousOn_const subset_closure Subset.rfl

Premises used: Set.EqOn.of_subset_closure, subset_closure, continuousOn_const, Complex.norm_eqOn_of_isPreconnected_of_isMaxOn, Set.Subset.rfl, DiffContOnCl.continuousOn, ContinuousOn.norm, DiffContOnCl.differentiableOn
-- 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
inst_4 : StrictConvexSpace ℝ 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
x : E
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + Function.const E (f c) x‖ = ‖f x‖ + ‖Function.const E (f c) x‖

Tactic:
simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]

Premises used: Function.const, SameRay.norm_add, SameRay.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
inst_4 : StrictConvexSpace ℝ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hd : DiffContOnCl ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
⊢ EqOn f (Function.const E (f c)) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
(eqOn_of_isPreconnected_of_isMaxOn_norm hc ho hd.differentiableOn hcU hm).of_subset_closure
    hd.continuousOn continuousOn_const subset_closure Subset.rfl

Premises used: Set.EqOn.of_subset_closure, subset_closure, continuousOn_const, Set.Subset.rfl, DiffContOnCl.continuousOn, Complex.eqOn_of_isPreconnected_of_isMaxOn_norm, DiffContOnCl.differentiableOn
-- 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
inst_4 : StrictConvexSpace ℝ 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
H₁ : ‖f w‖ = ‖f z‖
H₂ : ‖f w + f z‖ = ‖f z + f z‖
⊢ ‖f w + f z‖ = ‖f w‖ + ‖f z‖

Tactic:
simp only [H₂, SameRay.rfl.norm_add, H₁]

Premises used: SameRay.norm_add, SameRay.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
inst_4 : StrictConvexSpace ℝ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ EqOn f (Function.const E (f z)) (closedBall z r)

Tactic:
fun _x hx =>
  eq_of_isMaxOn_of_ball_subset hd hz <| ball_subset_ball hx

Premises used: Complex.eq_of_isMaxOn_of_ball_subset, Set.EqOn, Metric.ball_subset_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
inst_4 : StrictConvexSpace ℝ F
f : E → F
b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
v : E
hv : Membership.mem (γ := Set E) (ball 0 b) v
hv_max : IsMaxOn (norm ∘ f) (ball 0 b) v
⊢ EqOn f (Function.const E (f v)) (ball 0 b)

Tactic:
Complex.eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball 0 b).isPreconnected
    isOpen_ball h_an hv hv_max

Premises used: convex_ball, Metric.isOpen_ball, Complex.eqOn_of_isPreconnected_of_isMaxOn_norm, OfNat.ofNat, Convex.isPreconnected
-- 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
inst_4 : StrictConvexSpace ℝ F
inst_5 : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr :
  ∀ (z : E),
    Membership.mem (γ := Set E) (ball 0 b) z → ∃ (w : E), Membership.mem (γ := Set E) (closedBall 0 r) w ∧ ‖f z‖ ≤ ‖f w‖
obtain :
  ∀ (x : E) (hx_mem : Membership.mem (γ := Set E) (closedBall 0 r) x)
    (hx_max : IsMaxOn (β := ℝ) (fun (x : E) ↦ ‖f x‖) (closedBall 0 r) x), EqOn f (Function.const E (f 0)) (ball 0 b)
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
obtain ⟨x, hx_mem, hx_max⟩ := isCompact_closedBall (0 : E) r |>.exists_isMaxOn
    (nonempty_closedBall.mpr hr_nn)
    (h_an.continuousOn.mono <| closedBall_subset_ball hr_lt).norm

Premises used: Iff.mpr, DifferentiableOn.continuousOn, Metric.closedBall_subset_ball, Metric.nonempty_closedBall, ContinuousOn.mono, ContinuousOn.norm, ProperSpace.isCompact_closedBall, OfNat.ofNat, IsCompact.exists_isMaxOn
-- 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
inst_4 : StrictConvexSpace ℝ F
inst_5 : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr :
  ∀ (z : E),
    Membership.mem (γ := Set E) (ball 0 b) z → ∃ (w : E), Membership.mem (γ := Set E) (closedBall 0 r) w ∧ ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : Membership.mem (γ := Set E) (closedBall 0 r) x
hx_max : IsMaxOn (β := ℝ) (fun (x : E) ↦ ‖f x‖) (closedBall 0 r) x
this : EqOn f (Function.const E (f x)) (ball 0 b)
rwa rwa₁ rwa₂ rwa₃ : EqOn f (Function.const E (Function.const E (f x) 0)) (ball 0 b)
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]

Premises used: Metric.mem_ball_self, LE.le.trans_lt
-- 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
inst_4 : StrictConvexSpace ℝ F
inst_5 : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr :
  ∀ (z : E),
    Membership.mem (γ := Set E) (ball 0 b) z → ∃ (w : E), Membership.mem (γ := Set E) (closedBall 0 r) w ∧ ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : Membership.mem (γ := Set E) (closedBall 0 r) x
hx_max : IsMaxOn (β := ℝ) (fun (x : E) ↦ ‖f x‖) (closedBall 0 r) x
suffices : EqOn f (Function.const E (f x)) (ball 0 b)
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
suffices Set.EqOn f (Function.const E (f x)) (ball 0 b) by
    rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]
-- 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
inst_4 : StrictConvexSpace ℝ F
inst_5 : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr :
  ∀ (z : E),
    Membership.mem (γ := Set E) (ball 0 b) z → ∃ (w : E), Membership.mem (γ := Set E) (closedBall 0 r) w ∧ ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : Membership.mem (γ := Set E) (closedBall 0 r) x
hx_max : IsMaxOn (β := ℝ) (fun (x : E) ↦ ‖f x‖) (closedBall 0 r) x
apply :
  ∀ (z : E) (hz : Membership.mem (γ := Set E) (ball 0 b) z),
    Membership.mem (γ := Set E) {x_1 : E | (fun (x_2 : E) ↦ (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1} z
⊢ EqOn f (Function.const E (f x)) (ball 0 b)

Tactic:
apply eq_const_of_exists_max h_an (closedBall_subset_ball hr_lt hx_mem) (fun z hz ↦ ?_)

Premises used: Metric.closedBall_subset_ball, Complex.eq_const_of_exists_max
-- 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
inst_4 : StrictConvexSpace ℝ F
inst_5 : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr :
  ∀ (z : E),
    Membership.mem (γ := Set E) (ball 0 b) z → ∃ (w : E), Membership.mem (γ := Set E) (closedBall 0 r) w ∧ ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : Membership.mem (γ := Set E) (closedBall 0 r) x
hx_max : IsMaxOn (β := ℝ) (fun (x : E) ↦ ‖f x‖) (closedBall 0 r) x
z : E
hz : Membership.mem (γ := Set E) (ball 0 b) z
obtain :
  ∀ (w : E) (hw : Membership.mem (γ := Set E) (closedBall 0 r) w) (hw' : ‖f z‖ ≤ ‖f w‖),
    Membership.mem (γ := Set E) {x_1 : E | (fun (x_2 : E) ↦ (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1} z
⊢ Membership.mem (γ := Set E) {x_1 : E | (fun (x_2 : E) ↦ (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1} z

Tactic:
obtain ⟨w, hw, hw'⟩ := hr z hz
-- 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
inst_4 : StrictConvexSpace ℝ F
inst_5 : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr :
  ∀ (z : E),
    Membership.mem (γ := Set E) (ball 0 b) z → ∃ (w : E), Membership.mem (γ := Set E) (closedBall 0 r) w ∧ ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : Membership.mem (γ := Set E) (closedBall 0 r) x
hx_max : IsMaxOn (β := ℝ) (fun (x : E) ↦ ‖f x‖) (closedBall 0 r) x
z : E
hz : Membership.mem (γ := Set E) (ball 0 b) z
w : E
hw : Membership.mem (γ := Set E) (closedBall 0 r) w
hw' : ‖f z‖ ≤ ‖f w‖
⊢ Membership.mem (γ := Set E) {x_1 : E | (fun (x_2 : E) ↦ (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1} z

Tactic:
hw'.trans (hx_max hw)

Premises used: Set.Mem, setOf, LE.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
inst_4 : StrictConvexSpace ℝ F
inst_5 : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr :
  ∀ (z : E),
    Membership.mem (γ := Set E) (ball 0 b) z → ∃ (w : E), Membership.mem (γ := Set E) (closedBall 0 r) w ∧ ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : Membership.mem (γ := Set E) (closedBall 0 r) x
hx_max : IsMaxOn (β := ℝ) (fun (x : E) ↦ ‖f x‖) (closedBall 0 r) x
z : E
hz : Membership.mem (γ := Set E) (ball 0 b) z
w : E
hw : Membership.mem (γ := Set E) (closedBall 0 r) w
hw' : ‖f z‖ ≤ ‖f w‖
⊢ Membership.mem (γ := Set E) {x_1 : E | (fun (x_2 : E) ↦ (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1} z

Tactic:
exact hw'.trans (hx_max hw)

Premises used: LE.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
inst_4 : StrictConvexSpace ℝ 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
inst_4 : StrictConvexSpace ℝ 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₀, eqOn_closedBall_of_isMaxOn_norm (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, Complex.eqOn_closedBall_of_isMaxOn_norm, Metric.closure_ball_subset_closedBall, DifferentiableOn.diffContOnCl, And.right, And.left, And.intro, Exists.intro, 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
inst_4 : StrictConvexSpace ℝ 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₀, eqOn_closedBall_of_isMaxOn_norm (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, Complex.eqOn_closedBall_of_isMaxOn_norm, Metric.closure_ball_subset_closedBall, DifferentiableOn.diffContOnCl, And.right, And.left, And.intro, Exists.intro, 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 : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
⊢ (∀ᶠ (z : E) in 𝓝 c, f z = f c) ∨ f c = 0

Tactic:
or_iff_not_imp_right.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_right
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
refine : ∀ (h : ¬f c = 0), ∀ᶠ (z : E) in 𝓝 c, f z = f c
⊢ (∀ᶠ (z : E) in 𝓝 c, f z = f c) ∨ f c = 0

Tactic:
refine or_iff_not_imp_right.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_right
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
⊢ ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0

Tactic:
have h1 : ∀ᶠ z in 𝓝 c, f z ≠ 0 := hf.self_of_nhds.continuousAt.eventually_ne h
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
⊢ IsLocalMax (norm ∘ f)⁻¹ c

Tactic:
have h2 : IsLocalMax (norm ∘ f)⁻¹ c := hc.inv (h1.mono fun z => norm_pos_iff.mpr)
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ IsLocalMax (norm ∘ f⁻¹) c

Tactic:
h2.congr (Eventually.of_forall ?_)

Premises used: IsLocalMax.congr, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
refine : ∀ (x : E), (norm ∘ f)⁻¹ x = (norm ∘ f⁻¹) x
⊢ IsLocalMax (norm ∘ f⁻¹) c

Tactic:
refine h2.congr (Eventually.of_forall ?_)

Premises used: IsLocalMax.congr, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ ∀ (x : E), (norm ∘ f)⁻¹ x = (norm ∘ f⁻¹) x

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ IsLocalMax (norm ∘ f⁻¹) c

Tactic:
have h3 : IsLocalMax (norm ∘ f⁻¹) c := by refine h2.congr (Eventually.of_forall ?_); simp
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h_1 : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
z : E
h : DifferentiableAt ℂ f z
⊢ f z ≠ 0 → DifferentiableAt ℂ f⁻¹ z

Tactic:
h.inv

Premises used: DifferentiableAt.inv
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ DifferentiableAt ℂ f z) x} x →
          Membership.mem (γ := Set E)
            {x : E |
              Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ f z ≠ 0) x} x →
                Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ DifferentiableAt ℂ f⁻¹ z) x} x}
            x}
      a
h₂ h₃ : ∀ (z : E) (h : DifferentiableAt ℂ f z), f z ≠ 0 → DifferentiableAt ℂ f⁻¹ z
⊢ ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z

Tactic:
filter_upwards [hf, h1] with z h using h.inv
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
⊢ ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z

Tactic:
have h4 : ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f⁻¹ z := by filter_upwards [hf, h1] with z h using h.inv
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
h4 : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z
z : E
⊢ f⁻¹ z = f⁻¹ c → f z = f c

Tactic:
inv_inj.mp

Premises used: inv_inj, Iff.mp