awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
U : Set M
a b : M
hpc : IsPreconnected U
hc_1 : IsCompact U
ho : IsOpen[inst_6] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (β := ℝ) (fun (x : M) ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
rw : f a = 0
rw₁ : ‖f a‖ = 0
rw₂ : ‖f c‖ = 0
rw₃ : ‖f b‖ = 0
rw₄ : norm.{u_2} (E := F) 0 = 0
⊢ f a = f b
have rw₅ : Eq (α := ℝ) 0 0
Tactic: rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : H
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑I : H → E) x
have refine : ContDiffWithinAt 𝕜 n
  ((↑(extChartAt 𝓘(𝕜, E) ((↑I : H → E) x)) : E → E) ∘ (↑I : H → E) ∘ (↑(extChartAt I x).symm : E → H))
  (range (↑I : H → E)) ((↑(extChartAt I x) : H → E) x)
Tactic: refine contMDiffAt_iff.mpr ⟨I.continuousAt, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : H
⊢ ContDiffWithinAt 𝕜 n
    ((↑(extChartAt 𝓘(𝕜, E) ((↑I : H → E) x)) : E → E) ∘ (↑I : H → E) ∘ (↑(extChartAt I x).symm : E → H))
    (range (↑I : H → E)) ((↑(extChartAt I x) : H → E) x)
have simp : ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : H
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
have refine_1 : (↑I : H → E) ∘ (↑I.symm : E → H) =ᶠ[nhdsWithin ((↑I : H → E) x) (range (↑I : H → E))] id
Tactic: refine contDiffWithinAt_id.congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : H
refine_1 : (↑I : H → E) ∘ (↑I.symm : E → H) =ᶠ[nhdsWithin ((↑I : H → E) x) (range (↑I : H → E))] id
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
have refine_2 : ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = id ((↑I : H → E) x)
Tactic: refine contDiffWithinAt_id.congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : H
⊢ ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = id ((↑I : H → E) x)
have refine_2 : (↑I : H → E) ((↑I.symm : E → H) ((↑I : H → E) x)) = id ((↑I : H → E) x)
Tactic: simp_rw [Function.comp_apply, I.left_inv, Function.id_def]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : H
refine_2 : (↑I : H → E) ((↑I.symm : E → H) ((↑I : H → E) x)) = id ((↑I : H → E) x)
⊢ ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = id ((↑I : H → E) x)
have refine_2₁ : (↑I : H → E) x = id ((↑I : H → E) x)
Tactic: simp_rw [Function.comp_apply, I.left_inv, Function.id_def]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑I.symm : E → H) (range (↑I : H → E))
have rw : ContinuousOn (↑I.symm : E → H) (range (↑I : H → E)) ∧
  ∀ (x : E) (y : H),
    ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ (↑I.symm : E → H) ∘ (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E))
      ((extChartAt 𝓘(𝕜, E) x).target ∩
        (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E) ⁻¹' (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (extChartAt I y).source))
Tactic: rw [contMDiffOn_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
⊢ ContinuousOn (↑I.symm : E → H) (range (↑I : H → E)) ∧
    ∀ (x : E) (y : H),
      ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ (↑I.symm : E → H) ∘ (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E))
        ((extChartAt 𝓘(𝕜, E) x).target ∩
          (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E) ⁻¹'
            (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (extChartAt I y).source))
have refine : ∀ (x : E) (y : H),
  ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ (↑I.symm : E → H) ∘ (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E))
    ((extChartAt 𝓘(𝕜, E) x).target ∩
      (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E) ⁻¹' (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (extChartAt I y).source))
Tactic: refine ⟨I.continuousOn_symm, fun x y => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : E
y : H
⊢ ContDiffOn 𝕜 n ((↑(extChartAt I y) : H → E) ∘ (↑I.symm : E → H) ∘ (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E))
    ((extChartAt 𝓘(𝕜, E) x).target ∩
      (↑(extChartAt 𝓘(𝕜, E) x).symm : E → E) ⁻¹' (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (extChartAt I y).source))
have simp : ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E))
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑(extChartAt I x) : M → E) x
have rw : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M))
  (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: rw [contMDiffAt_iff_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M))
    (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have apply : (↑(extChartAt I x) : M → E) ∘
    (↑(extChartAt I x).symm : E → M) =ᶠ[nhdsWithin ((↑(extChartAt I x) : M → E) x) (range (↑I : H → E))]
  id
Tactic: apply contMDiffWithinAt_id.congr_of_eventuallyEq_of_mem _ (by simp)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ (↑(extChartAt I x) : M → E) ∘
      (↑(extChartAt I x).symm : E → M) =ᶠ[nhdsWithin ((↑(extChartAt I x) : M → E) x) (range (↑I : H → E))]
    id
have h : ∀ (y : E) (hy : y ∈ (extChartAt I x).target), ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = id y
Tactic: filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑(e.extend I).symm : E → M) ((↑I : H → E) '' e.target)
have refine : (↑I : H → E) '' e.target ⊆ (↑(I.restr e.target).symm : E → H) ⁻¹' e.target
Tactic: refine (contMDiffOn_symm_of_mem_maximalAtlas he).comp
    (contMDiffOn_model_symm.mono <| image_subset_range _ _) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
