awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
v : GroupLieAlgebra I G
⊢ ⁅v, v⁆ = 0

Tactic:
simp [GroupLieAlgebra.bracket_def]

Premises used: GroupLieAlgebra.bracket_def
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
simp :
  mlieBracket I (mulInvariantVectorField u) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G)
      (mlieBracket I (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v)) (mulInvariantVectorField w)
        1)
      (mlieBracket I (mulInvariantVectorField v) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w))
        1)
⊢ ⁅u, ⁅v, w⁆⁆ = ⁅⁅u, v⁆, w⁆ + ⁅v, ⁅u, w⁆⁆

Tactic:
simp only [GroupLieAlgebra.bracket_def, mulInvariantVector_mlieBracket]

Premises used: mulInvariantVector_mlieBracket, GroupLieAlgebra.bracket_def
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
hU :
  ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1
hV :
  ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1
hW :
  ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1
⊢ mlieBracket I (mulInvariantVectorField u) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G)
      (mlieBracket I (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v)) (mulInvariantVectorField w)
        1)
      (mlieBracket I (mulInvariantVectorField v) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w))
        1)

Tactic:
apply leibniz_identity_mlieBracket_apply

Premises used: VectorField.leibniz_identity_mlieBracket_apply
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1

Tactic:
contMDiff_mulInvariantVectorField _ _

Premises used: contMDiff_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1

Tactic:
exact contMDiff_mulInvariantVectorField _ _

Premises used: contMDiff_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
contMDiff_mulInvariantVectorField _ _

Premises used: contMDiff_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
exact contMDiff_mulInvariantVectorField _ _

Premises used: contMDiff_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
contMDiff_mulInvariantVectorField _ _

Premises used: contMDiff_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
exact contMDiff_mulInvariantVectorField _ _

Premises used: contMDiff_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G_1 : Type u_4
inst_4 : TopologicalSpace G_1
inst_5 : ChartedSpace H G_1
inst_6 : Group G_1
inst_7 : LieGroup I (minSmoothness 𝕜 3) G_1
inst_8 : CompleteSpace E
G : Type u_5
inst_9 : TopologicalSpace G
inst_10 : ChartedSpace H G
inst_11 : AddGroup G
inst_12 : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
simp :
  mlieBracket I (addInvariantVectorField v) (c • addInvariantVectorField w) 0 =
    HSMul.hSMul (β := AddGroupLieAlgebra I G) c
      (mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0)
⊢ ⁅v, c • w⁆ = c • ⁅v, w⁆

Tactic:
simp only [AddGroupLieAlgebra.bracket_def, addInvariantVectorField_smul]

Premises used: AddGroupLieAlgebra.bracket_def, addInvariantVectorField_smul
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G_1 : Type u_4
inst_4 : TopologicalSpace G_1
inst_5 : ChartedSpace H G_1
inst_6 : Group G_1
inst_7 : LieGroup I (minSmoothness 𝕜 3) G_1
inst_8 : CompleteSpace E
G : Type u_5
inst_9 : TopologicalSpace G
inst_10 : ChartedSpace H G
inst_11 : AddGroup G
inst_12 : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
rw : (MDiffAt fun (x : G) ↦ ⟨x, addInvariantVectorField w x⟩) 0
⊢ mlieBracket I (addInvariantVectorField v) (c • addInvariantVectorField w) 0 =
    HSMul.hSMul (β := AddGroupLieAlgebra I G) c
      (mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0)

Tactic:
rw [mlieBracket_const_smul_right]

Premises used: VectorField.mlieBracket_const_smul_right
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G_1 : Type u_4
inst_4 : TopologicalSpace G_1
inst_5 : ChartedSpace H G_1
inst_6 : Group G_1
inst_7 : LieGroup I (minSmoothness 𝕜 3) G_1
inst_8 : CompleteSpace E
G : Type u_5
inst_9 : TopologicalSpace G
inst_10 : ChartedSpace H G
inst_11 : AddGroup G
inst_12 : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, addInvariantVectorField w x⟩) 0

Tactic:
mdifferentiableAt_addInvariantVectorField _

Premises used: mdifferentiableAt_addInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G_1 : Type u_4
inst_4 : TopologicalSpace G_1
inst_5 : ChartedSpace H G_1
inst_6 : Group G_1
inst_7 : LieGroup I (minSmoothness 𝕜 3) G_1
inst_8 : CompleteSpace E
G : Type u_5
inst_9 : TopologicalSpace G
inst_10 : ChartedSpace H G
inst_11 : AddGroup G
inst_12 : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, addInvariantVectorField w x⟩) 0

Tactic:
exact mdifferentiableAt_addInvariantVectorField _

Premises used: mdifferentiableAt_addInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
simp :
  mlieBracket I (mulInvariantVectorField v) (c • mulInvariantVectorField w) 1 =
    HSMul.hSMul (β := GroupLieAlgebra I G) c (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)
⊢ ⁅v, c • w⁆ = c • ⁅v, w⁆

Tactic:
simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_smul]

Premises used: mulInvariantVectorField_smul, GroupLieAlgebra.bracket_def
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
rw : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1
⊢ mlieBracket I (mulInvariantVectorField v) (c • mulInvariantVectorField w) 1 =
    HSMul.hSMul (β := GroupLieAlgebra I G) c (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)

Tactic:
rw [mlieBracket_const_smul_right]

Premises used: VectorField.mlieBracket_const_smul_right
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u_5
inst : TopologicalSpace H
G : StructureGroupoid H
M : Type u_6
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : HasGroupoid M G
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'
⊢ e.symm ≫ₕ e' ∈ G

