mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ ∃ v, IsOpen[inst✝] v ∧ x ∈ v ∧ PG.property (↑e.symm) (e.target ∩ v)

Tactic:
refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩

Goal state after:
case right.refine_1
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ IsOpen[inst✝] (e.target ∩ ↑e.symm ⁻¹' s)

case right.refine_2
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑e.symm) (e.target ∩ (e.target ∩ ↑e.symm ⁻¹' s))
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case right.refine_1
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ IsOpen[inst✝] (e.target ∩ ↑e.symm ⁻¹' s)

pp: case right.refine_2
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑e.symm) (e.target ∩ (e.target ∩ ↑e.symm ⁻¹' s))

Tactic:
· exact ContinuousOn.isOpen_inter_preimage e.continuousOn_invFun e.open_target s_open

Goal state after:
case right.refine_2
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑e.symm) (e.target ∩ (e.target ∩ ↑e.symm ⁻¹' s))
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ
      t.openPartialHomeomorphSubtypeCoe this ≫ₕ OpenPartialHomeomorph.refl H ∈
    maximalAtlas (↥s) G

Tactic:
OpenPartialHomeomorph.trans_refl

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ map (↑I ∘ ↑f) (𝓝 x) = 𝓝[range ↑I] (↑I ∘ ↑f) x

Tactic:
comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ map (↑I ∘ ↑f) (𝓝 x) = 𝓝[range ↑I] ↑I (↑f x)
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
⊢ (g ∘ ↑(f.extend I).symm) (↑(f.extend I) z) ∈ f'.source

Tactic:
comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
⊢ g (↑(f.extend I).symm (↑(f.extend I) z)) ∈ f'.source
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑(f.extend I) '' (f.source ∩ f'.source) = (extendCoordChange f f').source

Tactic:
simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
    OpenPartialHomeomorph.symm_target]

Goal state after:
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
hs : s ∈ 𝓝 x
⊢ LiftPropAt P g x

Tactic:
rwa [← univ_inter s, hG.liftPropWithinAt_inter hs] at h

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝ : TopologicalSpace M
⊢ ∀ x ∈ ↑I.symm ⁻¹' univ ∩ range ↑I, (↑I ∘ id ∘ ↑I.symm) x = id x

Tactic:
rintro x ⟨_, hx2⟩

Goal state after:
m n : ℕ∞ω
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝ : TopologicalSpace M
x : E
left✝ : x ∈ ↑I.symm ⁻¹' univ
hx2 : x ∈ range ↑I
⊢ (↑I ∘ id ∘ ↑I.symm) x = id x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_2
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ P (↑(chartAt H' (f (inclusion hUV x))) ∘ f ∘ ↑(chartAt H (inclusion hUV x)).symm)
      (↑(chartAt H (inclusion hUV x)).symm ⁻¹' univ) (↑(chartAt H (inclusion hUV x)) (inclusion hUV x)) ↔
    P (↑(chartAt H' ((f ∘ inclusion hUV) x)) ∘ (f ∘ inclusion hUV) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ)
      (↑(chartAt H x) x)

Tactic:
apply hG.congr_iff
    exact (TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq hUV).fun_comp
      (chartAt H' (f (Set.inclusion hUV x)) ∘ f)

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] z = 𝓝[range ↑I] z

Tactic:
← PartialEquiv.right_inv (extChartAt I x) hz

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] ↑(extChartAt I x) (↑(extChartAt I x).symm z) =
    𝓝[range ↑I] ↑(extChartAt I x) (↑(extChartAt I x).symm z)
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
M' : Type u_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
p : M ⊕ M'
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g p)) ∘ Sum.elim f g ∘ ↑(extChartAt I p).symm) (range ↑I)
    (↑(extChartAt I p) p)

Tactic:
cases p with
  | inl x =>
    -- In charts around x : M, the map f ⊔ g looks like f.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) := by
      let hf' := hf x
      rw [contMDiffAt_iff] at hf'
      simpa using hf'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_inl]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]
      congr
  | inr x =>
    -- In charts around x : M, the map f ⊔ g looks like g.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (g x)) ∘ g ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) := by
      let hg' := hg x
      rw [contMDiffAt_iff] at hg'
      simpa using hg'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inr, ChartedSpace.sum_chartAt_inr]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]
      congr

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.LieGroup

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : Inv G
inst✝⁶ : Zero G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
f : M → G
inst✝ : ContinuousInv₀ G
this : T1Space G
A : ContMDiffOn I I 0 (fun x ↦ x⁻¹) {0}ᶜ
x : G
hx : x ≠ 0
⊢ ContMDiffAt I I 0 (fun y ↦ y⁻¹) x

Tactic:
have : ContMDiffWithinAt I I 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ x := A x hx

Goal state after:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : Inv G
inst✝⁶ : Zero G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
f : M → G
inst✝ : ContinuousInv₀ G
this✝ : T1Space G
A : ContMDiffOn I I 0 (fun x ↦ x⁻¹) {0}ᶜ
x : G
hx : x ≠ 0
this : ContMDiffWithinAt I I 0 (fun x ↦ x⁻¹) {0}ᶜ x
⊢ ContMDiffAt I I 0 (fun y ↦ y⁻¹) x
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
⊢ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
refine (eventually_mem_nhds_iff.mpr hu).mono fun x' hx' => ?_

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
x' : M
hx' : u ∈ 𝓝 x'
⊢ ContMDiffAt I I' n f x'
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
s : Set M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x ↔
    ContinuousWithinAt f s x ∧ LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) (↑(extChartAt I' y) ∘ f) s x

Tactic:
rw [differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart_target
      (chart_mem_maximalAtlas y) hy, and_congr_right]

Goal state after:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
s : Set M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f s x →
    (LiftPropWithinAt (DifferentiableWithinAtProp I I') (↑(chartAt H' y) ∘ f) s x ↔
      LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) (↑(extChartAt I' y) ∘ f) s x)
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen[inst✝⁷] (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q ↦ (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
hU' : IsOpen[inst✝⁷] U
Φ₀ : ↑U → F ≃L[𝕜] F := iUnionLift u (fun x ↦ φ x ∘ Subtype.val) huφ U ⋯
Φ : B → F ≃L[𝕜] F := fun y ↦ if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩
x : ↑U
y : B
⊢ y ∈ u x → Φ y = φ x y

Tactic:
hyu

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen[inst✝⁷] (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q ↦ (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
hU' : IsOpen[inst✝⁷] U
Φ₀ : ↑U → F ≃L[𝕜] F := iUnionLift u (fun x ↦ φ x ∘ Subtype.val) huφ U ⋯
Φ : B → F ≃L[𝕜] F := fun y ↦ if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩
x : ↑U
y : B
hyu : y ∈ u x
⊢ Φ y = φ x y
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝² b] (Trivialization.symmₗ R e b).toFun

Tactic:
by_cases hb : b ∈ e.baseSet
      · rw [(FiberBundle.totalSpaceMk_isInducing F E b).continuous_iff]
        refine .congr (f := TotalSpace.mk b ∘ e.symm b) ?_ (by simp [hb])
        exact e.continuousOn_symm.comp_continuous (.prodMk_right _) fun x ↦
          mk_mem_prod hb (mem_univ x)
      · exact continuous_zero.congr fun x => (e.symmₗ_apply_of_notMem hb x).symm

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = ↑(extChartAt I x).symm (↑(extChartAt I x) y)
⊢ mfderiv% ↑(extChartAt I x) y ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) y))

Tactic:
convert! mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm ((extChartAt I x).map_source hy)

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: case left
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        (↑((chartAt H x).symm.prod (OpenPartialHomeomorph.refl F).symm)
          ((fun p ↦ (↑I.symm p.1, id p.2)) (z, w)))).proj ∈
    s

Tactic:
OpenPartialHomeomorph.refl_symm,

Goal state after:
case left
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        (↑((chartAt H x).symm.prod (OpenPartialHomeomorph.refl F)) ((fun p ↦ (↑I.symm p.1, id p.2)) (z, w)))).proj ∈
    s