awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
have inr : ∀ (hne : z ≠ w), (norm ∘ f) w = Function.const E ‖f z‖ w
Tactic: rcases eq_or_ne z w with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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)
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
have hde : Differentiable ℂ e
Tactic: have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
have inr : ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
Tactic: suffices ‖(f ∘ e) (1 : ℂ)‖ = ‖(f ∘ e) (0 : ℂ)‖ by simpa [e]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
have hr : dist (α := ℂ) 1 0 = 1
Tactic: have hr : dist (1 : ℂ) 0 = 1 := by simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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)
have refine : ball ((lineMap z w : (a : ℂ) → E) 0) ((↑(nndist z w) : ℝ) * 1) ⊆ ball z r
Tactic: refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono
      Subset.rfl ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
have hball : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖
have 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‖
Tactic: rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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}
have 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)
Tactic: refine isOpen_iff_mem_nhds.2 fun z hz => (eventually_eventually_nhds.2 hz.1).and ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
⊢ Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)
have hd₁ : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w
Tactic: replace hd : ∀ᶠ w in 𝓝 z, DifferentiableAt ℂ f w := hd.eventually_differentiableAt hz.1
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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}
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U
have hV : ∀ 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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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‖
⊢ EqOn (norm ∘ f) (Function.const E ‖f c‖) U
have suffices : U ⊆ V
Tactic: suffices U ⊆ V from fun x hx => hV x (this hx)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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‖
⊢ U ⊆ V
have hVo : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
have hVne : (U ∩ V).Nonempty
Tactic: have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, hm⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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‖}
⊢ U ⊆ V
have hWo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] W
Tactic: have hWo : IsOpen W := hd.continuousOn.norm.isOpen_inter_preimage ho isOpen_ne
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
⊢ U ⊆ V
have hdVW : Disjoint V W
Tactic: have hdVW : Disjoint V W := disjoint_left.mpr fun x hxV hxW => hxW.2 (hV x hxV)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
have hUVW : 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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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‖
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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)
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)
have rwa : EqOn f (Function.const E (Function.const E (f x) 0)) (ball 0 b)
Tactic: rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)
have suffices : EqOn f (Function.const E (f x)) (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))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ EqOn f (Function.const E (f x)) (ball 0 b)
have 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
Tactic: apply eq_const_of_exists_max h_an (closedBall_subset_ball hr_lt hx_mem) (fun z hz ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ Membership.mem (γ := Set E) {x_1 : E | (fun (x_2 : E) ↦ (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1} z
have 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
Tactic: obtain ⟨w, hw, hw'⟩ := hr z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ ∀ᶠ (y : E) in 𝓝 c, f y = f c
have 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
Tactic: rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
have refine : ∀ (h : ¬f c = 0), ∀ᶠ (z : E) in 𝓝 c, f z = f c
Tactic: refine or_iff_not_imp_right.mpr fun h => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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 = f c
have h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
Tactic: have h1 : ∀ᶠ z in 𝓝 c, f z ≠ 0 := hf.self_of_nhds.continuousAt.eventually_ne h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
have h2 : IsLocalMax (norm ∘ f)⁻¹ c
Tactic: have h2 : IsLocalMax (norm ∘ f)⁻¹ c := hc.inv (h1.mono fun z => norm_pos_iff.mpr)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
have refine : ∀ (x : E), (norm ∘ f)⁻¹ x = (norm ∘ f⁻¹) x
Tactic: refine h2.congr (Eventually.of_forall ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
have h3 : IsLocalMax (norm ∘ f⁻¹) c
Tactic: have h3 : IsLocalMax (norm ∘ f⁻¹) c := by refine h2.congr (Eventually.of_forall ?_); simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
have 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
Tactic: filter_upwards [hf, h1] with z h using h.inv
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
⊢ ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z
have h₂ : ∀ (a : E), DifferentiableAt ℂ f a → f a ≠ 0 → DifferentiableAt ℂ f⁻¹ a
Tactic: filter_upwards [hf, h1] with z h using h.inv
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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, f z = f c
have h4 : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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) in 𝓝 c, f z = f c
have h₁ : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E |
      Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ f⁻¹ y = f⁻¹ c) x} x →
        Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ f z = f c) x} x}
    a
Tactic: filter_upwards [eventually_eq_of_isLocalMax_norm h4 h3] with z using inv_inj.mp
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ f⁻¹ y = f⁻¹ c) x} x →
          Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ f z = f c) x} x}
      a
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
have h₂ : ∀ (a : E), f⁻¹ a = f⁻¹ c → f a = f c
Tactic: filter_upwards [eventually_eq_of_isLocalMax_norm h4 h3] with z using inv_inj.mp
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
inst_5 : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
have hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
Tactic: have hc : IsCompact (closure U) := hb.isCompact_closure
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
inst_5 : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
have obtain : ∀ (w : E) (hwU : w ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
  (hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w),
  ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Tactic: obtain ⟨w, hwU, hle⟩ : ∃ w ∈ closure U, IsMaxOn (norm ∘ f) (closure U) w :=
    hc.exists_isMaxOn hne.closure hd.continuousOn.norm
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
inst_5 : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hwU : w ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
have hwU₁ : w ∈ interior U ∨ w ∈ frontier U
Tactic: rw [closure_eq_interior_union_frontier, mem_union] at hwU
Cleared hypotheses: hwU, hle