awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
h₂ h₃ : ∀ (z : E), f⁻¹ z = f⁻¹ c → f z = f c
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c

Tactic:
filter_upwards [eventually_eq_of_isLocalMax_norm h4 h3] with z using inv_inj.mp

Premises used: inv_inj, Iff.mp, Complex.eventually_eq_of_isLocalMax_norm
-- 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 : Nontrivial E
inst_5 : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
⊢ IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
have hc : IsCompact (closure U) := hb.isCompact_closure
-- 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 : 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 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U,
    IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w

Tactic:
hc.exists_isMaxOn hne.closure hd.continuousOn.norm

Premises used: Set.Nonempty.closure, DiffContOnCl.continuousOn, ContinuousOn.norm, 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 : 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)
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
⊢ ∃ 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

Premises used: Set.Nonempty.closure, closure, DiffContOnCl.continuousOn, ContinuousOn.norm, 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 : 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
⊢ w ∈ interior U ∨ w ∈ frontier U

Tactic:
rw [closure_eq_interior_union_frontier, mem_union] at hwU

Premises used: Set.mem_union, closure_eq_interior_union_frontier
-- 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 : 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
hwU₁ : w ∈ interior U ∨ w ∈ frontier U
⊢ IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w

Tactic:
rw [closure_eq_interior_union_frontier, mem_union] at hwU

Premises used: Set.mem_union, closure_eq_interior_union_frontier
-- 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 : 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 ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
inl :
  ∀ (hwU : w ∈ interior U),
    ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
inr :
  ∀ (hwU : w ∈ frontier U),
    ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
rcases hwU with hwU | hwU
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ frontier U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
⟨w, hwU, hle⟩

Premises used: And.intro, Exists.intro
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ frontier U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
exact ⟨w, hwU, hle⟩
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
⊢ interior U ≠ univ

Tactic:
have : interior U ≠ univ := ne_top_of_le_ne_top hc.ne_univ interior_subset_closure
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
inl :
  ∀ (z : E) (hzU : z ∈ frontier (interior U)) (hzw : infDist w (interior U)ᶜ = dist w z),
    ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
rcases exists_mem_frontier_infDist_compl_eq_dist hwU this with ⟨z, hzU, hzw⟩

Premises used: exists_mem_frontier_infDist_compl_eq_dist
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
⟨z, frontier_interior_subset hzU, fun x hx => (hle hx).out.trans_eq ?_⟩

Premises used: LE.le.trans_eq, Membership.mem.out, frontier_interior_subset, And.intro, Exists.intro
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
inl : ∀ (x : E) (hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U), (norm ∘ f) w = (norm ∘ f) z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
refine ⟨z, frontier_interior_subset hzU, fun x hx => (hle hx).out.trans_eq ?_⟩
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ (norm ∘ f) w = (norm ∘ f) z

Tactic:
(norm_eq_norm_of_isMaxOn_of_ball_subset hd (hle.on_subset subset_closure) ?_).symm

Premises used: subset_closure, Complex.norm_eq_norm_of_isMaxOn_of_ball_subset, IsMaxOn.on_subset, Eq.symm
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
inl : ball w (dist z w) ⊆ U
⊢ (norm ∘ f) w = (norm ∘ f) z

Tactic:
refine (norm_eq_norm_of_isMaxOn_of_ball_subset hd (hle.on_subset subset_closure) ?_).symm

Premises used: subset_closure, Complex.norm_eq_norm_of_isMaxOn_of_ball_subset, IsMaxOn.on_subset, Eq.symm
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
inl : ball w (infDist w (interior U)ᶜ) ⊆ U
⊢ ball w (dist z w) ⊆ U

Tactic:
rw [dist_comm, ← hzw]

Premises used: dist_comm
-- 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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ball w (infDist w (interior U)ᶜ) ⊆ U

Tactic:
ball_infDist_compl_subset.trans interior_subset

Premises used: interior_subset, Metric.ball_infDist_compl_subset, HasSubset.Subset.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 : 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
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ball w (infDist w (interior U)ᶜ) ⊆ U

Tactic:
exact ball_infDist_compl_subset.trans interior_subset

Premises used: interior_subset, Metric.ball_infDist_compl_subset, HasSubset.Subset.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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ z ∈ frontier U ∨ z ∈ U

Tactic:
rw [closure_eq_self_union_frontier, union_comm, mem_union] at hz

Premises used: Set.mem_union, Set.union_comm, closure_eq_self_union_frontier
-- 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U ∨ z ∈ U
inl : ∀ (hz : z ∈ frontier U), ‖f z‖ ≤ C
inr : ∀ (hz : z ∈ U), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
rcases hz with hz | 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C

Tactic:
hC 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C

Tactic:
exact hC 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
inr : ∀ (w : E) (hne : w ≠ z), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
rcases exists_ne z with ⟨w, hne⟩

Premises used: exists_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
inst_4 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
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
inst_4 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
⊢ AntilipschitzWith (nndist z w)⁻¹ e

Tactic:
have hL : AntilipschitzWith (nndist z w)⁻¹ e := antilipschitzWith_lineMap hne.symm
-- 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)

Tactic:
replace hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U) :=
    hd.comp hde.diffContOnCl (mapsTo_preimage _ _)
-- 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ 0 ∈ e ⁻¹' U

Tactic:
simpa only [e, mem_preimage, lineMap_apply_zero]

Premises used: AffineMap.lineMap_apply_zero, Set.mem_preimage
-- 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ 0 ∈ e ⁻¹' U

Tactic:
have h₀ : (0 : ℂ) ∈ e ⁻¹' U := by simpa only [e, mem_preimage, 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
inst_4 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
inr : ∀ (ζ : ℂ) (hζU : ζ ∈ frontier (e ⁻¹' U)) (hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
rcases exists_mem_frontier_isMaxOn_norm (hL.isBounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩

Premises used: Complex.exists_mem_frontier_isMaxOn_norm, AntilipschitzWith.isBounded_preimage, Exists.intro, OfNat.ofNat
-- 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ = ‖f (e 0)‖

Tactic:
simp only [e, lineMap_apply_zero]

Premises used: 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
inst_4 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f (e 0)‖ ≤ ‖f (e ζ)‖

Tactic:
hζ (subset_closure h₀)

Premises used: Set.Mem, subset_closure
-- 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f (e ζ)‖ ≤ C

Tactic:
hC _ (hde.continuous.frontier_preimage_subset _ hζU)

Premises used: Continuous.frontier_preimage_subset, Differentiable.continuous
-- 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 : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
by : ‖f z‖ = ‖f (e 0)‖
⊢ ‖f z‖ ≤ C

Tactic:
calc
    ‖f z‖ = ‖f (e 0)‖ := by simp only [e, lineMap_apply_zero]
    _ ≤ ‖f (e ζ)‖ := hζ (subset_closure h₀)
    _ ≤ C := hC _ (hde.continuous.frontier_preimage_subset _ hζU)

Premises used: subset_closure, Continuous.frontier_preimage_subset, OfNat.ofNat, Differentiable.continuous
-- 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 : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
H : ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0
⊢ EqOn f g (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
simpa [sub_eq_zero] using H

Premises used: sub_eq_zero