awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Complex
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
x : E
⊢ f c = (f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)

Tactic:
congr_arg f (extChartAt_to_inv _).symm

Premises used: extChartAt_to_inv, congr_arg, Eq.symm
-- Module: Mathlib.Geometry.Manifold.Complex
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
x : E
⊢ f c = (f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)

Tactic:
exact congr_arg f (extChartAt_to_inv _).symm

Premises used: extChartAt_to_inv, congr_arg, Eq.symm
-- Module: Mathlib.Geometry.Manifold.Complex
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
⊢ IsLocalMax (norm ∘ f ∘ (↑e.symm : E → M)) ((↑e : M → E) c)

Tactic:
simpa only [e, IsLocalMax, IsMaxFilter, ← H₂, (· ∘ ·), extChartAt_to_inv] using hc

Premises used: extChartAt_to_inv, IsLocalMax, Function.comp, IsMaxFilter
-- Module: Mathlib.Geometry.Manifold.Complex
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‖}
suffices : U ⊆ V
⊢ EqOn (norm ∘ f) (const M ‖f c‖) U

Tactic:
suffices U ⊆ V from fun x hx ↦ (this hx).2
-- Module: Mathlib.Geometry.Manifold.Complex
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

Tactic:
isOpen_iff_mem_nhds.2 fun x hx ↦ inter_mem (ho.mem_nhds hx.1) ?_

Premises used: Iff.mpr, Filter.inter_mem, And.left, IsOpen.mem_nhds, isOpen_iff_mem_nhds
-- Module: Mathlib.Geometry.Manifold.Complex
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‖}
refine : ∀ (x : M) (hx : x ∈ V), (fun (z : M) ↦ ‖f z‖ = ‖f c‖) ∈ 𝓝 x
⊢ IsOpen[inst_6] V

Tactic:
refine isOpen_iff_mem_nhds.2 fun x hx ↦ inter_mem (ho.mem_nhds hx.1) ?_

Premises used: Iff.mpr, Filter.inter_mem, And.left, IsOpen.mem_nhds, isOpen_iff_mem_nhds
-- Module: Mathlib.Geometry.Manifold.Complex
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
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Complex
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
⊢ ∀ᶠ (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
-- Module: Mathlib.Geometry.Manifold.Complex
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
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
hd : ∀ᶠ (y : M) in 𝓝 x, MDiffAt f y
⊢ (fun (z : M) ↦ ‖f z‖ = ‖f c‖) ∈ 𝓝 x

Tactic:
(Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax hd hm).mono fun _ ↦
      (Eq.trans · hx.2)

Premises used: Set.Mem, Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax, Filter.Eventually, setOf, Filter.Eventually.mono, And.right, Eq.trans
-- Module: Mathlib.Geometry.Manifold.Complex
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
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
hd : ∀ᶠ (y : M) in 𝓝 x, MDiffAt f y
⊢ (fun (z : M) ↦ ‖f z‖ = ‖f c‖) ∈ 𝓝 x

Tactic:
exact (Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax hd hm).mono fun _ ↦
      (Eq.trans · hx.2)

Premises used: Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax, Filter.Eventually.mono, And.right, Eq.trans
-- Module: Mathlib.Geometry.Manifold.Complex
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

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)
-- Module: Mathlib.Geometry.Manifold.Complex
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).Nonempty

Tactic:
have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, rfl⟩
-- Module: Mathlib.Geometry.Manifold.Complex
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‖}ᶜ
⊢ IsOpen[inst_6] W

Tactic:
have hWo : IsOpen W := hd.continuousOn.norm.isOpen_inter_preimage ho isOpen_ne
-- Module: Mathlib.Geometry.Manifold.Complex
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
⊢ Disjoint V W

Tactic:
have hdVW : Disjoint V W := disjoint_compl_right.mono inf_le_right inf_le_right
-- Module: Mathlib.Geometry.Manifold.Complex
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 ∪ W

