mathlib-initiative/mathlib-tactics huggingface dataset:
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'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ (∀ (x : M), ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)) ↔
    Continuous[inst✝⁴, inst✝¹] f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
forall_and,

Goal state after:
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'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ ((∀ (x : M), ContinuousAt f x) ∧
      ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)) ↔
    Continuous[inst✝⁴, inst✝¹] f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case pos.hs
𝕜 : 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
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Convex ℝ (range ↑I)

Tactic:
apply I.convex_range

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this✝¹ : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')

Tactic:
let := NormedSpace.restrictScalars ℝ 𝕜 E'

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this✝² : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')
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
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
⊢ LiftPropAt P f ↑x ↔ LiftPropAt P (f ∘ Subtype.val) x

Tactic:
by
  simp only [LiftPropAt, liftPropWithinAt_iff']
  congrm ?_ ∧ ?_
  · simp_rw [continuousWithinAt_univ, U.isOpenEmbedding'.continuousAt_iff]
  · apply hG.congr_iff
    exact (U.chartAt_subtype_val_symm_eventuallyEq).fun_comp (chartAt H' (f x) ∘ f)

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

Goal state before:
pp: case mp.refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ (e.restr f.source).source ⊆ f.source

pp: case mp.refine_2
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ EqOn (↑f) (↑(e.restr f.source)) (s ∩ (e.restr f.source).source)

pp: case mp.refine_3
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ x ∈ interior f.source

Tactic:
· simp_rw [OpenPartialHomeomorph.restr_source]
      exact inter_subset_right.trans interior_subset

Goal state after:
case mp.refine_2
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ EqOn (↑f) (↑(e.restr f.source)) (s ∩ (e.restr f.source).source)

case mp.refine_3
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ x ∈ interior f.source
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✝
inst✝ : ChartedSpace H✝ M
x : M
H : interior (extChartAt I x).target = ∅
⊢ False

Tactic:
have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) x)

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✝
inst✝ : ChartedSpace H✝ M
x : M
H : interior (extChartAt I x).target = ∅
this :
  ↑(extChartAt I x) x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x).target)
⊢ False
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
⊢ ↑(extChartAt I x₀) x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (interior (↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target))

Tactic:
simp_rw [mem_closure_iff, interior_inter, ← inter_assoc]

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),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o →
      ↑(extChartAt I x₀) x ∈ o →
        (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
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
this : (e.symm ≫ₕ e').source = ∅
⊢ t = ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I

Tactic:
rw [← Subtype.preimage_val_eq_preimage_val_iff]

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 (↑I' ∘ f) s x

Tactic:
by
  simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]

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'},
    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 x f e' he' hs hx h

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'
he' : e' ∈ contDiffGroupoid 1 I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : 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 t : Set M
x : M
n : ℕ∞ω
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x

Tactic:
have : T1Space M := I.t1Space M

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 t : Set M
x : M
n : ℕ∞ω
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t 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
h : MDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] f x
⊢ f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x

Tactic:
apply hf.1.preimage_mem_nhdsWithin

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
n : WithTop ℕ∞
hf : ContMDiffWithinAt I I' n f s x
hn : n ≠ 0
h : MDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] f x
⊢ (extChartAt I' (f x)).source ∈ 𝓝 (f 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) (induced Prod.fst inst✝¹) ⊓
      induced (pullbackTotalSpaceEmbedding f) (induced Prod.snd inst✝)

Tactic:
induced_compose,

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
⊢ Pullback.TotalSpace.topologicalSpace F E f =
    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' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
⊢ HasMFDerivAt[insert y s] f x f' ↔ HasMFDerivAt[s] f x f'

Tactic:
have : T1Space M := I.t1Space M

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)
y : M
this : T1Space M
⊢ HasMFDerivAt[insert y s] f x f' ↔ HasMFDerivAt[s] f x f'
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
this : T1Space M
⊢ HasMFDerivAt[insert y s] f x f' ↔ HasMFDerivAt[s] f x f'

Tactic:
refine ⟨fun h => h.mono <| subset_insert y s, fun 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)
y : M
this : T1Space M
hf : HasMFDerivAt[s] f x f'
⊢ HasMFDerivAt[insert y s] f x f'
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: case inr
𝕜 : 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
y : M
h : x ≠ y
⊢ MDiffAt[insert y s] f x ↔ MDiffAt[s] f x

Tactic:
have : T1Space M := I.t1Space M

Goal state after:
case inr
𝕜 : 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
y : M
h : x ≠ y
this : T1Space M
⊢ MDiffAt[insert y s] f x ↔ MDiffAt[s] 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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝[≠] ↑(extChartAt I x) x] ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I

Tactic:
have : T1Space M := I.t1Space M

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
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝[≠] ↑(extChartAt I x) x] ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
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
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasMFDerivAt[s] f x f' ↔ HasMFDerivAt[t] f x f'

Tactic:
have : T1Space M := I.t1Space M

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 t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ HasMFDerivAt[s] f x f' ↔ HasMFDerivAt[t] f x f'
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
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : ContinuousOn (fun x ↦ (a.coordChange he' he x.1) x.2) ((e'.baseSet ∩ e.baseSet) ×ˢ univ)
⊢ ContinuousOn (↑e ∘ ↑e'.symm) ((e'.baseSet ∩ e.baseSet) ×ˢ univ)

Tactic:
refine (continuousOn_fst.prodMk this).congr ?_

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✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : ContinuousOn (fun x ↦ (a.coordChange he' he x.1) x.2) ((e'.baseSet ∩ e.baseSet) ×ˢ univ)
⊢ EqOn (↑e ∘ ↑e'.symm) (fun x ↦ (x.1, (a.coordChange he' he x.1) x.2)) ((e'.baseSet ∩ e.baseSet) ×ˢ univ)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: case neg
𝕜 : 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
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : ¬MDiffAt[s] f x
⊢ mfderiv[s] f₁ x = mfderiv[s] f x

Tactic:
· unfold mfderivWithin
    rw [if_neg h, if_neg]
    rwa [← hL.mdifferentiableWithinAt_iff hx]

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

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
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
inst✝ : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x₀ ↔
    ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) x₀

Tactic:
by
  simp_rw [contMDiffAt_totalSpace, and_iff_right_iff_imp]; intro; exact contMDiffAt_id

Goal state after: