Theorem: sard_boundaryless (Sard/MainTheorem.lean)

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this : ↑(e.extend I) x' = x
⊢ ↑(e.extend I) '' e.source ∈ 𝓝 (↑(e.extend I) x')
Tactic:
have hesource : e.source ∈ 𝓝 x' := by
  have : (e.extend I).symm x = x' := rfl
  have : x' ∈ e.source := by sorry exact e.open_source.mem_nhds this
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this : ↑(e.extend I) x' = x
hesource : e.source ∈ 𝓝 x'
⊢ ↑(e.extend I) '' e.source ∈ 𝓝 (↑(e.extend I) x')

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this : ↑(e.extend I) x' = x
hesource : e.source ∈ 𝓝 x'
⊢ ↑(e.extend I) '' e.source ∈ 𝓝 (↑(e.extend I) x')
Tactic:
exact extendedChart_image_nhds_on I hesource (Eq.subset rfl)
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this : ↑(e.extend I) x' = x
⊢ e.source ∈ 𝓝 x'
Tactic:
have : (e.extend I).symm x = x' := rfl
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝¹ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this✝ : ↑(e.extend I) x' = x
this : ↑(e.extend I).symm x = x'
⊢ e.source ∈ 𝓝 x'

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝¹ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this✝ : ↑(e.extend I) x' = x
this : ↑(e.extend I).symm x = x'
⊢ e.source ∈ 𝓝 x'
Tactic:
have : x' ∈ e.source := by sorry
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this✝¹ : ↑(e.extend I) x' = x
this✝ : ↑(e.extend I).symm x = x'
this : x' ∈ e.source
⊢ e.source ∈ 𝓝 x'

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this✝¹ : ↑(e.extend I) x' = x
this✝ : ↑(e.extend I).symm x = x'
this : x' ∈ e.source
⊢ e.source ∈ 𝓝 x'
Tactic:
exact e.open_source.mem_nhds this
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝¹ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
x' : M := ↑(e.extend I).symm x
this✝ : ↑(e.extend I) x' = x
this : ↑(e.extend I).symm x = x'
⊢ x' ∈ e.source
Tactic:
sorry
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
⊢ e ∈ maximalAtlas I M
Tactic:
sorry
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
he : e ∈ maximalAtlas I M
this : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
⊢ MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
Tactic:
sorry
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
he : e ∈ maximalAtlas I M
this : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
⊢ MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
Tactic:
have : ContMDiffOn J 𝓘(ℝ, F) ∞ (J ∘ e') e'.source := extendedChart_smooth _ (chart_mem_atlas G _)
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝¹ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
he : e ∈ maximalAtlas I M
this✝ : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
this : ContMDiffOn J 𝓘(ℝ, F) ⊤ (↑J ∘ ↑e') e'.source
⊢ MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝¹ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
he : e ∈ maximalAtlas I M
this✝ : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
this : ContMDiffOn J 𝓘(ℝ, F) ⊤ (↑J ∘ ↑e') e'.source
⊢ MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
Tactic:
exact SmoothAt.mdifferentiableAt ((this.mono hw).contMDiffAt hnC)
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
he : e ∈ maximalAtlas I M
this : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
⊢ C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
    C.comp (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)
Tactic:
rw [(mfderiv_comp x hB hA)]
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
he : e ∈ maximalAtlas I M
this : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
⊢ (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
    mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) ((↑J ∘ ↑e') ∘ f ∘ e.invFun ∘ I.invFun) x
Tactic:
rw [(mfderiv_comp x hC hBA)]
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
⊢ f' x' = B
Tactic:
rw [← (hf' x' aux).mfderiv]
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝¹ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
⊢ Surjective ⇑B ↔ Surjective ⇑comp
Tactic:
have : comp = (C ∘ B) ∘ A := rfl
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : ⇑comp = (⇑C ∘ ⇑B) ∘ ⇑A
⊢ Surjective ⇑B ↔ Surjective ⇑comp

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : ⇑comp = (⇑C ∘ ⇑B) ∘ ⇑A
⊢ Surjective ⇑B ↔ Surjective ⇑comp
Tactic:
rw [this]
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : ⇑comp = (⇑C ∘ ⇑B) ∘ ⇑A
⊢ Surjective ⇑B ↔ Surjective ((⇑C ∘ ⇑B) ∘ ⇑A)

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : ⇑comp = (⇑C ∘ ⇑B) ∘ ⇑A
⊢ Surjective ⇑B ↔ Surjective ((⇑C ∘ ⇑B) ∘ ⇑A)
Tactic:
rw [hA.surjective.of_comp_iff (C ∘ B)]
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : ⇑comp = (⇑C ∘ ⇑B) ∘ ⇑A
⊢ Surjective ⇑B ↔ Surjective (⇑C ∘ ⇑B)

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : ⇑comp = (⇑C ∘ ⇑B) ∘ ⇑A
⊢ Surjective ⇑B ↔ Surjective (⇑C ∘ ⇑B)
Tactic:
rw [Surjective.of_comp_iff' hC B]
State after:
no goals

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : Surjective ⇑B ↔ Surjective ⇑comp
⊢ ¬Surjective ⇑comp
Tactic:
rw [← this]
State after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : Surjective ⇑B ↔ Surjective ⇑comp
⊢ ¬Surjective ⇑B

State before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : SmoothManifoldWithCorners I M
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : SecondCountableTopology M
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
G : Type u_5
inst✝⁸ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r✝ : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r✝ > m - n
f : M → N
hf : ContMDiff I J (↑r✝) f
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x✝ : M
e : PartialHomeomorph M H := chartAt H x✝
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝² : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r✝
he : e ∈ maximalAtlas I M
this✝¹ : ↑I '' e.target ∈ 𝓝 x
hA✝ : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
hC✝ : MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
comp : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  C.comp (B.comp A)
r : comp = D :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans (Trans.trans rfl rfl) rfl)
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    C.comp
                        ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x)) =
                      C.comp _a)
                  (mfderiv_comp x hB hA✝)))
              (Eq.refl
                (C.comp ((mfderiv I J f ((e.invFun ∘ I.invFun) x)).comp (mfderiv 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x))))))
          rfl)
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
                    (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x) =
                  _a)
              (mfderiv_comp x hC✝ hBA)))
          (Eq.refl
            ((mfderiv J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)).comp
              (mfderiv 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x)))))
      rfl)
    rfl
x' : M := ↑(e.extend I).symm x
aux : x' ∈ s
this✝ : f' x' = B
hBsurj : ¬Surjective ⇑B
hA : Bijective ⇑A
hC : Bijective ⇑C
this : Surjective ⇑B ↔ Surjective ⇑comp
⊢ ¬Surjective ⇑B
Tactic:
exact hBsurj
State after:
no goals