mathlib-initiative/mathlib-tactics huggingface dataset:
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 e' : OpenPartialHomeomorph H₃ H₁}, e ∈ atlas H₁ H₃ → e' ∈ atlas H₁ H₃ → e.symm ≫ₕ e' ∈ G₁

Tactic:
rintro _ _ ⟨e, he, f, hf, rfl⟩ ⟨e', he', f', hf', rfl⟩
      apply G₁.locality
      intro x hx
      simp only [mfld_simps] at hx
      have hxs : x ∈ f.symm ⁻¹' (e.symm ≫ₕ e').source := by simp only [hx, mfld_simps]
      have hxs' : x ∈ f.target ∩
          f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ e.symm ≫ₕ e' ⁻¹' f'.source) := by
        simp only [hx, mfld_simps]
      obtain ⟨φ, hφG₁, hφ, hφ_dom⟩ := LocalInvariantProp.liftPropOn_indep_chart
        (isLocalStructomorphWithinAt_localInvariantProp G₁) (G₁.subset_maximalAtlas hf)
        (G₁.subset_maximalAtlas hf') (H _ (G₂.compatible he he')) hxs' hxs
      simp_rw [← OpenPartialHomeomorph.coe_trans, OpenPartialHomeomorph.trans_assoc] at hφ
      simp_rw [OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm,
        OpenPartialHomeomorph.trans_assoc]
      have hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source :=
        (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source
      refine ⟨_, hs.inter φ.open_source, ?_, ?_⟩
      · simp only [hx, hφ_dom, mfld_simps]
      · refine G₁.mem_of_eqOnSource (closedUnderRestriction' hφG₁ hs) ?_
        rw [OpenPartialHomeomorph.restr_source_inter]
        refine OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source (hφ.mono ?_)
        mfld_set_tac

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 : ℕ∞ω
t : Set M'
g : M' → M''
x : M
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑(extChartAt I' (f x)).symm)
      (↑(extChartAt I' (f x)).symm ⁻¹' t ∩ range ↑I') (↑(extChartAt I' (f x)) (f x))
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)

Tactic:
set e' := extChartAt I' (f x)

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
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 : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I') (↑e' (f x))
hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)
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'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
inst✝ : One M'
f : M → M'
hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x
⊢ ContMDiff I I' n f

Tactic:
intro x
  by_cases hx : x ∈ mulTSupport f
  · exact hf x hx
  · exact ContMDiffAt.congr_of_eventuallyEq contMDiffAt_const
      (notMem_mulTSupport_iff_eventuallyEq.1 hx)

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
x x' : M
y : M'
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
⊢ ContinuousWithinAt f s x' →
    (ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x') ↔
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑e.symm)
        (e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) (↑e x'))

Tactic:
set e' := extChartAt I' (f x)

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x x' : M
y : M'
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
⊢ ContinuousWithinAt f s x' →
    (ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x') ↔
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑e.symm)
        (e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) (↑e x'))
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
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
g : E → F
⊢ ∫ (x : E) in f '' s, g x ∂μ = ∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ

Tactic:
rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
    (measurableEmbedding_of_fderivWithin hs hf' hf).integral_map]
  simp only [Set.domRestrict_apply, ← Function.comp_apply (f := g), ENNReal.ofReal]
  rw [← (MeasurableEmbedding.subtype_coe hs).integral_map, map_comap_subtype_coe hs,
    setIntegral_withDensity_eq_setIntegral_smul₀
      (aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf') _ hs]
  congr with x
  rw [NNReal.smul_def, Real.coe_toNNReal _ (abs_nonneg (f' x).det)]

Goal state after:
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)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen[inst✝⁷] (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
p : ↑e.source
⊢ (e.restr (s p)).source = u p ×ˢ univ

Tactic:
exact (heφ p).1

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
x : M
⊢ UniqueMDiffAt[univ] x

Tactic:
unfold UniqueMDiffWithinAt
  simp only [preimage_univ, univ_inter]
  exact I.uniqueDiffOn _ (mem_range_self _)

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

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

Tactic:
have hΦ : ∀ (y) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩ := fun y hy => dif_pos hy

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

Tactic:
← mdifferentiableWithinAt_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'
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
⊢ ContinuousAt f x ∧ MDiffAt[univ] (↑(extChartAt I' y) ∘ f) x ↔
    ContinuousAt f x ∧ MDiffAt[univ] (↑(extChartAt I' y) ∘ f) x
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x' : M
y : M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
⊢ ContinuousWithinAt f s x' →
    (DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x') ↔
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑e.symm)
        (e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) (↑e x'))

Tactic:
set e' := extChartAt I' (f x)

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
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x' : M
y : M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
⊢ ContinuousWithinAt f s x' →
    (DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x') ↔
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑e.symm)
        (e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) (↑e 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✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
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
⊢ Continuous[inst✝⁸, inst✝⁸]
    (↑(if hb : b ∈ e.baseSet ∩ e'.baseSet then (linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯
        else LinearEquiv.refl R F)).toFun

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✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
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
⊢ Continuous[inst✝⁸, inst✝⁸]
    (↑(if hb : b ∈ e.baseSet ∩ e'.baseSet then (linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯
        else LinearEquiv.refl R F)).toFun

Tactic:
· rw [dif_pos hb]
        refine (e'.continuousOn.comp_continuous ?_ ?_).snd
        · exact e.continuousOn_symm.comp_continuous (Continuous.prodMk_right b) fun y =>
            mk_mem_prod hb.1 (mem_univ y)
        · exact fun y => e'.mem_source.mpr hb.2

Goal state after:
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✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
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
⊢ Continuous[inst✝⁸, inst✝⁸]
    (↑(if hb : b ∈ e.baseSet ∩ e'.baseSet then (linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯
        else LinearEquiv.refl R F)).toFun
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
⊢ Continuous[inst✝² b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦
    if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
refine continuous_if_const _ (fun hb => ?_) fun _ => continuous_zero

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
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
⊢ Continuous[inst✝² b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦ (↑e { proj := b, snd := y }).2
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
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
h : MDiffAt f p.proj
⊢ tangentMapWithin I I' f s p = tangentMap I I' f p

Tactic:
← mdifferentiableWithinAt_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'
s : Set M
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
h : MDiffAt[univ] f p.proj
⊢ tangentMapWithin I I' f s p = tangentMap I I' f p
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet ∧ b ∈ (Z.localTriv j).baseSet
v : F
⊢ (Trivialization.coordChangeL R (Z.localTriv i) (Z.localTriv j) b) v = (Z.coordChange i j b) v

Tactic:
rw [Trivialization.coordChangeL_apply', localTriv_symm_fst, localTriv_apply, coordChange_comp]
  exacts [⟨⟨hb.1, Z.mem_baseSet_at b⟩, hb.2⟩, hb]

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 t : Set M
h : s =ᶠ[𝓝 x] t
⊢ MDiffAt[s] f x ↔ MDiffAt[t] f x

Tactic:
by
  simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]
  exact exists_congr fun _ => hasMFDerivWithinAt_congr_set h

Goal state after: