awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
x : H
h_1 : x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source
hx₁ :
  x ∈
    target (α := M ⊕ M')
      (OpenPartialHomeomorph.toPartialEquiv
        (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯))))
hx₂ :
  x ∈
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯)))) :
        H → M ⊕ M') ⁻¹'
      source (OpenPartialHomeomorph.toPartialEquiv (f'.lift_openEmbedding ⋯))
⊢ Membership.mem (γ := Set H) ∅ x

Tactic:
simp_all
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
x : H
⊢ x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source ↔
    Membership.mem (γ := Set H) ∅ x

Tactic:
exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all, fun hx ↦ hx.elim⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr : f.symm ≫ₕ f' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inr]

Premises used: OpenPartialHomeomorph.lift_openEmbedding_trans, Topology.IsOpenEmbedding.inr
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ f.symm ≫ₕ f' ∈ contDiffGroupoid n I

Tactic:
hM'.compatible hf hf'

Premises used: HasGroupoid.compatible
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ f.symm ≫ₕ f' ∈ contDiffGroupoid n I

Tactic:
exact hM'.compatible hf hf'

Premises used: HasGroupoid.compatible
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
e : OpenPartialHomeomorph M H
h : e.source = univ
⊢ IsManifold I n M

Tactic:
@IsManifold.mk' _ _ _ _ _ _ _ _ _ _ _ (id _) <|
    e.singleton_hasGroupoid h (contDiffGroupoid n I)

Premises used: IsManifold.mk'
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
H : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : Nonempty M
f : M → H
h : IsOpenEmbedding f
⊢ (toOpenPartialHomeomorph f h).source = univ

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I n M
s : Opens M
⊢ IsManifold.{u_1, u_2, u_3, u_4} I n ↥s

Tactic:
{ s.instHasGroupoid (contDiffGroupoid n I) with }

Premises used: contDiffGroupoid, TopologicalSpace.Opens.instHasGroupoid, IsManifold.mk
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
x : M
v : E
⊢ ∀ (x y : TangentSpace 𝓘(𝕜, E) v), x + y = x + y

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
x : M
v : E
⊢ ∀ (m : 𝕜) (x : TangentSpace 𝓘(𝕜, E) v), m • x = HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (↑(f.extend I) : M → E) = (↑I : H → E) ∘ (↑f : M → H)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (↑(f.extend I).symm : E → M) = (↑f.symm : H → M) ∘ (↑I.symm : E → H)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).source = f.source
rw₁ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' I.source = f.source
rw₂ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' univ = f.source
rw₃ : f.source ∩ univ = f.source
rw₄ rw₅ : f.source = f.source
⊢ (f.extend I).source = f.source

Tactic:
rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]

Premises used: PartialEquiv.trans_source, ModelWithCorners.source_eq, Set.inter_univ, Set.preimage_univ, OpenPartialHomeomorph.extend
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : IsOpen[inst_4] f.source
⊢ IsOpen[inst_4] (f.extend I).source

Tactic:
rw [extend_source]

Premises used: OpenPartialHomeomorph.extend_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen[inst_4] f.source

Tactic:
f.open_source

Premises used: OpenPartialHomeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen[inst_4] f.source

Tactic:
exact f.open_source

Premises used: OpenPartialHomeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
simp_rw₁ : I.target ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
simp_rw₂ : range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
simp_rw₃ : range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
⊢ (f.extend I).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)

Tactic:
simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm]

Premises used: Set.inter_comm, ModelWithCorners.target_eq, PartialEquiv.trans_target, OpenPartialHomeomorph.extend, ModelWithCorners.toPartialEquiv_coe_symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I : H → E) '' f.target
rw₁ : (↑I.toPartialEquiv : H → E) '' (I.source ∩ f.target) = (↑I : H → E) '' f.target
rw₂ : (↑I.toPartialEquiv : H → E) '' (univ ∩ f.target) = (↑I : H → E) '' f.target
rw₃ : (↑I.toPartialEquiv : H → E) '' f.target = (↑I : H → E) '' f.target
rw₄ rw₅ : (↑I : H → E) '' f.target = (↑I : H → E) '' f.target
⊢ (f.extend I).target = (↑I : H → E) '' f.target

Tactic:
rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]

Premises used: PartialEquiv.trans_target'', ModelWithCorners.source_eq, ModelWithCorners.toPartialEquiv_coe, Set.univ_inter, OpenPartialHomeomorph.extend
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (↑I : H → E) '' f.target = (↑(f.extend I) : M → E) '' f.source
rw₁ : (↑I : H → E) '' (↑f : M → H) '' f.source = (↑(f.extend I) : M → E) '' f.source
rw₂ : (↑I : H → E) ∘ (↑f : M → H) '' f.source = (↑(f.extend I) : M → E) '' f.source
rw₃ rw₄ : (↑I : H → E) ∘ (↑f : M → H) '' f.source = (↑I : H → E) ∘ (↑f : M → H) '' f.source
⊢ (f.extend I).target = (↑(f.extend I) : M → E) '' f.source

Tactic:
rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe]

Premises used: OpenPartialHomeomorph.image_source_eq_target, OpenPartialHomeomorph.extend_target', OpenPartialHomeomorph.extend_coe, Set.image_comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
rw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' f.target)
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.extend I).target

Tactic:
rw [extend_target, I.range_eq_univ, inter_univ]

Premises used: Set.inter_univ, OpenPartialHomeomorph.extend_target, ModelWithCorners.range_eq_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' f.target)

Tactic:
I.continuous_symm.isOpen_preimage _ f.open_target

Premises used: ModelWithCorners.continuous_symm, OpenPartialHomeomorph.open_target, Continuous.isOpen_preimage
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' f.target)

Tactic:
exact I.continuous_symm.isOpen_preimage _ f.open_target

Premises used: ModelWithCorners.continuous_symm, OpenPartialHomeomorph.open_target, Continuous.isOpen_preimage
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
rw : (↑I : H → E) '' (f.target ∩ (↑f.symm : H → M) ⁻¹' s) ⊆ (↑I : H → E) '' (↑f.symm : H → M) ⁻¹' s
⊢ MapsTo (↑(f.extend I) : M → E) s ((↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))

Tactic:
rw [mapsTo_iff_image_subset, extend_coe, extend_coe_symm, preimage_comp, ← I.image_eq, image_comp,
    f.image_eq_target_inter_inv_preimage hs]

Premises used: OpenPartialHomeomorph.image_eq_target_inter_inv_preimage, ModelWithCorners.image_eq, Set.mapsTo_iff_image_subset, OpenPartialHomeomorph.extend_coe_symm, Set.preimage_comp, OpenPartialHomeomorph.extend_coe, Set.image_comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ (↑I : H → E) '' (f.target ∩ (↑f.symm : H → M) ⁻¹' s) ⊆ (↑I : H → E) '' (↑f.symm : H → M) ⁻¹' s

Tactic:
image_mono inter_subset_right

Premises used: Set.image_mono, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ (↑I : H → E) '' (f.target ∩ (↑f.symm : H → M) ⁻¹' s) ⊆ (↑I : H → E) '' (↑f.symm : H → M) ⁻¹' s

Tactic:
exact image_mono inter_subset_right

Premises used: Set.image_mono, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf rwa rwa₁ rwa₂ rwa₃ : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Premises used: OpenPartialHomeomorph.extend_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
ht : t ⊆ f.source
⊢ (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) '' t = t

Tactic:
EqOn.image_eq_self (fun _ hx ↦ f.extend_left_inv (ht hx))

Premises used: OpenPartialHomeomorph.extend_left_inv, Set.EqOn.image_eq_self
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
h rwa rwa₁ rwa₂ rwa₃ : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Premises used: OpenPartialHomeomorph.extend_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
h : x ∈ f.source
⊢ (f.extend I).source ∈ 𝓝[s] x

Tactic:
mem_nhdsWithin_of_mem_nhds <| extend_source_mem_nhds f h

Premises used: OpenPartialHomeomorph.extend_source_mem_nhds, mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.extend I) : M → E) (f.extend I).source

Tactic:
I.continuous.comp_continuousOn ?_

Premises used: Continuous.comp_continuousOn, ModelWithCorners.toFun', ModelWithCorners.continuous
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
refine : ContinuousOn (↑(f.symm.restr I.source).symm : M → H) (f.extend I).source
⊢ ContinuousOn (↑(f.extend I) : M → E) (f.extend I).source

Tactic:
refine I.continuous.comp_continuousOn ?_

Premises used: Continuous.comp_continuousOn, ModelWithCorners.continuous
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : ContinuousOn (↑(f.symm.restr I.source).symm : M → H) f.source
⊢ ContinuousOn (↑(f.symm.restr I.source).symm : M → H) (f.extend I).source

Tactic:
rw [extend_source]

Premises used: OpenPartialHomeomorph.extend_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm : M → H) f.source

Tactic:
f.continuousOn

Premises used: setOf, OpenPartialHomeomorph.toFun', Set.inter, OpenPartialHomeomorph.continuousOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm : M → H) f.source

Tactic:
exact f.continuousOn

Premises used: OpenPartialHomeomorph.continuousOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
h : x ∈ f.source
⊢ ContinuousAt (↑(f.extend I) : M → E) x

Tactic:
(continuousOn_extend f).continuousAt <| extend_source_mem_nhds f h

Premises used: OpenPartialHomeomorph.extend_source_mem_nhds, OpenPartialHomeomorph.continuousOn_extend, ContinuousOn.continuousAt