Tactic:
have hUVW : U ⊆ V ∪ W := fun x hx => (eq_or_ne ‖f x‖ ‖f c‖).imp (.intro hx) (.intro hx)
-- Module: Mathlib.Geometry.Manifold.Complex
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
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.Geometry.Manifold.Complex
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
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.Geometry.Manifold.Complex
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
inst_9 : StrictConvexSpace ℝ F
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
x : M
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
hd' : MDiff[U] fun (x : M) ↦ f x + f c
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + const M (f c) x‖ = ‖f x‖ + ‖const M (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.Geometry.Manifold.Complex
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

Tactic:
?_
-- Module: Mathlib.Geometry.Manifold.Complex
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
wlog : ∀ {f : M → F} (hd : MDiff[U] f) (hb₀ : f b = 0), f a = f b
⊢ f a = f b

Tactic:
wlog hb₀ : f b = 0 generalizing f
-- Module: Mathlib.Geometry.Manifold.Complex
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
⊢ 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 _⟩
-- Module: Mathlib.Geometry.Manifold.Complex
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
hd' : MDiff[U] fun (x : M) ↦ f x - f b
⊢ f a = f b

Tactic:
simpa [sub_eq_zero] using this hd' (sub_self _)

Premises used: sub_self, sub_eq_zero
-- Module: Mathlib.Geometry.Manifold.Complex
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
rcases : ∀ (c : M) (hcU : c ∈ U) (hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c), f a = f b
⊢ f a = f b

Tactic:
rcases hc.exists_isMaxOn ⟨a, ha⟩ hd.continuousOn.norm with ⟨c, hcU, hc⟩

Premises used: MDifferentiableOn.continuousOn, Exists.intro, ContinuousOn.norm, IsCompact.exists_isMaxOn
-- Module: Mathlib.Geometry.Manifold.Complex
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
⊢ ∀ 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
-- Module: Mathlib.Geometry.Manifold.Complex
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
rw₄ : norm.{u_2} (E := F) 0 = 0
rw₅ rw₆ : Eq (α := ℝ) 0 0
⊢ f a = f b

Tactic:
rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]

Premises used: norm_eq_zero, norm_zero
-- Module: Mathlib.Geometry.Manifold.Complex
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
inst_9 : CompactSpace M
f : M → F
hf : MDiff f
⊢ IsLocallyConstant f

Tactic:
haveI : LocallyConnectedSpace H := I.toHomeomorph.locallyConnectedSpace
  haveI : LocallyConnectedSpace M := ChartedSpace.locallyConnectedSpace H M
  IsLocallyConstant.of_constant_on_preconnected_clopens fun _ hpc hclo _a ha _b hb ↦
    hf.mdifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen hpc
      hclo.isClosed.isCompact hclo.isOpen hb ha

Premises used: MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen, IsClopen.isOpen, IsClopen.isClosed, IsClosed.isCompact, IsLocallyConstant.of_constant_on_preconnected_clopens, MDifferentiable.mdifferentiableOn
-- Module: Mathlib.Geometry.Manifold.Complex
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
inst_9 : CompactSpace M
inst_10 : PreconnectedSpace M
f : M → F
hf : MDiff f
a b : M
⊢ f a = f b

Tactic:
hf.isLocallyConstant.apply_eq_of_preconnectedSpace _ _

Premises used: IsLocallyConstant.apply_eq_of_preconnectedSpace, MDifferentiable.isLocallyConstant
-- Module: Mathlib.Geometry.Manifold.Complex
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
inst_9 : CompactSpace M
inst_10 : PreconnectedSpace M
f : M → F
hf : MDiff f
⊢ ∃ (v : F), f = const M v

Tactic:
hf.isLocallyConstant.exists_eq_const

Premises used: MDifferentiable.isLocallyConstant, IsLocallyConstant.exists_eq_const
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
x : H
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑I : H → E) x

Tactic:
contMDiffAt_iff.mpr ⟨I.continuousAt, ?_⟩

Premises used: Iff.mpr, contMDiffAt_iff, ModelWithCorners.continuousAt, And.intro
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
x : H
refine :
  ContDiffWithinAt 𝕜 n
    ((↑(extChartAt 𝓘(𝕜, E) ((↑I : H → E) x)) : E → E) ∘ (↑I : H → E) ∘ (↑(extChartAt I x).symm : E → H))
    (range (↑I : H → E)) ((↑(extChartAt I x) : H → E) x)
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑I : H → E) x

Tactic:
refine contMDiffAt_iff.mpr ⟨I.continuousAt, ?_⟩

Premises used: Iff.mpr, contMDiffAt_iff, ModelWithCorners.continuousAt, And.intro
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
x : H
simp : ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 n
    ((↑(extChartAt 𝓘(𝕜, E) ((↑I : H → E) x)) : E → E) ∘ (↑I : H → E) ∘ (↑(extChartAt I x).symm : E → H))
    (range (↑I : H → E)) ((↑(extChartAt I x) : H → E) x)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
x : H
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
contDiffWithinAt_id.congr_of_eventuallyEq ?_ ?_

Premises used: ContDiffWithinAt.congr_of_eventuallyEq, contDiffWithinAt_id