mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst✝ : IsManifold I n M
φ : OpenPartialHomeomorph M H
hφ : ContMDiffOn I I n (↑φ) φ.source
hφ' : ContMDiffOn I I n (↑φ.symm) φ.target
⊢ φ ∈ maximalAtlas I n M

Tactic:
by
  simp only [mfld_simps, IsManifold.mem_maximalAtlas_iff, StructureGroupoid.maximalAtlas,
    contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid,
    ← contMDiffOn_iff_contDiffOn]
  intro e he
  have he' := contMDiffOn_of_mem_maximalAtlas (I := I) (n := n)
    (StructureGroupoid.subset_maximalAtlas _ he)
  have he'' := contMDiffOn_symm_of_mem_maximalAtlas (I := I) (n := n)
    (StructureGroupoid.subset_maximalAtlas _ he)
  refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
  all_goals apply I.contMDiff.comp_contMDiffOn
  · apply he'.comp (hφ'.comp (I.contMDiffOn_symm.mono (by simp)) (by grind)) (by grind)
  · apply hφ.comp (he''.comp (I.contMDiffOn_symm.mono (by simp)) (by grind)) (by grind)
  · exact hφ.comp (he''.comp (I.contMDiffOn_symm.mono (by simp)) (by grind)) (by grind)
  · exact he'.comp (hφ'.comp (I.contMDiffOn_symm.mono (by simp)) (by grind)) (by grind)

