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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) '' s ∈ 𝓝 (↑(f.extend I) x)

Tactic:
rw [← f.map_extend_nhds_of_boundaryless hx, Filter.mem_map]

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) ⁻¹' ↑(f.extend I) '' s ∈ 𝓝 x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case refine_1
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ ContinuousWithinAt f s x

pp: case refine_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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)

Tactic:
· have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
    simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range,
      inter_univ] at this
    rwa [Function.comp_assoc, I.symm_comp_self] at this

Goal state after:
case refine_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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P g t x

Tactic:
by
  rw [← hG.liftPropWithinAt_inter (s := s) hu, ← hG.liftPropWithinAt_inter (s := t) hu,
    ← eq_iff_iff]
  congr 1
  aesop

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
inst✝ : IsEmpty M
e e' : OpenPartialHomeomorph M H
a✝¹ : e ∈ atlas H M
a✝ : e' ∈ atlas H M
x : E
t : Set E := ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
hx : x ∈ t
⊢ e.symm.source ∩ ↑e.symm ⁻¹' e'.source = e.symm.source ∩ ↑e.symm ⁻¹' ∅

Tactic:
rw [eq_empty_of_isEmpty (e'.source)]

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

Goal state before:
pp: case hn
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
⊢ Pairwise (Disjoint on fun i ↦ f '' (s ∩ t i))

Tactic:
intro i j hij

Goal state after:
case hn
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
i j : ℕ
hij : i ≠ j
⊢ (Disjoint on fun i ↦ f '' (s ∩ t i)) i j
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 : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ↑I.symm ⁻¹' s ∈ 𝓝[↑I.symm ⁻¹' t ∩ range ↑I] ↑I x

Tactic:
rwa [← Filter.mem_map, ← I.image_eq, I.symm_map_nhdsWithin_image]

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

Goal state before:
pp: case hn
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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ Pairwise (Disjoint on fun i ↦ f '' (s ∩ u i))

Tactic:
intro i j hij

Goal state after:
case hn
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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
i j : ℕ
hij : i ≠ j
⊢ (Disjoint on fun i ↦ f '' (s ∩ u i)) i j
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
x : M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' n) (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    LiftPropWithinAt (ContDiffWithinAtProp 𝓘(𝕜, E) I' n) (f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ range ↑I)
      (↑(e.extend I) x)

