awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
hinv :
  Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (mfderiv% (f ∘ (↑hf.localInverse.toPartialEquiv : N → M)) (f x))
⊢ Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace J (f x)))

Tactic:
rw [← mfderiv_id, ← hf.localInverse_eventuallyEq_right.mfderiv_eq]

Premises used: IsLocalDiffeomorphAt.localInverse_eventuallyEq_right, Filter.EventuallyEq.mfderiv_eq, mfderiv_id
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : MDiffAt f x
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
rw : MDiffAt f x
⊢ MDiffAt f ((↑hf.localInverse.toPartialEquiv : N → M) (f x))

Tactic:
rw [hf.localInverse_left_inv hf.localInverse_mem_target]

Premises used: IsLocalDiffeomorphAt.localInverse_mem_target, IsLocalDiffeomorphAt.localInverse_left_inv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ MDiffAt f x

Tactic:
hf.mdifferentiableAt hn

Premises used: IsLocalDiffeomorphAt.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ MDiffAt f x

Tactic:
exact hf.mdifferentiableAt hn

Premises used: IsLocalDiffeomorphAt.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ MDiffAt f ((↑hf.localInverse.toPartialEquiv : N → M) (f x))

Tactic:
have hf' : MDifferentiableAt I J f (hf.localInverse (f x)) := by
      rw [hf.localInverse_left_inv hf.localInverse_mem_target]
      exact hf.mdifferentiableAt hn
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
hf' : MDiffAt f ((↑hf.localInverse.toPartialEquiv : N → M) (f x))
hinv :
  Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
      (mfderiv% f ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
hinv₁ hinv₂ :
  Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
⊢ Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (mfderiv% (f ∘ (↑hf.localInverse.toPartialEquiv : N → M)) (f x))

Tactic:
rw [mfderiv_comp _ hf' (hf.localInverse_mdifferentiableAt hn),
      hf.localInverse_left_inv hf.localInverse_mem_target]

Premises used: mfderiv_comp, IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, IsLocalDiffeomorphAt.localInverse_mem_target, IsLocalDiffeomorphAt.localInverse_left_inv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ (↑(hf.mfderivToContinuousLinearEquiv hn) : TangentSpace I x →L[𝕜] TangentSpace J (f x)) = mfderiv% f x

Tactic:
rfl

Premises used: mfderiv, rfl, ContinuousLinearEquiv.toContinuousLinearMap, ite
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
x : M
Φ : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
⊢ (↑(Φ.mfderivToContinuousLinearEquiv hn x) : TangentSpace I x →L[𝕜] TangentSpace J ((Φ : (a : M) → N) x)) =
    mfderiv% (⇑Φ : (a : M) → N) x

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
hn : n ≠ 0
x : M
⊢ (↑(hf.mfderivToContinuousLinearEquiv hn x) : TangentSpace I x →L[𝕜] TangentSpace J (f x)) = mfderiv% f x

Tactic:
(hf x).mfderivToContinuousLinearEquiv_coe hn

Premises used: IsLocalDiffeomorph.mfderivToContinuousLinearEquiv, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
obtain :
  ∀ (o : Set H) (host : o ⊆ {x : H | (fun (x : H) ↦ x ∈ s ↔ x ∈ t) x}) (ho : IsOpen[inst] o) (hxo : x ∈ o),
    P f s x ↔ P f t x
⊢ P f s x ↔ P f t x

Tactic:
obtain ⟨o, host, ho, hxo⟩ := mem_nhds_iff.mp hu.mem_iff

Premises used: mem_nhds_iff, Filter.EventuallyEq.mem_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
host : o ⊆ {x : H | (fun (x : H) ↦ x ∈ s ↔ x ∈ t) x}
ho : IsOpen[inst] o
hxo : x ∈ o
⊢ s ∩ o = t ∩ o

Tactic:
simp_rw [subset_def, mem_setOf, ← and_congr_left_iff, ← mem_inter_iff, ← Set.ext_iff] at host

Premises used: Set.subset_def, Set.mem_inter_iff, Set.mem_setOf, and_congr_left_iff, Set.ext_iff
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
rw : P f (s ∩ o) x ↔ P f t x
rw₁ : P f (t ∩ o) x ↔ P f t x
rw₂ rw₃ : P f t x ↔ P f t x
⊢ P f s x ↔ P f t x

Tactic:
rw [hG.is_local ho hxo, host, ← hG.is_local ho hxo]

Premises used: StructureGroupoid.LocalInvariantProp.is_local
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s u : Set H
x : H
f : H → H'
hu : u ∈ 𝓝[s] x
⊢ P f s x ↔ P f (s ∩ u) x

Tactic:
hG.congr_set <| mem_nhdsWithin_iff_eventuallyEq.mp hu

Premises used: mem_nhdsWithin_iff_eventuallyEq, Iff.mp, StructureGroupoid.LocalInvariantProp.congr_set
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
simp_rw : P f (s ∩ {x : H | f x = g x}) x ↔ P g (s ∩ {x : H | f x = g x}) x
⊢ P f s x ↔ P g s x

Tactic:
simp_rw [hG.is_local_nhds h1]

Premises used: StructureGroupoid.LocalInvariantProp.is_local_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f (s ∩ {x : H | f x = g x}) x ↔ P g (s ∩ {x : H | f x = g x}) x

Tactic:
⟨hG.congr_of_forall (fun y hy ↦ hy.2) h2, hG.congr_of_forall (fun y hy ↦ hy.2.symm) h2.symm⟩

Premises used: And.right, StructureGroupoid.LocalInvariantProp.congr_of_forall, Iff.intro, Eq.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f (s ∩ {x : H | f x = g x}) x ↔ P g (s ∩ {x : H | f x = g x}) x

Tactic:
exact ⟨hG.congr_of_forall (fun y hy ↦ hy.2) h2, hG.congr_of_forall (fun y hy ↦ hy.2.symm) h2.symm⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
hP : P f s x
⊢ P g s x

Tactic:
(hG.congr_iff_nhdsWithin h1 h2).mp hP

Premises used: Iff.mp, StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
hP : P g s x
⊢ P f s x

Tactic:
(hG.congr_iff_nhdsWithin h1 h2).mpr hP

Premises used: Iff.mpr, StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h : f =ᶠ[𝓝 x] g
⊢ P f s x ↔ P g s x

Tactic:
hG.congr_iff_nhdsWithin (mem_nhdsWithin_of_mem_nhds h) (mem_of_mem_nhds h :)

Premises used: mem_of_mem_nhds, mem_nhdsWithin_of_mem_nhds, StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h : f =ᶠ[𝓝 x] g
hP : P f s x
⊢ P g s x

Tactic:
(hG.congr_iff h).mp hP

Premises used: StructureGroupoid.LocalInvariantProp.congr_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h : f =ᶠ[𝓝 x] g
hP : P g s x
⊢ P f s x

Tactic:
hG.congr h.symm hP

Premises used: StructureGroupoid.LocalInvariantProp.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
⊢ f ⁻¹' e'.source ∈ 𝓝[s] x

Tactic:
have h2f := hfs.preimage_mem_nhdsWithin (e'.open_source.mem_nhds hxe')
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
⊢ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x

Tactic:
have h3f :=
    ((e'.continuousAt hxe').comp_continuousWithinAt hfs).preimage_mem_nhdsWithin <|
      e'.symm.open_source.mem_nhds <| e'.mapsTo hxe'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
mp : P ((↑e' : H' → H') ∘ f) s x → P f s x
mpr : P f s x → P ((↑e' : H' → H') ∘ f) s x
⊢ P ((↑e' : H' → H') ∘ f) s x ↔ P f s x

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) s x
⊢ P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x

Tactic:
rw [hG.is_local_nhds h3f] at h

Premises used: StructureGroupoid.LocalInvariantProp.is_local_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
mp : ∀ (h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x), P f s x
⊢ P f s x

Tactic:
have h2 := hG.left_invariance' (G'.symm he') inter_subset_right (e'.mapsTo hxe') h
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
⊢ P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) s x

Tactic:
rw [← hG.is_local_nhds h3f] at h2

Premises used: StructureGroupoid.LocalInvariantProp.is_local_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) s x
⊢ P f s x

Tactic:
hG.congr_nhdsWithin ?_ (e'.left_inv hxe') h2

Premises used: StructureGroupoid.LocalInvariantProp.congr_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) s x
mp : (↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f =ᶠ[𝓝[s] x] f
⊢ P f s x

Tactic:
refine hG.congr_nhdsWithin ?_ (e'.left_inv hxe') h2

Premises used: StructureGroupoid.LocalInvariantProp.congr_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) s x
⊢ (↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f =ᶠ[𝓝[s] x] f

Tactic:
eventually_of_mem h2f fun x' ↦ e'.left_inv

Premises used: Filter.EventuallyEq, OpenPartialHomeomorph.left_inv, Filter.eventually_of_mem
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) s x
⊢ (↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f =ᶠ[𝓝[s] x] f

Tactic:
exact eventually_of_mem h2f fun x' ↦ e'.left_inv

Premises used: OpenPartialHomeomorph.left_inv, Filter.eventually_of_mem
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
mpr : P f (s ∩ f ⁻¹' e'.source) x → P ((↑e' : H' → H') ∘ f) (s ∩ f ⁻¹' e'.source) x
⊢ P f s x → P ((↑e' : H' → H') ∘ f) s x

Tactic:
simp_rw [hG.is_local_nhds h2f]

Premises used: StructureGroupoid.LocalInvariantProp.is_local_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P f (s ∩ f ⁻¹' e'.source) x → P ((↑e' : H' → H') ∘ f) (s ∩ f ⁻¹' e'.source) x

Tactic:
hG.left_invariance' he' inter_subset_right hxe'

Premises used: StructureGroupoid.LocalInvariantProp.left_invariance', Set.inter_subset_right