⊢ (↑I : H → E) '' e.target ⊆ (↑(I.restr e.target).symm : E → H) ⁻¹' e.target
have simp_rw : e.target ⊆ e.target
Tactic: simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.toPartialEquiv_coe_symm,
    preimage_preimage, I.left_inv, preimage_id']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
x : M
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑(extChartAt I x).symm : E → M) (extChartAt I x).target
have h : (extChartAt I x).target = (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
Tactic: convert! contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
x : M
⊢ (extChartAt I x).target = (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
have h : (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) =
  (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
Tactic: rw [extChartAt_target, I.image_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
x : M
h :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) =
    (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ (extChartAt I x).target = (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
have h₁ : (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) =
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)
Tactic: rw [extChartAt_target, I.image_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I n (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
have rw : ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x) ∧
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
    ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
      (↑(extChartAt I x).symm : E → M))
    (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
Tactic: rw [contMDiffWithinAt_iff_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x) ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
      ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
have left : ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
left : ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x) ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
      ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
have right : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
  ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
    (↑(extChartAt I x).symm : E → M))
  (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
have left : ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
Tactic: apply ContinuousAt.continuousWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
have apply : ContinuousAt.{u_3, u_4} (Y := M) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).2
  ((↑I.symm : E → H) ((↑(extChartAt I x) : M → E) x))
Tactic: apply ContinuousAt.comp _ I.continuousAt_symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
    ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
      (↑(extChartAt I x).symm : E → M))
    (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
have apply : ∀ (y : E) (hy : y ∈ (extChartAt I x).target),
  ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      y =
    id y
Tactic: apply contMDiffWithinAt_id.congr_of_mem (fun y hy ↦ ?_) (by simp)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      y =
    id y
have h : ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
      (↑(extChartAt I x).symm : E → M))
    y =
  (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
Tactic: convert! PartialEquiv.right_inv (extChartAt I x) hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
⊢ ContMDiffOn I I n (↑f : M → M') f.source
have h : ∀ x ∈ f.source, ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
Tactic: apply contMDiffOn_of_locally_contMDiffOn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
⊢ ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
have hxf : (contDiffGroupoid n I).IsLocalStructomorphWithinAt
  ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
Tactic: obtain ⟨-, hxf⟩ := hf x hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
⊢ ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
have h : ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ contDiffGroupoid n I)
  (he' :
    EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source))
  (hex : (↑c : M → H) x ∈ e.source), ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
Tactic: obtain
    ⟨e, he, he' : EqOn (c' ∘ f ∘ c.symm) e (c.symm ⁻¹' f.source ∩ e.source), hex :
      c x ∈ e.source⟩ :=
    hxf (by simp only [hx, mfld_simps])
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
have h : x ∈ s
Tactic: refine ⟨s, (f.trans c').open_source.inter ((c.trans e).trans c'.symm).open_source, ?_, ?_⟩