awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
refine_2 : ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = id ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
refine contDiffWithinAt_id.congr_of_eventuallyEq ?_ ?_

Premises used: ContDiffWithinAt.congr_of_eventuallyEq, contDiffWithinAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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) =ᶠ[nhdsWithin ((↑I : H → E) x) (range (↑I : H → E))] id

Tactic:
Filter.eventuallyEq_of_mem self_mem_nhdsWithin fun x₂ => I.right_inv

Premises used: Filter.eventuallyEq_of_mem, ModelWithCorners.right_inv, self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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) =ᶠ[nhdsWithin ((↑I : H → E) x) (range (↑I : H → E))] id

Tactic:
exact Filter.eventuallyEq_of_mem self_mem_nhdsWithin fun x₂ => I.right_inv

Premises used: Filter.eventuallyEq_of_mem, ModelWithCorners.right_inv, self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)
refine_2₁ : (↑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)

Tactic:
simp_rw [Function.comp_apply, I.left_inv, Function.id_def]

Premises used: Function.id_def, Function.comp_apply, ModelWithCorners.left_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 : ℕ∞ω
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))
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑I.symm : E → H) (range (↑I : H → E))

Tactic:
rw [contMDiffOn_iff]

Premises used: contMDiffOn_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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))

Tactic:
⟨I.continuousOn_symm, fun x y => ?_⟩

Premises used: ModelWithCorners.continuousOn_symm, And.intro
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 : ℕ∞ω
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))
⊢ 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:
refine ⟨I.continuousOn_symm, fun x y => ?_⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
simp : ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E))
⊢ 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:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E))

Tactic:
contDiffOn_id.congr fun x' => I.right_inv

Premises used: ContDiffOn.congr, ModelWithCorners.right_inv, contDiffOn_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E))

Tactic:
exact contDiffOn_id.congr fun x' => I.right_inv

Premises used: ContDiffOn.congr, ModelWithCorners.right_inv, contDiffOn_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
⊢ ContMDiffOn I I n (↑e : M → H) e.source

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropOn_of_mem_maximalAtlas
    contDiffWithinAtProp_id h

Premises used: ContMDiffWithinAt, contDiffWithinAtProp_id, ChartedSpace.LiftPropOn, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
⊢ ContMDiffOn I I n (↑e.symm : H → M) e.target

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropOn_symm_of_mem_maximalAtlas
      contDiffWithinAtProp_id h

Premises used: ContMDiffWithinAt, contDiffWithinAtProp_id, ChartedSpace.LiftPropOn, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
x : M
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hx : x ∈ e.source
⊢ ContMDiffAt I I n (↑e : M → H) x

Tactic:
(contMDiffOn_of_mem_maximalAtlas h).contMDiffAt <| e.open_source.mem_nhds hx

Premises used: OpenPartialHomeomorph.open_source, ContMDiffOn.contMDiffAt, IsOpen.mem_nhds, contMDiffOn_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
x : H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hx : x ∈ e.target
⊢ ContMDiffAt I I n (↑e.symm : H → M) x

Tactic:
(contMDiffOn_symm_of_mem_maximalAtlas h).contMDiffAt <| e.open_target.mem_nhds hx

Premises used: ContMDiffOn.contMDiffAt, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target, contMDiffOn_symm_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 I I n (↑(chartAt H x) : M → H) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
contMDiffOn_of_mem_maximalAtlas <| chart_mem_maximalAtlas x

Premises used: IsManifold.chart_mem_maximalAtlas, contMDiffOn_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 I I n (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
contMDiffOn_symm_of_mem_maximalAtlas <| chart_mem_maximalAtlas x

Premises used: IsManifold.chart_mem_maximalAtlas, contMDiffOn_symm_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
x : M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hx : x ∈ e.source
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑(e.extend I) : M → E) x

Tactic:
(contMDiff_model _).comp x <| contMDiffAt_of_mem_maximalAtlas he hx

Premises used: contMDiff_model, ModelWithCorners.toFun', contMDiffAt_of_mem_maximalAtlas, ContMDiffAt.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 I 𝓘(𝕜, E) n (↑(e.extend I) : M → E) e.source

Tactic:
fun _x' hx' ↦ (contMDiffAt_extend he hx').contMDiffWithinAt

Premises used: contMDiffAt_extend, ContMDiffAt.contMDiffWithinAt, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 x' : M
h : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑(extChartAt I x) : M → E) x'

Tactic:
contMDiffAt_extend (chart_mem_maximalAtlas x) h

