mathlib-initiative/mathlib-tactics huggingface dataset:
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'
x : M
n : ℕ∞ω
⊢ ContMDiffWithinAt I I' n f univ x ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
contMDiffWithinAt_iff_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
n : ℕ∞ω
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I)
      (↑(extChartAt I x) x) ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)
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} {u : Set H} {f : H → H'},
    IsOpen[inst✝³] u → x ∈ u → (DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x)

Tactic:
intro s

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
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} {u : Set H} {f : H → H'},
    IsOpen[inst✝³] u → x ∈ u → (DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x)
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},
    e ∈ contDiffGroupoid 1 I →
      x ∈ e.source →
        DifferentiableWithinAtProp I I' f s x → DifferentiableWithinAtProp I I' (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
intro s

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
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},
    e ∈ contDiffGroupoid 1 I →
      x ∈ e.source →
        DifferentiableWithinAtProp I I' f s x → DifferentiableWithinAtProp I I' (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
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
g : E → ℝ≥0∞
⊢ ∫⁻ (a : ↑s), (g ∘ f) ↑a ∂Measure.comap Subtype.val (μ.withDensity fun x ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ

Tactic:
← (MeasurableEmbedding.subtype_coe hs).lintegral_map,

Goal state after:
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
g : E → ℝ≥0∞
⊢ ∫⁻ (a : E),
      (g ∘ f)
        a ∂Measure.map Subtype.val (Measure.comap Subtype.val (μ.withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
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 g : H → H'},
    (∀ y ∈ s, f y = g y) → f x = g x → DifferentiableWithinAtProp I I' f s x → DifferentiableWithinAtProp I I' g s x

Tactic:
intro s

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
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'},
    (∀ y ∈ s, f y = g y) → f x = g x → DifferentiableWithinAtProp I I' f s x → DifferentiableWithinAtProp I I' g s x
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'},
    e' ∈ contDiffGroupoid 1 I' →
      s ⊆ f ⁻¹' e'.source →
        f x ∈ e'.source → DifferentiableWithinAtProp I I' f s x → DifferentiableWithinAtProp I I' (↑e' ∘ f) s x

Tactic:
intro s

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
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'},
    e' ∈ contDiffGroupoid 1 I' →
      s ⊆ f ⁻¹' e'.source →
        f x ∈ e'.source → DifferentiableWithinAtProp I I' f s x → DifferentiableWithinAtProp I I' (↑e' ∘ f) s x
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 : M
n : ℕ∞
⊢ ContMDiffWithinAt I I' (↑n) f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContMDiffWithinAt I I' (↑m) f s x

Tactic:
refine ⟨fun h m hm => h.of_le (mod_cast hm), fun h => ?_⟩
  obtain - | n := n
  · exact contMDiffWithinAt_infty.2 fun n => h n le_top
  · exact h n le_rfl

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 : M
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContMDiffWithinAt I I' n f s x
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u)

Tactic:
have : IsManifold I m M := .of_le hm
  have : IsManifold I' m M' := .of_le hm
  match m with
  | (m : ℕ) | ω =>
    rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp)).1 (h.of_le hm) with ⟨t, ht, h't⟩
    rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
    rw [inter_comm] at hu
    exact ⟨u, u_open, xu, h't.mono hu⟩
  | ∞ =>
    rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp [h'])).1 h with ⟨t, ht, h't⟩
    rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
    rw [inter_comm] at hu
    exact ⟨u, u_open, xu, (h't.mono hu).of_le hm⟩

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 : ℕ∞ω
x : M
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑(extChartAt I x)) x

Tactic:
contMDiffAt_iff_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
n : ℕ∞ω
x : M
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) 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
n : WithTop ℕ∞
hf : ContMDiffWithinAt I I' n f s x
hn : n ≠ 0
⊢ MDiffAt[s] f x

