awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.target ×ˢ e'.target)
right :
  ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I') : ModelProd H H' → E × E') '' (e.prod e'.toPartialEquiv).target)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' (e.prod e'.toPartialEquiv).target ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))

Tactic:
rw [← (I.prod I').image_eq]

Premises used: ModelWithCorners.image_eq, ModelWithCorners.prod
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.target ×ˢ e'.target)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I') : ModelProd H H' → E × E') '' (e.prod e'.toPartialEquiv).target)

Tactic:
h3

Premises used: OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', ModelProd
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.target ×ˢ e'.target)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I') : ModelProd H H' → E × E') '' (e.prod e'.toPartialEquiv).target)

Tactic:
exact h3
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst_3] s
hes : e ≈ OpenPartialHomeomorph.ofSet s hs
apply : OpenPartialHomeomorph.ofSet s hs ∈ (contDiffGroupoid n I).members
⊢ e ∈ contDiffGroupoid n I

Tactic:
apply (contDiffGroupoid n I).mem_of_eqOnSource' _ _ _ hes

Premises used: contDiffGroupoid, StructureGroupoid.mem_of_eqOnSource'
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst_3] s
hes : e ≈ OpenPartialHomeomorph.ofSet s hs
⊢ OpenPartialHomeomorph.ofSet s hs ∈ (contDiffGroupoid n I).members

Tactic:
ofSet_mem_contDiffGroupoid hs

Premises used: ofSet_mem_contDiffGroupoid
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst_3] s
hes : e ≈ OpenPartialHomeomorph.ofSet s hs
⊢ OpenPartialHomeomorph.ofSet s hs ∈ (contDiffGroupoid n I).members

Tactic:
exact ofSet_mem_contDiffGroupoid hs

Premises used: ofSet_mem_contDiffGroupoid
-- 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
gr : HasGroupoid M (contDiffGroupoid n I)
⊢ IsManifold I n M

Tactic:
{ gr with }