Tactic:
HasGroupoid.compatible he he'

Premises used: HasGroupoid.compatible
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G₁ G₂ : StructureGroupoid H
h : HasGroupoid M G₁
hle : G₁ ≤ G₂
⊢ HasGroupoid M G₂

Tactic:
⟨fun he he' ↦ hle (h.compatible he he')⟩

Premises used: HasGroupoid.mk, HasGroupoid.compatible
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G₁ G₂ : StructureGroupoid H
⊢ HasGroupoid M (G₁ ⊓ G₂) ↔ HasGroupoid M G₁ ∧ HasGroupoid M G₂

Tactic:
⟨(fun h ↦ ⟨hasGroupoid_of_le h inf_le_left, hasGroupoid_of_le h inf_le_right⟩),
  fun ⟨h1, h2⟩ ↦ { compatible := fun he he' ↦ ⟨h1.compatible he he', h2.compatible he he'⟩ }⟩

Premises used: hasGroupoid_of_le, HasGroupoid, HasGroupoid.mk, inf_le_right, _private.0.hasGroupoid_inf_iff.match_1, And.intro, Iff.intro, inf_le_left, Min.min, HasGroupoid.compatible
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
PG : Pregroupoid H
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' →
        PG.property (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source
⊢ HasGroupoid M PG.groupoid

Tactic:
⟨fun he he' ↦ mem_groupoid_of_pregroupoid.mpr ⟨h he he', h he' he⟩⟩

Premises used: Iff.mpr, HasGroupoid.mk, And.intro, mem_groupoid_of_pregroupoid
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H_1 : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H_1
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H_1 M
H : Type u_5
inst_3 : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e'
⊢ e = OpenPartialHomeomorph.refl H

Tactic:
rw [chartedSpaceSelf_atlas] at he he'

Premises used: chartedSpaceSelf_atlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H_1 : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H_1
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H_1 M
H : Type u_5
inst_3 : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e'
he₁ : e = OpenPartialHomeomorph.refl H
⊢ e' = OpenPartialHomeomorph.refl H

Tactic:
rw [chartedSpaceSelf_atlas] at he he'

Premises used: chartedSpaceSelf_atlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H_1 : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H_1
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H_1 M
H : Type u_5
inst_3 : TopologicalSpace H
G : StructureGroupoid H
e e' : OpenPartialHomeomorph H H
he : e = OpenPartialHomeomorph.refl H
he' : e' = OpenPartialHomeomorph.refl H
⊢ e.symm ≫ₕ e' ∈ G

Tactic:
simp [he, he', StructureGroupoid.id_mem]

Premises used: StructureGroupoid.id_mem
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
⊢ HasGroupoid M (continuousGroupoid H)

Tactic:
⟨fun _ _ ↦ ?_⟩

Premises used: HasGroupoid.mk
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
refine :
  ∀ {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' →
        Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) (e.symm ≫ₕ e')
⊢ HasGroupoid M (continuousGroupoid H)

Tactic:
refine ⟨fun _ _ ↦ ?_⟩
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
⊢ Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source ∧
    Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e').symm : H → H) (e.symm ≫ₕ e').target

Tactic:
simp only [and_self_iff]

Premises used: and_self_iff
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e e' : OpenPartialHomeomorph M H
G : StructureGroupoid H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
⊢ (e.subtypeRestr hs).symm ≫ₕ e'.subtypeRestr hs ∈ G

Tactic:
G.mem_of_eqOnSource (closedUnderRestriction' (G.compatible he he')
    (e.isOpen_inter_preimage_symm s.2)) (e.subtypeRestr_symm_trans_subtypeRestr hs e')

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr, StructureGroupoid.compatible, TopologicalSpace.Opens.is_open', OpenPartialHomeomorph.isOpen_inter_preimage_symm, closedUnderRestriction'
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
⊢ Subset (α := Set (OpenPartialHomeomorph M H)) (atlas H M) (maximalAtlas M G)

Tactic:
fun _ he _ he' ↦ ⟨G.compatible he he', G.compatible he' he⟩

Premises used: Set.Mem, setOf, StructureGroupoid.compatible, Set.Subset, And.intro, StructureGroupoid.maximalAtlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
x : M
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) (chartAt H x)

Tactic:
G.subset_maximalAtlas (chart_mem_atlas H x)

Premises used: chart_mem_atlas, StructureGroupoid.subset_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e ↔
    ∀ (e' : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' → e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, StructureGroupoid.maximalAtlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
⊢ e.symm ≫ₕ e' ∈ G

Tactic:
G.locality fun x hx ↦ ?_

Premises used: StructureGroupoid.locality
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
refine : ∀ (x : H) (hx : x ∈ (e.symm ≫ₕ e').source), ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
⊢ e.symm ≫ₕ e' ∈ G

Tactic:
refine G.locality fun x hx ↦ ?_

Premises used: StructureGroupoid.locality
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
hs : IsOpen[inst] e.symm.source
ht : IsOpen[inst_1] f.source
⊢ IsOpen[inst] s

Tactic:
apply e.symm.continuousOn_toFun.isOpen_inter_preimage

Premises used: ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_toFun, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H ((↑e.symm : H → M) x)
s : Set H := e.target ∩ (↑e.symm : H → M) ⁻¹' f.source
⊢ IsOpen[inst] e.symm.source

Tactic:
apply open_source

Premises used: OpenPartialHomeomorph.open_source