Premises used: contMDiffAt_extend, IsManifold.chart_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
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)
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑(extChartAt I x) : M → E) x

Tactic:
rw [contMDiffAt_iff_source]

Premises used: contMDiffAt_iff_source
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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) x ∈ range (↑I : H → E)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
apply :
  (↑(extChartAt I x) : M → E) ∘
      (↑(extChartAt I x).symm : E → M) =ᶠ[nhdsWithin ((↑(extChartAt I x) : M → E) x) (range (↑I : H → E))]
    id
⊢ 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:
apply contMDiffWithinAt_id.congr_of_eventuallyEq_of_mem _ (by simp)

Premises used: ContMDiffWithinAt.congr_of_eventuallyEq_of_mem, contMDiffWithinAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
h :
  ∀ (y : E) (hy : y ∈ (extChartAt I x).target),
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = id y
⊢ (↑(extChartAt I x) : M → E) ∘
      (↑(extChartAt I x).symm : E → M) =ᶠ[nhdsWithin ((↑(extChartAt I x) : M → E) x) (range (↑I : H → E))]
    id

Tactic:
filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy

Premises used: extChartAt_target_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = id y

Tactic:
PartialEquiv.right_inv (extChartAt I x) hy

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = id y

Tactic:
exact PartialEquiv.right_inv (extChartAt I x) hy

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 I 𝓘(𝕜, E) n (↑(extChartAt I x) : M → E) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
fun _x' hx' => (contMDiffAt_extChartAt' hx').contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, contMDiffAt_extChartAt', ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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)

Tactic:
(contMDiffOn_symm_of_mem_maximalAtlas he).comp
    (contMDiffOn_model_symm.mono <| image_subset_range _ _) ?_

Premises used: Set.image_subset_range, OpenPartialHomeomorph.toFun', ContMDiffOn.mono, contMDiffOn_model_symm, contMDiffOn_symm_of_mem_maximalAtlas, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
refine : (↑I : H → E) '' e.target ⊆ (↑(I.restr e.target).symm : E → H) ⁻¹' e.target
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑(e.extend I).symm : E → M) ((↑I : H → E) '' e.target)

Tactic:
refine (contMDiffOn_symm_of_mem_maximalAtlas he).comp
    (contMDiffOn_model_symm.mono <| image_subset_range _ _) ?_

Premises used: Set.image_subset_range, ContMDiffOn.mono, contMDiffOn_model_symm, contMDiffOn_symm_of_mem_maximalAtlas, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
simp_rw : e.target ⊆ e.target
⊢ (↑I : H → E) '' e.target ⊆ (↑(I.restr e.target).symm : E → H) ⁻¹' e.target

Tactic:
simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.toPartialEquiv_coe_symm,
    preimage_preimage, I.left_inv, preimage_id']

Premises used: Set.preimage_preimage, Set.preimage_id', PartialEquiv.restr_coe_symm, Set.image_subset_iff, ModelWithCorners.left_inv, ModelWithCorners.toPartialEquiv_coe_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
⊢ e.target ⊆ e.target

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M)
    ((↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)

Tactic:
contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)

Premises used: IsManifold.chart_mem_maximalAtlas, contMDiffOn_extend_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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 : (extChartAt I x).target = (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
convert_1 convert_3 : IsManifold I n M
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑(extChartAt I x).symm : E → M) (extChartAt I x).target

Tactic:
convert! contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)

Premises used: IsManifold.chart_mem_maximalAtlas, contMDiffOn_extend_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
h₁ 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)
⊢ (extChartAt I x).target = (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
rw [extChartAt_target, I.image_eq]

Premises used: ModelWithCorners.image_eq, extChartAt_target
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
⊢ IsManifold I n M

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
y : E
hy : y ∈ (extChartAt I x).target
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I n (↑(extChartAt I x).symm : E → M) (extChartAt I x).target y

Tactic:
contMDiffOn_extChartAt_symm x y hy

Premises used: contMDiffOn_extChartAt_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
y : E
hy : y ∈ (extChartAt I x).target
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I n (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y

Tactic:
(contMDiffWithinAt_extChartAt_symm_target x hy).mono_of_mem_nhdsWithin
    (extChartAt_target_mem_nhdsWithin_of_mem hy)

Premises used: extChartAt_target_mem_nhdsWithin_of_mem, ContMDiffWithinAt.mono_of_mem_nhdsWithin, contMDiffWithinAt_extChartAt_symm_target