Premises used: 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
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
h :
  ∀ (e e' : OpenPartialHomeomorph M H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
        ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
          ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
⊢ HasGroupoid M (contDiffGroupoid n I)

Tactic:
haveI : HasGroupoid M (contDiffGroupoid n I) := hasGroupoid_of_pregroupoid _ (h _ _)
-- 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
h :
  ∀ (e e' : OpenPartialHomeomorph M H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
        ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
          ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
this : HasGroupoid M (contDiffGroupoid n I)
⊢ ∀ {e e' : OpenPartialHomeomorph M H},
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' → e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
apply StructureGroupoid.compatible

Premises used: StructureGroupoid.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 : ℕ∞ω
⊢ IsManifold I n H

Tactic:
{ hasGroupoid_model_space _ _ with }

Premises used: contDiffGroupoid, IsManifold.mk, hasGroupoid_model_space
-- 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
m n : ℕ∞ω
hmn : m ≤ n
inst_6 : IsManifold I n M
⊢ HasGroupoid M (contDiffGroupoid n I)

Tactic:
infer_instance
-- 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
m n : ℕ∞ω
hmn : m ≤ n
inst_6 : IsManifold I n M
⊢ HasGroupoid M (contDiffGroupoid m I)

Tactic:
have : HasGroupoid M (contDiffGroupoid m I) :=
    hasGroupoid_of_le (G₁ := contDiffGroupoid n I) (by infer_instance)
      (contDiffGroupoid_le hmn)
-- 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
m n : ℕ∞ω
hmn : m ≤ n
inst_6 : IsManifold I n M
this : HasGroupoid M (contDiffGroupoid m I)
⊢ IsManifold I m M

Tactic:
mk' I m M

Premises used: 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
m n : ℕ∞ω
hmn : m ≤ n
inst_6 : IsManifold I n M
this : HasGroupoid M (contDiffGroupoid m I)
⊢ IsManifold I m M

Tactic:
exact mk' I m M

Premises used: 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
n_1 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞
⊢ LEInfty (↑n : ℕ∞ω)

Tactic:
⟨mod_cast le_top⟩

Premises used: WithTop.coe_le_coe._simp_1, cast, ENat.LEInfty.mk, le_top, Eq.symm
-- 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_1 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ
⊢ LEInfty (↑n : ℕ∞ω)

Tactic:
⟨mod_cast le_top⟩

Premises used: WithTop.coe_le_coe._simp_1, cast, ENat.LEInfty.mk, le_top, Eq.symm
-- 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_1 : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ
inst_6 : n.AtLeastTwo
⊢ LEInfty (OfNat.ofNat n)

Tactic:
inferInstanceAs (LEInfty (n : ℕ∞ω))

Premises used: _private.0.IsManifold.instLEInftyOfNatWithTopENat._proof_1
-- 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
⊢ LEInfty 1

Tactic:
inferInstanceAs (LEInfty ((1 : ℕ) : ℕ∞ω))

Premises used: _private.0.IsManifold.instLEInftyOfNatWithTopENat_1._proof_1
-- 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
⊢ LEInfty 0

Tactic:
inferInstanceAs (LEInfty ((0 : ℕ) : ℕ∞ω))

Premises used: _private.0.IsManifold.instLEInftyOfNatWithTopENat_2._proof_1
-- 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
a : ℕ∞ω
inst_6 : IsManifold I ∞ M
h : LEInfty a
⊢ IsManifold I a M

Tactic:
IsManifold.of_le h.out

Premises used: ENat.LEInfty.out, IsManifold.of_le
-- 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
a : ℕ∞ω
inst_6 : IsManifold I ω M
⊢ IsManifold I a M

Tactic:
IsManifold.of_le le_top

Premises used: le_top, IsManifold.of_le
-- 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
suffices : HasGroupoid M (contDiffGroupoid 0 I)
⊢ IsManifold I 0 M

Tactic:
suffices HasGroupoid M (contDiffGroupoid 0 I) from mk' I 0 M
-- 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
compatible :
  ∀ {e e' : OpenPartialHomeomorph M H},
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' → e.symm ≫ₕ e' ∈ contDiffGroupoid 0 I
⊢ HasGroupoid M (contDiffGroupoid 0 I)

Tactic:
constructor
-- 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
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
compatible : Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) (e.symm ≫ₕ e')
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid 0 I

Tactic:
rw [contDiffGroupoid_zero_eq]

Premises used: contDiffGroupoid_zero_eq
-- 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
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
compatible : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source
compatible₁ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e').symm : H → H) (e.symm ≫ₕ e').target
compatible₂ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source
compatible₃ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e').symm : H → H) (e.symm ≫ₕ e').target
compatible₄ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source
compatible₅ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e').symm : H → H) (e.symm ≫ₕ e').target
compatible₆ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source
compatible₇ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e').symm : H → H) (e.symm ≫ₕ e').target
⊢ Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) (e.symm ≫ₕ e')

Tactic:
trivial
-- 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 2 M
⊢ IsManifold I 1 M

Tactic:
IsManifold.of_le one_le_two

Premises used: one_le_two, IsManifold.of_le
-- 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 3 M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LE.le (α := ℕ) 2 3
⊢ LE.le (α := ℕ∞ω) 2 3

Tactic:
norm_cast
-- 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
e : OpenPartialHomeomorph M H
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e ↔
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M (contDiffGroupoid n I)) e

Tactic:
rfl
-- 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
⊢ Subset (α := Set (OpenPartialHomeomorph M H)) (atlas H M) (maximalAtlas I n M)

Tactic:
StructureGroupoid.subset_maximalAtlas _

Premises used: IsManifold.maximalAtlas, StructureGroupoid.subset_maximalAtlas
-- 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
x : M
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) (chartAt H x)

Tactic:
StructureGroupoid.chart_mem_maximalAtlas _ x

Premises used: Set.Mem, IsManifold.maximalAtlas, StructureGroupoid.chart_mem_maximalAtlas
-- 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
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
StructureGroupoid.compatible_of_mem_maximalAtlas he he'

Premises used: StructureGroupoid.compatible_of_mem_maximalAtlas
-- 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
m n : ℕ∞ω
h : m ≤ n
⊢ Subset (α := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) (maximalAtlas I m M)

Tactic:
StructureGroupoid.maximalAtlas_mono (contDiffGroupoid_le h)

Premises used: IsManifold.maximalAtlas, contDiffGroupoid_le, StructureGroupoid.maximalAtlas_mono
-- 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 : IsEmpty M
h :
  ∀ (e e' : OpenPartialHomeomorph M H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
        ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
          ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
⊢ IsManifold I n M

Tactic:
apply isManifold_of_contDiffOn

Premises used: isManifold_of_contDiffOn
-- 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 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h :
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
      ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
        ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
      ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
        ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))

Tactic:
_
-- 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 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h :
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
    ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
    ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))

Tactic:
_