Tactic:
StructureGroupoid.liftPropWithinAt_self_source,

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
x : M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ ContinuousWithinAt (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' ((f ∘ ↑e.symm) (↑e x))) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    ContinuousWithinAt (f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x) ∧
      ContDiffWithinAtProp 𝓘(𝕜, E) I' n
        (↑(chartAt H' ((f ∘ ↑(e.extend I).symm) (↑(e.extend I) x))) ∘ f ∘ ↑(e.extend I).symm)
        (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : Mul G
inst✝¹ : TopologicalSpace G
inst✝ : ChartedSpace H G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffMul I n G
⊢ ContMDiffMul I m G

Tactic:
have : IsManifold I m G := IsManifold.of_le hmn
  exact ⟨h.contMDiff_mul.of_le hmn⟩

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 : ℕ∞ω
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:
simp only [mfld_simps, IsManifold.mem_maximalAtlas_iff, StructureGroupoid.maximalAtlas,
    contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid,
    ← contMDiffOn_iff_contDiffOn]

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
n : ℕ∞ω
inst✝ : IsManifold I n M
φ : OpenPartialHomeomorph M H
hφ : ContMDiffOn I I n (↑φ) φ.source
hφ' : ContMDiffOn I I n (↑φ.symm) φ.target
⊢ ∀ e' ∈ atlas H M,
    (ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E) n (↑I ∘ (↑e' ∘ ↑φ.symm) ∘ ↑I.symm)
          (↑I.symm ⁻¹' φ.target ∩ ↑I.symm ⁻¹' ↑φ.symm ⁻¹' e'.source ∩ range ↑I) ∧
        ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E) n (↑I ∘ (↑φ ∘ ↑e'.symm) ∘ ↑I.symm)
          (↑I.symm ⁻¹' e'.target ∩ ↑I.symm ⁻¹' ↑e'.symm ⁻¹' φ.source ∩ range ↑I)) ∧
      ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E) n (↑I ∘ (↑φ ∘ ↑e'.symm) ∘ ↑I.symm)
          (↑I.symm ⁻¹' e'.target ∩ ↑I.symm ⁻¹' ↑e'.symm ⁻¹' φ.source ∩ range ↑I) ∧
        ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E) n (↑I ∘ (↑e' ∘ ↑φ.symm) ∘ ↑I.symm)
          (↑I.symm ⁻¹' φ.target ∩ ↑I.symm ⁻¹' ↑φ.symm ⁻¹' e'.source ∩ range ↑I)
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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
h1 : c' = chartAt H (↑f x)
h2 : ↑c' ∘ ↑f ∘ ↑c.symm = ↑(c.symm ≫ₕ f ≫ₕ c')
hcx : ↑c x ∈ ↑c.symm ⁻¹' f.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧ EqOn (↑(c.symm ≫ₕ f ≫ₕ c')) (↑e) e.source ∧ ↑c x ∈ e.source

Tactic:
← h1,

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
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑c' ∘ ↑f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' f.source)
    (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
h1 : c' = chartAt H (↑f x)
h2 : ↑c' ∘ ↑f ∘ ↑c.symm = ↑(c.symm ≫ₕ f ≫ₕ c')
hcx : ↑c x ∈ ↑c.symm ⁻¹' f.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧ EqOn (↑(c.symm ≫ₕ f ≫ₕ c')) (↑e) e.source ∧ ↑c x ∈ e.source
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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source
hex : ↑c x ∈ e.source
⊢ ↑f.symm X ∈ c.source

Tactic:
simp only [c, x, 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
x : M
⊢ UniqueMDiffAt[univ] x

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

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
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I 1 M
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    LiftPropWithinAt (DifferentiableWithinAtProp 𝓘(𝕜, E) I') (f ∘ ↑(e.extend I).symm)
      (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)

Tactic:
StructureGroupoid.liftPropWithinAt_self_source,

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
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I 1 M
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ ContinuousWithinAt (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      DifferentiableWithinAtProp I I' (↑(chartAt H' ((f ∘ ↑e.symm) (↑e x))) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    ContinuousWithinAt (f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x) ∧
      DifferentiableWithinAtProp 𝓘(𝕜, E) I'
        (↑(chartAt H' ((f ∘ ↑(e.extend I).symm) (↑(e.extend I) x))) ∘ f ∘ ↑(e.extend I).symm)
        (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding f) instTopologicalSpaceProd

Tactic:
simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose,
    Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]

Goal state after:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ =
    induced (Prod.fst ∘ pullbackTotalSpaceEmbedding f) inst✝¹ ⊓ induced (Prod.snd ∘ pullbackTotalSpaceEmbedding f) inst✝
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
⊢ (∃ f', HasMFDerivAt[s] f x f') → MDiffAt[s] f x

Tactic:
rintro ⟨f', hf'⟩

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

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:
Module: Mathlib.Topology.VectorBundle.Constructions

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
⊢ ∀ (e : Trivialization (F₁ × F₂) TotalSpace.proj) [MemTrivializationAtlas e], Trivialization.IsLinear 𝕜 e

Tactic:
by
    rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩
    infer_instance

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
x : M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I)
    (↑(extChartAt I x) x)

Tactic:
have : ∀ᶠ y in 𝓝[range I] (extChartAt I x) x, (extChartAt I x ∘ (extChartAt I x).symm) y = y := by
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
    mfld_set_tac

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
x : M
this : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I)
    (↑(extChartAt I x) 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
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'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffAt[s] x
⊢ mfderiv[s] Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]; exact mfderiv_fst

Goal state after: