mathlib-initiative/mathlib-tactics huggingface dataset:
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 e' : OpenPartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
e'' : OpenPartialHomeomorph M H
he'' : e'' ∈ atlas H M
l : e.symm ≫ₕ e'' ∈ G
r : e''.symm ≫ₕ e ∈ G
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G

Tactic:
exact ⟨G.mem_of_eqOnSource l (EqOnSource.trans' (EqOnSource.symm' h) (e''.eqOnSource_refl)),
         G.mem_of_eqOnSource r (EqOnSource.trans' (e''.symm).eqOnSource_refl h)⟩

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

Goal state before:
pp: case refine_1
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e.source = univ

pp: case refine_2
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e.target = univ

Tactic:
<;>

Goal state after:
case refine_1
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e.source = univ

case refine_2
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e.target = univ
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case refine_1
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ (OpenPartialHomeomorph.refl H).source = univ

pp: case refine_2
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ (OpenPartialHomeomorph.refl H).target = univ

Tactic:
<;>

Goal state after:
case refine_1
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ (OpenPartialHomeomorph.refl H).source = univ

case refine_2
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ (OpenPartialHomeomorph.refl H).target = univ
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
⊢ PG.property (↑e'.symm) e'.target

Tactic:
have A := EqOnSource.symm' ee'

Goal state after:
case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
A : e'.symm ≈ e.symm
⊢ PG.property (↑e'.symm) e'.target
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case h
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑((OpenPartialHomeomorph.refl H).restr s) x✝

pp: case hinv
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs).symm x✝ = ↑((OpenPartialHomeomorph.refl H).restr s).symm x✝

pp: case hs
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).source ↔ x✝ ∈ ((OpenPartialHomeomorph.refl H).restr s).source

Tactic:
<;>

Goal state after:
case h
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑((OpenPartialHomeomorph.refl H).restr s) x✝

case hinv
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs).symm x✝ = ↑((OpenPartialHomeomorph.refl H).restr s).symm x✝

case hs
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).source ↔ x✝ ∈ ((OpenPartialHomeomorph.refl H).restr s).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 : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝[s] x
⊢ ↑(f.extend I).symm ⁻¹' t ∈ 𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) x

Tactic:
by
  rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this✝² : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')

Tactic:
exact I.convex_range.prod I'.convex_range

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

Goal state before:
pp: case toFun
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ ↑𝓘(𝕜, E × F).toPartialEquiv = ↑(𝓘(𝕜, E).prod 𝓘(𝕜, F)).toPartialEquiv

pp: case invFun
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F).invFun = (𝓘(𝕜, E).prod 𝓘(𝕜, F)).invFun

pp: case source
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F).source = (𝓘(𝕜, E).prod 𝓘(𝕜, F)).source

pp: case target
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F).target = (𝓘(𝕜, E).prod 𝓘(𝕜, F)).target

Tactic:
<;>

Goal state after:
case toFun
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ ↑𝓘(𝕜, E × F).toPartialEquiv = ↑(𝓘(𝕜, E).prod 𝓘(𝕜, F)).toPartialEquiv

case invFun
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F).invFun = (𝓘(𝕜, E).prod 𝓘(𝕜, F)).invFun

case source
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F).source = (𝓘(𝕜, E).prod 𝓘(𝕜, F)).source

case target
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F).target = (𝓘(𝕜, E).prod 𝓘(𝕜, F)).target
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case left
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e')) (e.prod e').source

pp: case right
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e').symm) (e.prod e').target

Tactic:
<;>

Goal state after:
case left
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e')) (e.prod e').source

case right
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e').symm) (e.prod e').target
Module: Mathlib.Geometry.Manifold.IsManifold.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
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty M
⊢ IsManifold I n M

Tactic:
apply isManifold_of_contDiffOn
  intro e e' _ _ x hx
  set t := I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I
  -- Since `M` is empty, the condition about compatibility of transition maps is vacuous.
  have : (e.symm ≫ₕ e').source = ∅ := calc (e.symm ≫ₕ e').source
    _ = (e.symm.source) ∩ e.symm ⁻¹' e'.source := by rw [← OpenPartialHomeomorph.trans_source]
    _ = (e.symm.source) ∩ e.symm ⁻¹' ∅ := by rw [eq_empty_of_isEmpty (e'.source)]
    _ = (e.symm.source) ∩ ∅ := by rw [preimage_empty]
    _ = ∅ := inter_empty e.symm.source
  have : t = ∅ := calc t
    _ = I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I := by
      rw [← Subtype.preimage_val_eq_preimage_val_iff]
    _ = ∅ ∩ range I := by rw [this, preimage_empty]
    _ = ∅ := empty_inter (range I)
  apply (this ▸ hx).elim

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: case none
𝕜 : 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
x : M
h : ∀ (m : ℕ), ↑m ≤ none → ContMDiffWithinAt I I' (↑m) f s x
⊢ ContMDiffWithinAt I I' (↑none) f s x

pp: case some
𝕜 : 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
x : M
n : ℕ
h : ∀ (m : ℕ), ↑m ≤ some n → ContMDiffWithinAt I I' (↑m) f s x
⊢ ContMDiffWithinAt I I' (↑(some n)) f s x

Tactic:
· exact contMDiffWithinAt_infty.2 fun n => h n le_top

Goal state after:
case some
𝕜 : 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
x : M
n : ℕ
h : ∀ (m : ℕ), ↑m ≤ some n → ContMDiffWithinAt I I' (↑m) f s x
⊢ ContMDiffWithinAt I I' (↑(some n)) f s 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'
s t : Set M
x : M
n : ℕ∞ω
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f t x

Tactic:
← contMDiffWithinAt_insert_self (s := t)

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 t : Set M
x : M
n : ℕ∞ω
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f (insert x t) x
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : ι → M → G
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ ContMDiff I' I n fun x ↦ ∏ᶠ (j : Subtype p), f (↑j) x

Tactic:
exact contMDiff_finprod (fun i ↦ hc i i.2) (hf.comp_injective Subtype.coe_injective)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 n (↑(extChartAt 𝓘(𝕜, 𝕜) y) ∘ (fun p ↦ p.1 * p.2) ∘ ↑(extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).symm)
    ((extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).target ∩
      ↑(extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).symm ⁻¹' (fun p ↦ p.1 * p.2) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source)

Tactic:
simp only [mfld_simps, chartAt_self_eq]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 n (fun p ↦ p.1 * p.2) Set.univ
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
⊢ ContMDiffInv₀ I 0 G

Tactic:
have : T1Space G := I.t1Space G

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
⊢ ContMDiffInv₀ I 0 G
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: case mp
𝕜 : 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
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
⊢ LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source

Tactic:
intro X hX

Goal state after:
case mp
𝕜 : 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
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source 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'
x : M
s : Set M
⊢ MDiffAt[s] f x ↔ ContinuousWithinAt f s x ∧ MDiffAt[s] (↑(extChartAt I' (f x)) ∘ f) x

Tactic:
simp_rw [MDifferentiableWithinAt, liftPropWithinAt_iff', ← and_assoc]

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
s : Set M
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x) ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (↑(chartAt E' ((↑(extChartAt I' (f x)) ∘ f) x)) ∘ (↑(extChartAt I' (f x)) ∘ f) ∘ ↑(chartAt H x).symm)
        (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case pos
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
h✝ : b ∈ e.baseSet
⊢ ⇑↑(linearEquivAt R e b h✝) = fun y ↦ (↑e { proj := b, snd := y }).2

pp: case neg
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
h✝ : b ∉ e.baseSet
⊢ ⇑0 = fun y ↦ 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
h✝ : b ∈ e.baseSet
⊢ ⇑↑(linearEquivAt R e b h✝) = fun y ↦ (↑e { proj := b, snd := y }).2

case neg
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
h✝ : b ∉ e.baseSet
⊢ ⇑0 = fun y ↦ 0