Tactic:
suffices h : MDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] f x by
    rwa [mdifferentiableWithinAt_inter'] at h
    apply hf.1.preimage_mem_nhdsWithin
    exact extChartAt_source_mem_nhds (f x)
  rw [mdifferentiableWithinAt_iff]
  exact ⟨hf.1.mono inter_subset_left, (hf.2.differentiableWithinAt hn).mono (by mfld_set_tac)⟩

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

Goal state before:
pp: case refine_1
𝕜 : 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' ⋯ ⋯)
⊢ ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑((fun b ↦ (φ b).trans (φ' b)) x)) (U ∩ U')

Tactic:
change
        ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n
          (fun x : B => (φ' x).toContinuousLinearMap ∘L (φ x).toContinuousLinearMap) (U ∩ U')

Goal state after:
case refine_1
𝕜 : 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' ⋯ ⋯)
⊢ ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ' x) ∘SL ↑(φ x)) (U ∩ U')
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
⊢ ⇑(Pretrivialization.linearMapAt R e b) = fun y ↦ if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
rw [Pretrivialization.linearMapAt]

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
⊢ ⇑(if hb : b ∈ e.baseSet then ↑(linearEquivAt R e b hb) else 0) = fun y ↦
    if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
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' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
⊢ HasMFDerivAt[s \ {y}] f x f' ↔ HasMFDerivAt[s] f x f'

Tactic:
rw [← hasMFDerivWithinAt_insert, insert_sdiff_singleton, hasMFDerivWithinAt_insert]

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
s : Set M
x : M
hxs : UniqueMDiffAt[s] x
⊢ mfderiv[s] id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_id hxs]

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
s : Set M
x : M
hxs : UniqueMDiffAt[s] x
⊢ mfderiv% id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case refine_2
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁹ : NormedAddCommGroup EB
inst✝¹⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁶ : TopologicalSpace B
inst✝¹⁵ : ChartedSpace HB B
EM : Type u_9
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
inst✝ : IsManifold IB n B
e : Trivialization F TotalSpace.proj
he : e ∈ trivializationAtlas F E
e' : Trivialization F TotalSpace.proj
he' : e' ∈ trivializationAtlas F E
this✝ : MemTrivializationAtlas e
this : MemTrivializationAtlas e'
⊢ EqOn (↑(FiberwiseLinear.openPartialHomeomorph (Trivialization.coordChangeL 𝕜 e e') ⋯ ⋯ ⋯))
    (↑(((fun e ↦ e.toOpenPartialHomeomorph) e).symm ≫ₕ (fun e ↦ e.toOpenPartialHomeomorph) e'))
    (FiberwiseLinear.openPartialHomeomorph (Trivialization.coordChangeL 𝕜 e e') ⋯ ⋯ ⋯).source

Tactic:
rintro ⟨b, v⟩ hb

Goal state after:
case refine_2
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁹ : NormedAddCommGroup EB
inst✝¹⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁶ : TopologicalSpace B
inst✝¹⁵ : ChartedSpace HB B
EM : Type u_9
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
inst✝ : IsManifold IB n B
e : Trivialization F TotalSpace.proj
he : e ∈ trivializationAtlas F E
e' : Trivialization F TotalSpace.proj
he' : e' ∈ trivializationAtlas F E
this✝ : MemTrivializationAtlas e
this : MemTrivializationAtlas e'
b : B
v : F
hb : (b, v) ∈ (FiberwiseLinear.openPartialHomeomorph (Trivialization.coordChangeL 𝕜 e e') ⋯ ⋯ ⋯).source
⊢ ↑(FiberwiseLinear.openPartialHomeomorph (Trivialization.coordChangeL 𝕜 e e') ⋯ ⋯ ⋯) (b, v) =
    ↑(((fun e ↦ e.toOpenPartialHomeomorph) e).symm ≫ₕ (fun e ↦ e.toOpenPartialHomeomorph) e') (b, v)
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
hy : y ∈ t
⊢ ↑I
      (Function.extend Sum.inr (↑(chartAt H x)) (fun x_1 ↦ Classical.arbitrary H)
        (Sum.inr (↑(chartAt H x).symm (↑I.symm y)))) =
    y

Tactic:
rw [Sum.inr_injective.extend_apply, (chartAt H x).right_inv (by grind)]

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
hy : y ∈ t
⊢ ↑I (↑I.symm y) = y
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : EqOn (writtenInExtChartAt I I (Sum.inl x) Sum.swap) id t
⊢ (chartAt H x).target ∈ 𝓝 (↑I.symm (↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x))))

Tactic:
exact (chartAt H x).open_target.mem_nhds (by simp)

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

Goal state before:
pp: case refine_1
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝³⁸ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝³⁷ : NormedAddCommGroup EB
inst✝³⁶ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³⁵ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝³⁴ : TopologicalSpace B
inst✝³³ : ChartedSpace HB B
EM : Type u_9
inst✝³² : NormedAddCommGroup EM
inst✝³¹ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝³⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝²⁹ : TopologicalSpace M
inst✝²⁸ : ChartedSpace HM M
inst✝²⁷ : (x : B) → AddCommMonoid (E x)
inst✝²⁶ : (x : B) → Module 𝕜 (E x)
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
inst✝²³ : TopologicalSpace (TotalSpace F E)
inst✝²² : (x : B) → TopologicalSpace (E x)
inst✝²¹ : FiberBundle F E
inst✝²⁰ : VectorBundle 𝕜 F E
inst✝¹⁹ : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹⁵ : (x : B) → AddCommMonoid (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
F₂ : Type u_13
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)
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₂
inst✝² : ContMDiffVectorBundle n F₁ E₁ IB
inst✝¹ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝ : IsManifold IB n B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
i₁ : MemTrivializationAtlas e₁
i₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
i₁' : MemTrivializationAtlas e₁'
i₂' : MemTrivializationAtlas e₂'
⊢ ContMDiffOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) n (fun y ↦ ↑(Trivialization.coordChangeL 𝕜 e₁ e₁' y))
    ((e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet)

Tactic:
refine (contMDiffOn_coordChangeL e₁ e₁').mono ?_
      simp only [Trivialization.prod_baseSet, mfld_simps]
      mfld_set_tac

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : EqOn (writtenInExtChartAt I I (Sum.inr x) Sum.swap) id t
⊢ (chartAt H x).target ∈ 𝓝 (↑I.symm (↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))))

Tactic:
exact (chartAt H x).open_target.mem_nhds (by simp)

Goal state after: