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

Goal state before:
pp: H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
⊢ ∀ {s : Set H} {x : H} {f : H → H} {e : OpenPartialHomeomorph H H},
    e ∈ G →
      x ∈ e.source →
        G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
intro s x f e' he'G he'x h hx
      have hxs : x ∈ s := by simpa only [e'.left_inv he'x, mfld_simps] using hx
      rcases h hxs with ⟨e, heG, hef, hex⟩
      refine ⟨e'.symm.trans e, G.trans (G.symm he'G) heG, ?_, ?_⟩
      · intro y hy
        simp only [mfld_simps] at hy
        simp only [hef ⟨hy.1, hy.2.2⟩, mfld_simps]
      · simp only [hex, he'x, mfld_simps]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
s_eq : s = ⋃ n, s ∩ t n
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
I : |(f' x).det| ≤ |(A n).det| + ↑ε
⊢ ENNReal.ofReal (|(A n).det| + ↑ε) = ENNReal.ofReal |(A n).det| + ↑ε

Tactic:
simp only [ENNReal.ofReal_add, abs_nonneg, NNReal.zero_le_coe, ENNReal.ofReal_coe_nnreal]

Goal state after:
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
⊢ IsManifold I 0 M

Tactic:
suffices HasGroupoid M (contDiffGroupoid 0 I) from mk' I 0 M
  constructor
  intro e e' he he'
  rw [contDiffGroupoid_zero_eq]
  trivial

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
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 (↑(extChartAt I x₀).symm (↑(extChartAt I x₀) y))

Tactic:
simp only [hy, PartialEquiv.left_inv]

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
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 y
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
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : DiscreteTopology M
inst✝ : Unique E
⊢ IsManifold 𝓘(𝕜, E) n M

Tactic:
by
  apply isManifold_of_contDiffOn _ _ _ (fun _ _ _ _ ↦ contDiff_of_subsingleton.contDiffOn)

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

Goal state before:
pp: H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : OpenPartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : OpenPartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : OpenPartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
⊢ x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source

Tactic:
simp only [hx, mfld_simps]

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

Goal state before:
pp: H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : OpenPartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : OpenPartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : OpenPartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source
⊢ x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)

Tactic:
simp only [hx, mfld_simps]

Goal state after:
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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))

Tactic:
simp only [hx, mfld_simps]

Goal state after:
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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))
this : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))
⊢ ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I

Tactic:
simp only [hx, mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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'
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
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
g : M' → M''
x : M
hf : ContMDiffWithinAt I I' n f s x
hg : ContMDiffAt I' I'' n g (f x)
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Tactic:
exact hg.comp_contMDiffWithinAt x hf

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

Goal state before:
pp: 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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
⊢ (↑I' ∘ g ∘ ↑I.symm) (↑I x) = (↑I' ∘ f ∘ ↑I.symm) (↑I x)

Tactic:
simp only [hx, mfld_simps]

Goal state after:
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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'

Tactic:
simp only [hx, mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))

Tactic:
simp only [hx, mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))
this : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))
⊢ ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I

Tactic:
simp only [hx, mfld_simps]

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

Goal state before:
pp: 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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : DifferentiableWithinAtProp I I' f s x
⊢ (↑I' ∘ g ∘ ↑I.symm) (↑I x) = (↑I' ∘ f ∘ ↑I.symm) (↑I x)

Tactic:
simp only [hx, mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid 1 I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'

Tactic:
simp only [hx, mfld_simps]

Goal state after:
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 : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n (↑(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
⊢ ↑(extChartAt I x) x ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
simp only [hx, mfld_simps]

Goal state after:
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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hs : s ⊆ e.source
⊢ ContMDiffOn I I' n f s ↔ ContMDiffOn 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)

Tactic:
simp_rw [ContMDiffOn, Set.forall_mem_image]

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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hs : s ⊆ e.source
⊢ (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
    ∀ ⦃x : M⦄, x ∈ s → ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)
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:
rw [← mfderivWithin_univ, ← fderivWithin_univ]
  exact mfderivWithin_eq_fderivWithin

Goal state after:
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 : ℕ∞ω
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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
⊢ ↑(chartAt H x) x ∈ ↑(chartAt H x).symm ⁻¹' f.source

Tactic:
simp only [hx, mfld_simps]

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'
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
⊢ ↑(extChartAt I x) x ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
simp only [hx, mfld_simps]

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
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt% f x f'
⊢ MDiffAt f x

Tactic:
mdifferentiableAt_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
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt% f x f'
⊢ ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: case refine_4
𝕜 : 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 e' : OpenPartialHomeomorph (B × F) (B × F)
φ : B → F ≃L[𝕜] F
U : Set B
hU : IsOpen[inst✝⁷] U
hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U
h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
φ' : B → F ≃L[𝕜] F
U' : Set B
hU' : IsOpen[inst✝⁷] U'
hφ' : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ' x)) U'
h2φ' : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ' x).symm) U'
heφ' : e'.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ' hU' ⋯ ⋯)
b : B
v : F
⊢ ↑(FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯ ≫ₕ FiberwiseLinear.openPartialHomeomorph φ' hU' ⋯ ⋯) (b, v) =
    ↑(FiberwiseLinear.openPartialHomeomorph (fun b ↦ (φ b).trans (φ' b)) ⋯ ⋯ ⋯) (b, v)

Tactic:
apply FiberwiseLinear.trans_openPartialHomeomorph_apply

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✝⁹ : 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 (zeroSection F E) x

Tactic:
unfold zeroSection

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 ↦ { proj := x, snd := 0 }) x
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 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)

Tactic:
simp only [hx, mfld_simps]

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✝⁶ : 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✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    ContinuousOn (fun b ↦ ↑(Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
by
      rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
      refine (a.continuousOn_coordChange he he').congr fun b hb ↦ ?_
      ext v
      have h₁ := a.linear_trivializationOfMemPretrivializationAtlas he
      have h₂ := a.linear_trivializationOfMemPretrivializationAtlas he'
      rw [trivializationOfMemPretrivializationAtlas] at h₁ h₂
      rw [a.coordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe,
        Trivialization.coordChangeL_apply]
      exacts [rfl, hb]

Goal state after: