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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
v : TangentSpace (I.prod I') p
hf : MDiffAt f p
⊢ (HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2))) (β :=
          TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I p.1)
              ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1) (id (ContinuousLinearMap.fst 𝕜 E E')) :
            TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I' p.2)
              ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2) (id (ContinuousLinearMap.snd 𝕜 E E')) :
            TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2))) :
        (a : TangentSpace (I.prod I') p) → TangentSpace I'' (f p))
      v =
    HAdd.hAdd (α := TangentSpace I'' (f (p.1, p.2))) (β := TangentSpace I'' (f (p.1, p.2)))
      ((((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1 :
              ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I p.1)
                (TangentSpace I'' (f (p.1, p.2)))) :
            (a : TangentSpace I p.1) → TangentSpace I'' (f (p.1, p.2)))
          v.1 :
        TangentSpace I'' (f (p.1, p.2)))
      ((((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2 :
              ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' p.2)
                (TangentSpace I'' (f (p.1, p.2)))) :
            (a : TangentSpace I' p.2) → TangentSpace I'' (f (p.1, p.2)))
          v.2 :
        TangentSpace I'' (f (p.1, p.2)))

Tactic:
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'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
y : E
hy : y ∈ t
simp :
  Function.comp (β := M' ⊕ M)
      (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M' ⊕ M → E)
      (Sum.swap ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
          E → M ⊕ M'))
      y =
    id y
⊢ writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x) Sum.swap y = id y

Tactic:
simp only [writtenInExtChartAt, extChartAt, Sum.swap_inl,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, ChartedSpace.sum_chartAt_inl, writtenInExtChartAt, Sum.swap_inl
-- 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)
y : E
hy : y ∈ t
dsimp :
  (↑I : H → E)
      (Function.extend Sum.inr (↑(chartAt H x) : M → H) (fun (x_1 : M' ⊕ M) ↦ Classical.arbitrary H)
        (Sum.inr ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)))) =
    y
⊢ Function.comp (β := M' ⊕ M)
      (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M' ⊕ M → E)
      (Sum.swap ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
          E → M ⊕ M'))
      y =
    id y

Tactic:
dsimp
-- 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)
y : E
hy : y ∈ t
⊢ (↑I.symm : E → H) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
grind
-- 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)
y : E
hy : y ∈ t
rw : (↑I : H → E) ((↑I.symm : E → H) y) = y
⊢ (↑I : H → E)
      (Function.extend Sum.inr (↑(chartAt H x) : M → H) (fun (x_1 : M' ⊕ M) ↦ Classical.arbitrary H)
        (Sum.inr ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)))) =
    y

Tactic:
rw [Sum.inr_injective.extend_apply, (chartAt H x).right_inv (by grind)]

Premises used: Sum.inr_injective, chartAt, Function.Injective.extend_apply, 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'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
y : E
hy : y ∈ t
⊢ y ∈ range (↑I : H → E)

Tactic:
grind
-- 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)
y : E
hy : y ∈ t
⊢ (↑I : H → E) ((↑I.symm : E → H) y) = y

Tactic:
exact I.right_inv (by grind)

Premises used: ModelWithCorners.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'
x : M
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
⊢ EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inl x) Sum.swap) id t

Tactic:
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)
-- 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.inl x) Sum.swap) id t
apply : t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))
⊢ 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

Tactic:
apply Filter.eventually_of_mem ?_ this

Premises used: Filter.eventually_of_mem
-- 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.inl x) Sum.swap) id t
rw :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
      𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x)) ∧
    range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))
⊢ t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))

Tactic:
rw [Filter.inter_mem_iff]

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'
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.inl x) Sum.swap) id t
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
      𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x)) ∧
    range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))

Tactic:
⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin, ModelWithCorners.continuousWithinAt_symm, self_mem_nhdsWithin, And.intro
-- 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.inl x) Sum.swap) id t
refine :
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x))))
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
      𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl x)) ∧
    range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl 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.inl x) Sum.swap) id t
⊢ (↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl 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.inl x) Sum.swap) id t
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl 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'
x : M'
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
y : E
hy : y ∈ t
simp :
  Function.comp (β := M' ⊕ M)
      (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M' ⊕ M → E)
      (Sum.swap ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
          E → M ⊕ M'))
      y =
    id y
⊢ writtenInExtChartAt (M := M ⊕ M') I I (Sum.inr x) Sum.swap y = id y

Tactic:
simp only [writtenInExtChartAt, extChartAt, Sum.swap_inr,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, Sum.swap_inr, ChartedSpace.sum_chartAt_inl, writtenInExtChartAt
-- 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)
y : E
hy : y ∈ t
dsimp :
  (↑I : H → E)
      (Function.extend Sum.inl (↑(chartAt H x) : M' → H) (fun (x_1 : M' ⊕ M) ↦ Classical.arbitrary H)
        (Sum.inl ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M') ((↑I.symm : E → H) y)))) =
    y
⊢ Function.comp (β := M' ⊕ M)
      (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M' ⊕ M → E)
      (Sum.swap ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
          E → M ⊕ M'))
      y =
    id y

Tactic:
dsimp
-- 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)
y : E
hy : y ∈ t
⊢ (↑I.symm : E → H) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
grind
-- 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)
y : E
hy : y ∈ t
rw : (↑I : H → E) ((↑I.symm : E → H) y) = y
⊢ (↑I : H → E)
      (Function.extend Sum.inl (↑(chartAt H x) : M' → H) (fun (x_1 : M' ⊕ M) ↦ Classical.arbitrary H)
        (Sum.inl ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M') ((↑I.symm : E → H) y)))) =
    y

Tactic:
rw [Sum.inl_injective.extend_apply, (chartAt H x).right_inv (by grind)]

Premises used: chartAt, Sum.inl_injective, Function.Injective.extend_apply, 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'
x : M'
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
y : E
hy : y ∈ t
⊢ y ∈ range (↑I : H → E)

Tactic:
grind
-- 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)
y : E
hy : y ∈ t
⊢ (↑I : H → E) ((↑I.symm : E → H) y) = y

Tactic:
exact I.right_inv (by grind)

Premises used: ModelWithCorners.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'
x : M'
t : Set E := (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
⊢ EqOn (writtenInExtChartAt (M := M ⊕ M') I I (Sum.inr x) Sum.swap) id t

Tactic:
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)
-- 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
apply : t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))
⊢ 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

Tactic:
apply Filter.eventually_of_mem ?_ this

Premises used: Filter.eventually_of_mem
-- 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
rw :
  (↑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))
⊢ t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))

Tactic:
rw [Filter.inter_mem_iff]

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'
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) ⁻¹' (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:
⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin, ModelWithCorners.continuousWithinAt_symm, self_mem_nhdsWithin, And.intro