Goal state after:
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
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x ↔
    ContinuousWithinAt f s x ∧ LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) (↑(extChartAt I' (f x)) ∘ f) s x

Tactic:
liftPropWithinAt_iff',

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.FiberBundle.Constructions

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : y ∈ (⇑f ⁻¹' e.baseSet) ×ˢ univ
⊢ TotalSpace.mk' F y.1 (e.symm (f y.1) y.2) ∈ Pullback.lift ⇑f ⁻¹' e.source

Tactic:
mem_prod,

Goal state after:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : y.1 ∈ ⇑f ⁻¹' e.baseSet ∧ y.2 ∈ univ
⊢ TotalSpace.mk' F y.1 (e.symm (f y.1) y.2) ∈ Pullback.lift ⇑f ⁻¹' e.source
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : x ∈ (⇑f ⁻¹' e.baseSet) ×ˢ univ
⊢ ((TotalSpace.mk' F x.1 (e.symm (f x.1) x.2)).proj,
      (↑e (Pullback.lift (⇑f) (TotalSpace.mk' F x.1 (e.symm (f x.1) x.2)))).2) =
    x

Tactic:
mem_prod,

Goal state after:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : x.1 ∈ ⇑f ⁻¹' e.baseSet ∧ x.2 ∈ univ
⊢ ((TotalSpace.mk' F x.1 (e.symm (f x.1) x.2)).proj,
      (↑e (Pullback.lift (⇑f) (TotalSpace.mk' F x.1 (e.symm (f x.1) x.2)))).2) =
    x
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : x ∈ (⇑f ⁻¹' e.baseSet) ×ˢ univ
⊢ ((TotalSpace.mk' F x.1 (e.symm (f x.1) x.2)).proj,
      (↑e (Pullback.lift (⇑f) (TotalSpace.mk' F x.1 (e.symm (f x.1) x.2)))).2) =
    x

Tactic:
simp_rw [mem_prod, mem_preimage, mem_univ, and_true] at h
    simp_rw [Pullback.lift_mk, e.apply_mk_symm h]

Goal state after:
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✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ (↑(coordChangeL R e e' b)).symm = (linearEquivAt R e' b ⋯).symm ≪≫ₗ linearEquivAt R e b ⋯

Tactic:
coe_coordChangeL' e e' hb.symm,

Goal state after:
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✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ ((linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯).symm =
    (linearEquivAt R e' b ⋯).symm ≪≫ₗ linearEquivAt R e b ⋯
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
f : M → F₁ × F₂
⊢ MDiffAt[s] f x ↔ MDiffAt[s] (Prod.fst ∘ f) x ∧ MDiffAt[s] (Prod.snd ∘ f) x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
f : M → F₁ × F₂
⊢ MDiffAt[s] f x ↔ MDiffAt[s] (Prod.fst ∘ f) x ∧ MDiffAt[s] (Prod.snd ∘ f) x
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
f : M → F₁ × F₂
⊢ MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
f : M → F₁ × F₂
⊢ MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
f : M → F₁ × F₂
⊢ MDiff[s] f ↔ MDiff[s] (Prod.fst ∘ f) ∧ MDiff[s] (Prod.snd ∘ f)

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
f : M → F₁ × F₂
⊢ MDiff[s] f ↔ MDiff[s] (Prod.fst ∘ f) ∧ MDiff[s] (Prod.snd ∘ f)
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
f : M → F₁ × F₂
⊢ MDiff f ↔ MDiff (Prod.fst ∘ f) ∧ MDiff (Prod.snd ∘ f)

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
f : M → F₁ × F₂
⊢ MDiff f ↔ MDiff (Prod.fst ∘ f) ∧ MDiff (Prod.snd ∘ f)
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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
u : Set M'
x : M
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffAt[s] x
hg : MDiffAt[u] g (f x)
⊢ mfderiv[s] (g ∘ f) x = mfderiv[u] g (f x) ∘SL mfderiv[s] f x

Tactic:
exact mfderivWithin_comp x hg hf h hxs

Goal state after:
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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
u : Set M'
x : M
y : M'
hg : MDiffAt[u] g y
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffAt[s] x
hy : f x = y
⊢ mfderiv[s] (g ∘ f) x = mfderiv[u] g y ∘SL mfderiv[s] f x

Tactic:
subst hy; exact mfderivWithin_comp x hg hf h hxs

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

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_9
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : (x : B) → AddCommMonoid (E x)
inst✝⁹ : (x : B) → Module 𝕜 (E x)
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : (x : B) → TopologicalSpace (E x)
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle n F E IB
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
s : Set M
x : M
f : M → TotalSpace F E
hp : ContMDiffWithinAt IM IB n (TotalSpace.proj ∘ f) s x
hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (↑e (f y)).2) s x
he : f x ∈ e.source
he' : f x ∈ e'.source
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (↑e' (f y)).2) s x

Tactic:
rw [Trivialization.mem_source] at he he'
  refine (hp.coordChange hf he he').congr_of_eventuallyEq ?_ (by simp [he])
  filter_upwards [hp.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
  simp_all

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_9
f : N → H
g : N → H'
ϕ : N → E →L[𝕜] E'
x₀ : N
⊢ inTangentCoordinates I I' f g ϕ x₀ = ϕ

Tactic:
simp +unfoldPartialApp only [inTangentCoordinates,
    inCoordinates_tangent_bundle_core_model_space]

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

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_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
t : Set M'
⊢ HasMFDerivAt[t] Sum.inr q' (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))

Tactic:
refine ⟨by fun_prop, ?_⟩
  have : (writtenInExtChartAt I I q' (@Sum.inr M M'))
      =ᶠ[𝓝[(extChartAt I q').symm ⁻¹' t ∩ Set.range I] (extChartAt I q' q')] id :=
    writtenInExtChartAt_sumInr_eventuallyEq_id.filter_mono (nhdsWithin_mono _ (fun _y hy ↦ hy.2))
  exact (hasFDerivWithinAt_id (extChartAt I q' q') _).congr_of_eventuallyEq this
    (by simp [writtenInExtChartAt, extChartAt])

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e✝ e : E ≃L[𝕜] F
x : M
⊢ ↑(extChartAt (I.transContinuousLinearEquiv e) x).symm (↑(extChartAt (I.transContinuousLinearEquiv e) x) x) ∈
    ⇑(Equiv.refl M).symm ⁻¹' (extChartAt I ((Equiv.refl M).symm x)).source

Tactic:
by
      simp only [e.symm_apply_apply, Equiv.refl_symm, Equiv.coe_refl, mfld_simps]

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → x ∉ v.toFun j
⊢ x ∈ update v.toFun i vi i

Tactic:
update_self

Goal state after:
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → x ∉ v.toFun j
⊢ x ∈ vi
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := ⋯
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → x ∉ v.toFun j
⊢ x ∈ update v.toFun i vi i

Tactic:
update_self

Goal state after:
case h
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → x ∉ v.toFun j
⊢ x ∈ vi
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_3.inl
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
vi : Set X
j : ι
hi : j ∉ v.carrier
si : Set X := s ∩ (⋃ j_1, ⋃ (_ : j_1 ≠ j), v.toFun j_1)ᶜ
hsi : si = s ∩ ⋂ i, ⋂ (_ : ¬i = j), (v.toFun i)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun j
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun j ∧ IsCompact (closure vi)
⊢ closure (update v.toFun j vi j) ⊆ u j

Tactic:
update_self

Goal state after:
case refine_3.inl
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
vi : Set X
j : ι
hi : j ∉ v.carrier
si : Set X := s ∩ (⋃ j_1, ⋃ (_ : j_1 ≠ j), v.toFun j_1)ᶜ
hsi : si = s ∩ ⋂ i, ⋂ (_ : ¬i = j), (v.toFun i)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun j
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun j ∧ IsCompact (closure vi)
⊢ closure vi ⊆ u j
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑((BumpCovering.single i s) j)

Tactic:
rcases eq_or_ne j i with (rfl | h)

Goal state after:
case inl
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsManifold I ∞ M
n : ℕ∞
s : Set M
j : ι
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑((BumpCovering.single j s) j)

case inr
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
h : j ≠ i
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑((BumpCovering.single i s) j)