awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ writtenInExtChartAt (M := M ⊕ M') I I (Sum.inr x) Sum.swap y = id y
have simp : Function.comp (β := M' ⊕ M)
    (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I) : M' ⊕ M → E)
    (Sum.swap ∘
      (↑(PartialEquiv.symm
            (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I)) :
        E → M ⊕ M'))
    y =
  id y
Tactic: simp only [writtenInExtChartAt, extChartAt, Sum.swap_inr,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ 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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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)
      (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
have rw : (↑I : H → E) ((↑I.symm : E → H) y) = y
Tactic: rw [Sum.inl_injective.extend_apply, (chartAt H x).right_inv (by grind)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
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)
⊢ 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
have this : 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)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ 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
have apply : t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))
Tactic: apply Filter.eventually_of_mem ?_ this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ t ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr x))
have 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))
Tactic: rw [Filter.inter_mem_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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))
have 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))))
Tactic: refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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)] (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)] id
have 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
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)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ writtenInExtChartAt I I p Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)] id
have 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
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)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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'
⊢ HasMFDerivAt I I Sum.swap p (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
have refine : HasFDerivWithinAt (writtenInExtChartAt I I p Sum.swap) (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
  (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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'
⊢ HasFDerivWithinAt (writtenInExtChartAt I I p Sum.swap) (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
    (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)
have h₁ : writtenInExtChartAt I I p Sum.swap =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I p) : M ⊕ M' → E) p] id
Tactic: apply (hasFDerivWithinAt_id _ (range I)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ HasFDerivWithinAt (writtenInExtChartAt I I p Sum.swap) (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
    (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)
have hx : writtenInExtChartAt I I p Sum.swap ((↑(extChartAt I p) : M ⊕ M' → E) p) = id ((↑(extChartAt I p) : M ⊕ M' → E) p)
Tactic: apply (hasFDerivWithinAt_id _ (range I)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 ((↑(extChartAt I p) : M ⊕ M' → E) p) = id ((↑(extChartAt I p) : M ⊕ M' → E) p)
have hx : (↑I : H → E) ((↑(chartAt H p.swap) : M' ⊕ M → H) p.swap) = (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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'
⊢ (↑I : H → E) ((↑(chartAt H p.swap) : M' ⊕ M → H) p.swap) = (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)
have 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))
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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))
⊢ (↑I : H → E) ((↑(chartAt H p.swap) : M' ⊕ M → H) p.swap) = (↑I : H → E) ((↑(chartAt H p) : M ⊕ M' → H) p)
have 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))
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
have rw : (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q)).target ∈
  𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q
Tactic: rw [← I.image_eq (chartAt H q).target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
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
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q] id
have 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
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)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I q) : M → E) q] id
have 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
Tactic: filter_upwards [hmem] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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)
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl y = id y
have 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)
Tactic: rcases hy with ⟨hyT, ⟨z, rfl⟩⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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'
have rw : (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∈
  𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'
Tactic: rw [← I.image_eq (chartAt H q').target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
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'
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'] id
have 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'
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')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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'
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'] id
have 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
Tactic: filter_upwards [hmem] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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)
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr y = id y
have 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.inr ((↑I : H → E) z) = id ((↑I : H → E) z)
Tactic: rcases hy with ⟨hyT, ⟨z, rfl⟩⟩
Cleared hypotheses: y, hy