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

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
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
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContinuousOn f s
⊢ (∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n
        (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
          f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
        (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
          ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
            (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))) →
    ∀ (y : M'),
      ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          ContDiffOn 𝕜 n
            (↑𝓘(𝕜, E').toPartialEquiv ∘
              (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) ∘
                ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
            (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
              ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
                (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))

Tactic:
refine fun h' y => ⟨?_, fun x _ => h' x y⟩
    have h'' : ContinuousOn _ univ := (ModelWithCorners.continuous I').continuousOn
    convert! (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h
    simp

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

Goal state before:
pp: case top
𝕜 : 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 ≠ ∞ → ContMDiffWithinAt I I' m f s x
⊢ ContMDiffWithinAt I I' ω f s x

Tactic:
exact h _ le_rfl (by simp)

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

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 : E → E'
x : E
⊢ mfderiv% f x = fderiv 𝕜 f x

Tactic:
← mfderivWithin_univ,

Goal state after:
𝕜 : 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 : E → E'
x : E
⊢ mfderiv[Set.univ] f x = fderiv 𝕜 f 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) ⋯ ⋯ ⋯)
x : ↑U
p : B × F
hp : p ∈ u x ×ˢ univ
⊢ p ∈ (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯).source

Tactic:
exact hp

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
cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
        (↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x)) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜
        (↑𝓘(𝕜, E') ∘
          (↑(chartAt E' (((↑I' ∘ ↑(chartAt H' (f x)).toPartialEquiv) ∘ f) x)) ∘
              ((↑I' ∘ ↑(chartAt H' (f x)).toPartialEquiv) ∘ f) ∘ ↑(chartAt H x).symm) ∘
            ↑I.symm)
        (↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))

Tactic:
OpenPartialHomeomorph.coe_toPartialEquiv,

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
cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
        (↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x)) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜
        (↑𝓘(𝕜, E') ∘
          (↑(chartAt E' (((↑I' ∘ ↑(chartAt H' (f x))) ∘ f) x)) ∘
              ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f) ∘ ↑(chartAt H x).symm) ∘
            ↑I.symm)
        (↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: case mpr.refine_1.convert_2
𝕜 : 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₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H✝ := chartAt H✝ x
c' : OpenPartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f) (f ≫ₕ c').source (↑(extChartAt I x).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I (↑f x)) ∘ ↑f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' (f ≫ₕ c').source ∩ range ↑I) (↑(extChartAt I x) (↑(extChartAt I x).symm y))
hy' : ↑(extChartAt I x).symm y ∈ c.source
hy'' : ↑f (↑(extChartAt I x).symm y) ∈ c'.source
⊢ ↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range ↑I ⊆ ↑(extChartAt I x).symm ⁻¹' (f ≫ₕ c').source ∩ range ↑I

Tactic:
dsimp [c, c']

Goal state after:
case mpr.refine_1.convert_2
𝕜 : 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₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H✝ := chartAt H✝ x
c' : OpenPartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f) (f ≫ₕ c').source (↑(extChartAt I x).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I (↑f x)) ∘ ↑f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' (f ≫ₕ c').source ∩ range ↑I) (↑(extChartAt I x) (↑(extChartAt I x).symm y))
hy' : ↑(extChartAt I x).symm y ∈ c.source
hy'' : ↑f (↑(extChartAt I x).symm y) ∈ c'.source
⊢ ↑I.symm ⁻¹' (chartAt H✝ x).target ∩ ↑I.symm ⁻¹' ↑(chartAt H✝ x).symm ⁻¹' f.source ∩
        ↑I.symm ⁻¹' ↑f ∘ ↑(chartAt H✝ x).symm ⁻¹' (chartAt H✝ (↑f x)).source ∩
      range ↑I ⊆
    ↑(chartAt H✝ x).symm ∘ ↑I.symm ⁻¹' f.source ∩ ↑(chartAt H✝ x).symm ∘ ↑I.symm ⁻¹' ↑f ⁻¹' (chartAt H✝ (↑f x)).source ∩
      range ↑I
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: case mpr.refine_2.convert_2
𝕜 : 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₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H✝ := chartAt H✝ x
c' : OpenPartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy :
  (↑I.symm y ∈ c'.target ∧ ↑c'.symm (↑I.symm y) ∈ f.target ∧ ↑f.symm (↑c'.symm (↑I.symm y)) ∈ c.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f.symm) (f.symm ≫ₕ c).source (↑(extChartAt I (↑f x)).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑f.symm ∘ ↑(extChartAt I (↑f x)).symm)
      (↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I)
      (↑(extChartAt I (↑f x)) (↑(extChartAt I (↑f x)).symm y))
hy' : ↑(extChartAt I (↑f x)).symm y ∈ c'.source
hy'' : ↑f.symm (↑(extChartAt I (↑f x)).symm y) ∈ c.source
⊢ ↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range ↑I ⊆ ↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I

Tactic:
dsimp [c, c']

Goal state after:
case mpr.refine_2.convert_2
𝕜 : 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₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H✝ := chartAt H✝ x
c' : OpenPartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy :
  (↑I.symm y ∈ c'.target ∧ ↑c'.symm (↑I.symm y) ∈ f.target ∧ ↑f.symm (↑c'.symm (↑I.symm y)) ∈ c.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f.symm) (f.symm ≫ₕ c).source (↑(extChartAt I (↑f x)).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑f.symm ∘ ↑(extChartAt I (↑f x)).symm)
      (↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I)
      (↑(extChartAt I (↑f x)) (↑(extChartAt I (↑f x)).symm y))
hy' : ↑(extChartAt I (↑f x)).symm y ∈ c'.source
hy'' : ↑f.symm (↑(extChartAt I (↑f x)).symm y) ∈ c.source
⊢ ↑I.symm ⁻¹' (chartAt H✝ (↑f x)).target ∩
        (↑I.symm ⁻¹' ↑(chartAt H✝ (↑f x)).symm ⁻¹' f.target ∩
          ↑I.symm ⁻¹' ↑(chartAt H✝ (↑f x)).symm ⁻¹' ↑f.symm ⁻¹' (chartAt H✝ x).source) ∩
      range ↑I ⊆
    ↑(chartAt H✝ (↑f x)).symm ∘ ↑I.symm ⁻¹' f.target ∩
        ↑(chartAt H✝ (↑f x)).symm ∘ ↑I.symm ⁻¹' ↑f.symm ⁻¹' (chartAt H✝ x).source ∩
      range ↑I
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: case mpr
𝕜 : 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
inst✝ : IsManifold I' 1 M'
⊢ (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))) →
    MDiff[s] f

Tactic:
rintro ⟨hcont, hdiff⟩ x hx

Goal state after:
case mpr
𝕜 : 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
inst✝ : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ MDiffAt[s] f x
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

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
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
inst✝ : IsManifold I' 1 M'
h : ContinuousOn f s
⊢ (∀ (x : M) (y : M'),
      DifferentiableOn 𝕜
        (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
          f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
        (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
          ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
            (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))) →
    ∀ (y : M'),
      ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          DifferentiableOn 𝕜
            (↑𝓘(𝕜, E').toPartialEquiv ∘
              (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) ∘
                ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
            (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
              ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
                (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))

Tactic:
refine fun h' y => ⟨?_, fun x _ => h' x y⟩
    have h'' : ContinuousOn _ univ := (ModelWithCorners.continuous I').continuousOn
    convert! (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h
    simp

Goal state after:
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: case refine_2
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x ↦ E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p ↦ ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ (↑e₁ p.1, ↑e₂ p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ } ∈ e₁.source

Tactic:
rw [e₁.source_eq, mem_preimage]

Goal state after:
case refine_2
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x ↦ E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p ↦ ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ (↑e₁ p.1, ↑e₂ p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ }.proj ∈ e₁.baseSet
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
h : s ∈ 𝓝 x
⊢ mfderiv[s] f x = mfderiv% f x

Tactic:
← mfderivWithin_univ,

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
h : s ∈ 𝓝 x
⊢ mfderiv[s] f x = mfderiv[univ] f x
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
inst✝ : VectorBundle R F E
x : B
⊢ ContinuousAt (fun x ↦ { proj := x, snd := 0 }) x

Tactic:
rw [FiberBundle.continuousAt_section]

Goal state after:
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
inst✝ : VectorBundle R F E
x : B
⊢ ContinuousAt (fun x_1 ↦ (↑(trivializationAt F E x) { proj := x_1, snd := 0 }).2) x
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy : y ∈ (chartAt (ModelProd HB F) x).target
⊢ (↑(chartAt (ModelProd HB F) x).symm y).proj = ↑(chartAt HB x.proj).symm y.1

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps] at hy ⊢

Goal state after:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy :
  y ∈ (chartAt HB x.proj).target ×ˢ univ ∧
    ↑((chartAt HB x.proj).prod (PartialEquiv.refl F)).symm y ∈ (trivializationAt F E x.proj).target
⊢ (↑(trivializationAt F E x.proj).symm (↑((chartAt HB x.proj).prod (OpenPartialHomeomorph.refl F)).symm y)).proj =
    ↑(chartAt HB x.proj).symm y.1
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 f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f₁) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
apply HasFDerivWithinAt.congr_of_eventuallyEq h.2

Goal state after:
case h₁
𝕜 : 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 f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ writtenInExtChartAt I I' x f₁ =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    writtenInExtChartAt I I' x f

case hx
𝕜 : 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 f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ writtenInExtChartAt I I' x f₁ (↑(extChartAt I x) x) = writtenInExtChartAt I I' x f (↑(extChartAt I x) x)