awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
⊢ ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
have this : e.target ∈ 𝓝 ((↑e : M → E) c)
Tactic: have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
⊢ ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
have h : ∀ (y : E) (hyt : y ∈ e.target) (hy₂ : MDiffAt f ((↑e.symm : E → M) y)), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
Tactic: filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
⊢ (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
have rw : (↑e.symm : E → M) y ∈ (extChartAt I c).source
Tactic: rw [← extChartAt_source I c]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
⊢ DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
have hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
Tactic: have hys : e.symm y ∈ (chartAt H c).source := by
      rw [← extChartAt_source I c]
      exact (extChartAt I c).map_target hyt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
have hfy : Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
  (f ((↑e.symm : E → M) y))
Tactic: have hfy : f (e.symm y) ∈ (chartAt F (0 : F)).source := mem_univ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
this : e.target ∈ 𝓝 ((↑e : M → E) c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f ((↑e.symm : E → M) y)
hys : (↑e.symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hfy :
  Membership.mem (γ := Set F) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (chartAt F 0)))
    (f ((↑e.symm : E → M) y))
⊢ DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
have hy₃ : ContinuousAt f ((↑e.symm : E → M) y) ∧
  DifferentiableAt ℂ ((↑(extChartAt 𝓘(ℂ, F) 0) : F → F) ∘ f ∘ (↑(extChartAt I c).symm : E → M)) y
Tactic: rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ,
      e.right_inv hyt] at hy₂
Cleared hypotheses: hy₂, hys, hfy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
⊢ ∀ᶠ (a : E) in 𝓝 ((↑e : M → E) c), ‖f ((↑e.symm : E → M) a)‖ = ‖f c‖
have hd₁ : ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
Tactic: replace hd : ∀ᶠ y in 𝓝 (e c), DifferentiableAt ℂ (f ∘ e.symm) y := by
    have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c
    filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂
    have hys : e.symm y ∈ (chartAt H c).source := by
      rw [← extChartAt_source I c]
      exact (extChartAt I c).map_target hyt
    have hfy : f (e.symm y) ∈ (chartAt F (0 : F)).source := mem_univ _
    rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ,
      e.right_inv hyt] at hy₂
    exact hy₂.2
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
⊢ ∀ᶠ (a : E) in 𝓝 ((↑e : M → E) c), ‖f ((↑e.symm : E → M) a)‖ = ‖f c‖
have h : ∀ (x : E), f c = (f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)
Tactic: convert! norm_eventually_eq_of_isLocalMax hd _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 ((↑e : M → E) c), DifferentiableAt ℂ (f ∘ (↑e.symm : E → M)) y
h : ∀ (x : E), f c = (f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)
⊢ ∀ᶠ (a : E) in 𝓝 ((↑e : M → E) c), ‖f ((↑e.symm : E → M) a)‖ = ‖f c‖
have convert! : IsLocalMax (norm ∘ f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)
Tactic: convert! norm_eventually_eq_of_isLocalMax hd _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ EqOn (norm ∘ f) (const M ‖f c‖) U
have suffices : U ⊆ V
Tactic: suffices U ⊆ V from fun x hx ↦ (this hx).2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ IsOpen[inst_6] V
have refine : ∀ (x : M) (hx : x ∈ V), (fun (z : M) ↦ ‖f z‖ = ‖f c‖) ∈ 𝓝 x
Tactic: refine isOpen_iff_mem_nhds.2 fun x hx ↦ inter_mem (ho.mem_nhds hx.1) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
x : M
hx : x ∈ V
⊢ (fun (z : M) ↦ ‖f z‖ = ‖f c‖) ∈ 𝓝 x
have hm₁ : IsLocalMax (β := ℝ) (fun (x : M) ↦ ‖f x‖) x
Tactic: replace hm : IsLocalMax (‖f ·‖) x :=
      mem_of_superset (ho.mem_nhds hx.1) fun z hz ↦ (hm hz).out.trans_eq hx.2.symm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
