awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inr x) Sum.swap) id t
refine :
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))))
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
      𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x)) ∧
    range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))

Tactic:
refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inr x) Sum.swap) id t
⊢ (↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
this : EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inr x) Sum.swap) id t
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))))

Tactic:
exact (chartAt H x).open_target.mem_nhds (by simp)

Premises used: chartAt, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
inl :
  ∀ (x : M),
    writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x)
        Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))]
      id
inr :
  ∀ (x : M'),
    writtenInExtChartAt (M := M ⊕ M') I I (Sum.inr x)
        Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))]
      id
⊢ writtenInExtChartAt I I p Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)] id

Tactic:
cases p with
    | inl x =>
      let t := I.symm ⁻¹' (chartAt H x).target ∩ range I
      have : EqOn (writtenInExtChartAt I I (Sum.inl x) (@Sum.swap M M')) id t := by
        intro y hy
        simp only [writtenInExtChartAt, extChartAt, Sum.swap_inl,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]
        dsimp
        rw [Sum.inr_injective.extend_apply, (chartAt H x).right_inv (by grind)]
        exact I.right_inv (by grind)
      apply Filter.eventually_of_mem ?_ this
      rw [Filter.inter_mem_iff]
      refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩
      exact (chartAt H x).open_target.mem_nhds (by simp)
    | inr x =>
      let t := I.symm ⁻¹' (chartAt H x).target ∩ range I
      have : EqOn (writtenInExtChartAt I I (Sum.inr x) (@Sum.swap M M')) id t := by
        intro y hy
        simp only [writtenInExtChartAt, extChartAt, Sum.swap_inr,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]
        dsimp
        rw [Sum.inl_injective.extend_apply, (chartAt H x).right_inv (by grind)]
        exact I.right_inv (by grind)
      apply Filter.eventually_of_mem ?_ this
      rw [Filter.inter_mem_iff]
      refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩
      exact (chartAt H x).open_target.mem_nhds (by simp)

Premises used: Filter.inter_mem_iff
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
⊢ ContinuousAt Sum.swap p

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
refine :
  HasFDerivWithinAt (writtenInExtChartAt I I p Sum.swap) (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
    (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)
⊢ HasMFDerivAt I I Sum.swap p (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
h₁ : writtenInExtChartAt I I p Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I p) : M ⊕ M' → E) p] id
hx : writtenInExtChartAt I I p Sum.swap ((↑(extChartAt I p) : M ⊕ M' → E) p) = id ((↑(extChartAt I p) : M ⊕ M' → E) p)
⊢ HasFDerivWithinAt (writtenInExtChartAt I I p Sum.swap) (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
    (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)

Tactic:
apply (hasFDerivWithinAt_id _ (range I)).congr_of_eventuallyEq

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, ModelWithCorners.toFun', Set.range, hasFDerivWithinAt_id
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
⊢ writtenInExtChartAt I I p Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I p) : M ⊕ M' → E) p] id

Tactic:
writtenInExtChartAt_sumSwap_eventuallyEq_id

Premises used: OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', writtenInExtChartAt_sumSwap_eventuallyEq_id
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
⊢ writtenInExtChartAt I I p Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I p) : M ⊕ M' → E) p] id

Tactic:
exact writtenInExtChartAt_sumSwap_eventuallyEq_id

Premises used: writtenInExtChartAt_sumSwap_eventuallyEq_id
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
hx : (↑I : H → E) ((↑(chartAt H p.swap) : M' ⊕ M → H) p.swap) = (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)
⊢ writtenInExtChartAt I I p Sum.swap ((↑(extChartAt I p) : M ⊕ M' → E) p) = id ((↑(extChartAt I p) : M ⊕ M' → E) p)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
hx :
  ∀ (val : M),
    (↑I : H → E) ((↑(chartAt H (Sum.swap (Sum.inl val))) : M' ⊕ M → H) (Sum.swap (Sum.inl val))) =
      (↑I : H → E) ((↑(chartAt H (Sum.inl val)) : M ⊕ M' → H) (Sum.inl val))
hx₁ :
  ∀ (val : M'),
    (↑I : H → E) ((↑(chartAt H (Sum.swap (Sum.inr val))) : M' ⊕ M → H) (Sum.swap (Sum.inr val))) =
      (↑I : H → E) ((↑(chartAt H (Sum.inr val)) : M ⊕ M' → H) (Sum.inr val))
⊢ (↑I : H → E) ((↑(chartAt H p.swap) : M' ⊕ M → H) p.swap) = (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)

Tactic:
cases p
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
val : M
⊢ (↑I : H → E) ((↑(chartAt H (Sum.swap (Sum.inl val))) : M' ⊕ M → H) (Sum.swap (Sum.inl val))) =
    (↑I : H → E) ((↑(chartAt H (Sum.inl val)) : M ⊕ M' → H) (Sum.inl val))

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
val : M'
⊢ (↑I : H → E) ((↑(chartAt H (Sum.swap (Sum.inr val))) : M' ⊕ M → H) (Sum.swap (Sum.inr val))) =
    (↑I : H → E) ((↑(chartAt H (Sum.inr val)) : M ⊕ M' → H) (Sum.inr val))

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
s : Set (M ⊕ M')
hs : UniqueMDiffWithinAt I s p
⊢ Eq (α := TangentSpace I p →L[𝕜] TangentSpace I p.swap) (mfderivWithin I I Sum.swap s p)
    (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
hasMFDerivAt_sumSwap.hasMFDerivWithinAt.mfderivWithin hs

Premises used: hasMFDerivAt_sumSwap, HasMFDerivWithinAt.mfderivWithin, HasMFDerivAt.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
⊢ Eq (α := TangentSpace I p →L[𝕜] TangentSpace I p.swap) (mfderiv% Sum.swap p)
    (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
simpa [mfderivWithin_univ] using (mfderivWithin_sumSwap (uniqueMDiffWithinAt_univ I))

Premises used: mfderivWithin_univ, uniqueMDiffWithinAt_univ, mfderivWithin_sumSwap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
rw :
  (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q

Tactic:
rw [← I.image_eq (chartAt H q).target]

Premises used: ModelWithCorners.image_eq, chartAt, PartialEquiv.target, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
⊢ (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q

Tactic:
(chartAt H q).extend_image_target_mem_nhds (mem_chart_source H q)

Premises used: mem_chart_source, chartAt, Set.Mem, setOf, OpenPartialHomeomorph.extend_image_target_mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
⊢ (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q

Tactic:
exact (chartAt H q).extend_image_target_mem_nhds (mem_chart_source H q)

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.extend_image_target_mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q

Tactic:
have hmem : I.symm ⁻¹'
      (chartAt H q).target ∩ Set.range I ∈ 𝓝[Set.range I] (extChartAt I q q) := by
    rw [← I.image_eq (chartAt H q).target]
    exact (chartAt H q).extend_image_target_mem_nhds (mem_chart_source H q)
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q
h :
  ∀ (y : E)
    (hy : y ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E)),
    writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl y = id y
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q] id

Tactic:
filter_upwards [hmem] with y hy
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E)
h :
  ∀ (z : H) (hyT : (↑I : H → E) z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target),
    writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl ((↑I : H → E) z) = id ((↑I : H → E) z)
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl y = id y

Tactic:
rcases hy with ⟨hyT, ⟨z, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q
z : H
hyT : (↑I : H → E) z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target
⊢ z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target

Tactic:
simpa [Set.mem_preimage, I.left_inv] using hyT

Premises used: ModelWithCorners.left_inv, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q
z : H
hyT : (↑I : H → E) z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl ((↑I : H → E) z) = id ((↑I : H → E) z)

Tactic:
simp [writtenInExtChartAt, extChartAt, ChartedSpace.sum_chartAt_inl,
    Sum.inl_injective.extend_apply <| chartAt H q,
    (chartAt H q).right_inv (by simpa [Set.mem_preimage, I.left_inv] using hyT)]

Premises used: extChartAt, chartAt, Sum.inl_injective, ChartedSpace.sum_chartAt_inl, Function.Injective.extend_apply, writtenInExtChartAt, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
rw :
  (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'

Tactic:
rw [← I.image_eq (chartAt H q').target]

Premises used: ModelWithCorners.image_eq, chartAt, PartialEquiv.target, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
⊢ (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'

Tactic:
(chartAt H q').extend_image_target_mem_nhds (mem_chart_source H q')

Premises used: mem_chart_source, chartAt, Set.Mem, setOf, OpenPartialHomeomorph.extend_image_target_mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
⊢ (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'

Tactic:
exact (chartAt H q').extend_image_target_mem_nhds (mem_chart_source H q')

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.extend_image_target_mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'

Tactic:
have hmem : I.symm ⁻¹'
      (chartAt H q').target ∩ Set.range I ∈ 𝓝[Set.range I] (extChartAt I q' q') := by
    rw [← I.image_eq (chartAt H q').target]
    exact (chartAt H q').extend_image_target_mem_nhds (mem_chart_source H q')
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'
h :
  ∀ (y : E)
    (hy : y ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E)),
    writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr y = id y
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'] id

Tactic:
filter_upwards [hmem] with y hy