x : M
hx : x ∈ V
hm : IsLocalMax (β := ℝ) (fun (x : M) ↦ ‖f x‖) x
⊢ (fun (z : M) ↦ ‖f z‖ = ‖f c‖) ∈ 𝓝 x
have hd₁ : ∀ᶠ (y : M) in 𝓝 x, MDiffAt f y
Tactic: replace hd : ∀ᶠ y in 𝓝 x, MDiffAt f y :=
      (eventually_mem_nhds_iff.2 (ho.mem_nhds hx.1)).mono fun z ↦ hd.mdifferentiableAt
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ U ⊆ V
have hVo : IsOpen[inst_6] V
Tactic: have hVo : IsOpen V := by
    refine isOpen_iff_mem_nhds.2 fun x hx ↦ inter_mem (ho.mem_nhds hx.1) ?_
    replace hm : IsLocalMax (‖f ·‖) x :=
      mem_of_superset (ho.mem_nhds hx.1) fun z hz ↦ (hm hz).out.trans_eq hx.2.symm
    replace hd : ∀ᶠ y in 𝓝 x, MDiffAt f y :=
      (eventually_mem_nhds_iff.2 (ho.mem_nhds hx.1)).mono fun z ↦ hd.mdifferentiableAt
    exact (Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax hd hm).mono fun _ ↦
      (Eq.trans · hx.2)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen[inst_6] V
⊢ U ⊆ V
have hVne : (U ∩ V).Nonempty
Tactic: have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, rfl⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen[inst_6] V
hVne : (U ∩ V).Nonempty
W : Set M := U ∩ {z : M | ‖f z‖ = ‖f c‖}ᶜ
⊢ U ⊆ V
have hWo : IsOpen[inst_6] W
Tactic: have hWo : IsOpen W := hd.continuousOn.norm.isOpen_inter_preimage ho isOpen_ne
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen[inst_6] V
hVne : (U ∩ V).Nonempty
W : Set M := U ∩ {z : M | ‖f z‖ = ‖f c‖}ᶜ
hWo : IsOpen[inst_6] W
⊢ U ⊆ V
have hdVW : Disjoint V W
Tactic: have hdVW : Disjoint V W := disjoint_compl_right.mono inf_le_right inf_le_right
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst_6] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z : M | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen[inst_6] V
hVne : (U ∩ V).Nonempty
W : Set M := U ∩ {z : M | ‖f z‖ = ‖f c‖}ᶜ
hWo : IsOpen[inst_6] 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 (.intro hx) (.intro hx)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
a b : M
hd : MDiff[U] f
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
⊢ f a = f b
have inr : ∀ (this : ∀ {f : M → F} (hd : MDiff[U] f) (hb₀ : f b = 0), f a = f b) (hb₀ : ¬f b = 0), f a = f b
Tactic: wlog hb₀ : f b = 0 generalizing f
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
a b : M
hd : MDiff[U] f
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
inr : ∀ (this : ∀ {f : M → F} (hd : MDiff[U] f) (hb₀ : f b = 0), f a = f b) (hb₀ : ¬f b = 0), f a = f b
⊢ f a = f b
have wlog : ∀ {f : M → F} (hd : MDiff[U] f) (hb₀ : f b = 0), f a = f b
Tactic: wlog hb₀ : f b = 0 generalizing f
Cleared hypotheses: f, hd
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
U : Set M
a b : M
hd : MDiff[U] f
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
this : ∀ {f : M → F} (hd : MDiff[U] f) (hb₀ : f b = 0), f a = f b
hb₀ : ¬f b = 0
⊢ f a = f b
have hd' : MDiff[U] fun (x : M) ↦ f x - f b
Tactic: have hd' : MDiff[U] (f · - f b) := fun x hx ↦
      ⟨(hd x hx).1.sub continuousWithinAt_const, (hd x hx).2.sub_const _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
⊢ f a = f b
have rcases : ∀ (c : M) (hcU : c ∈ U) (hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c), f a = f b
Tactic: rcases hc.exists_isMaxOn ⟨a, ha⟩ hd.continuousOn.norm with ⟨c, hcU, hc⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc_1 : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c
⊢ f a = f b
have this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
Tactic: have : ∀ x ∈ U, ‖f x‖ = ‖f c‖ :=
    norm_eqOn_of_isPreconnected_of_isMaxOn hd hpc ho hcU hc
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc_1 : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
⊢ f a = f b
have rw : f a = 0
Tactic: rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc_1 : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
rw : f a = 0
⊢ f a = f b
have rw₁ : ‖f a‖ = 0
Tactic: rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc_1 : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
rw : f a = 0
rw₁ : ‖f a‖ = 0
⊢ f a = f b
have rw₂ : ‖f c‖ = 0
Tactic: rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc_1 : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
rw : f a = 0
rw₁ : ‖f a‖ = 0
rw₂ : ‖f c‖ = 0
⊢ f a = f b
have rw₃ : ‖f b‖ = 0
Tactic: rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc_1 : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
rw : f a = 0
rw₁ : ‖f a‖ = 0
rw₂ : ‖f c‖ = 0
rw₃ : ‖f b‖ = 0
⊢ f a = f b
have rw₄ : norm.{u_2} (E := F) 0 = 0
Tactic: rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]