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

Goal state before:
pp: case refine_3
𝕜 : 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
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContinuousWithinAt f s y ∧
    ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
      (↑(φ.extend I) y)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
    (↑(φ.extend I) y)

Tactic:
contMDiffWithinAt_iff_contDiffWithinAt

Goal state after:
case refine_3
𝕜 : 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
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContinuousWithinAt f s y ∧
    ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
      (↑(φ.extend I) y)
⊢ ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I) (↑(φ.extend I) y)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: case right
𝕜 : 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)
hs : HasMFDerivAt[s] f x f'
ht : HasMFDerivAt[t] f x f'
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' (s ∪ t) ∩ range ↑I)
    (↑(extChartAt I x) x)

Tactic:
convert! HasFDerivWithinAt.union hs.2 ht.2 using 1

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)
hs : HasMFDerivAt[s] f x f'
ht : HasMFDerivAt[t] f x f'
⊢ ↑(extChartAt I x).symm ⁻¹' (s ∪ t) ∩ range ↑I =
    ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I ∪ ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case fst
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)
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
y : F
⊢ (b, (coordChangeL R e e' b) y).1 = (↑e.symm (b, y)).proj

pp: case fst
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)
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
y : F
⊢ (↑e.symm (b, y)).proj ∈ e'.baseSet

Tactic:
e.proj_symm_apply' hb.1

Goal state after:
case fst
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)
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
y : F
⊢ (b, (coordChangeL R e e' b) y).1 = b

case fst
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)
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
y : F
⊢ (↑e.symm (b, y)).proj ∈ e'.baseSet
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case fst
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)
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
y : F
⊢ (↑e.symm (b, y)).proj ∈ e'.baseSet

Tactic:
e.proj_symm_apply' hb.1

Goal state after:
case fst
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)
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
y : F
⊢ b ∈ e'.baseSet
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
y : M
⊢ MDiffAt[insert y s] f x ↔ MDiffAt[s] f x

Tactic:
rcases eq_or_ne x y with (rfl | h)

Goal state after:
case inl
𝕜 : 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
⊢ MDiffAt[insert x s] f x ↔ MDiffAt[s] f x

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
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
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
⊢ ⟨p.proj, (mfderiv[s] id p.proj) p.snd⟩ = p

Tactic:
rw [mfderivWithin_id]

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
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
⊢ ⟨p.proj, (ContinuousLinearMap.id 𝕜 (TangentSpace I p.proj)) p.snd⟩ = p

𝕜 : 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
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
⊢ UniqueMDiffAt[s] p.proj
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case fst
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 e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (b, (a.coordChange he he' b) v).1 = (↑e.symm (b, v)).proj

pp: case fst
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 e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑e.symm (b, v)).proj ∈ e'.baseSet

Tactic:
e.proj_symm_apply' hb.1

Goal state after:
case fst
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 e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (b, (a.coordChange he he' b) v).1 = b

case fst
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 e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑e.symm (b, v)).proj ∈ e'.baseSet
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case fst
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 e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑e.symm (b, v)).proj ∈ e'.baseSet

Tactic:
e.proj_symm_apply' hb.1

Goal state after:
case fst
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 e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ e'.baseSet
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:
contMDiffAt_totalSpace,

Goal state after:
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 n (fun x ↦ x) x₀ ∧
      ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) x₀ ↔
    ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) 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'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
s : Set M
p : M × M'
t : Set M'
f : M → N
g : M' → N'
hf : MDiffAt[s] f p.1
hg : MDiffAt[t] g p.2
hs : UniqueMDiffAt[s] p.1
ht : UniqueMDiffAt[t] p.2
hf' : HasMFDerivAt[Prod.fst '' s ×ˢ t] f p.1 (mfderiv[s] f p.1)
hg' : HasMFDerivAt[Prod.snd '' s ×ˢ t] g p.2 (mfderiv[t] g p.2)
⊢ mfderiv[s ×ˢ t] (Prod.map f g) p = (mfderiv[s] f p.1).prodMap (mfderiv[t] g p.2)

Tactic:
exact (hf'.prodMap hg').mfderivWithin (hs.prod ht)

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
inst✝ : IsManifold IB n B
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 ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)) e.source

Tactic:
rw [EqOnSource.source_eq heφ]

Goal state after:
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
inst✝ : IsManifold IB n B
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 ⋯ ⋯)
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯))
    (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯).source
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E →L[𝕜] E) n ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm)
    (↑((↑i).extend I) '' ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j))

pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ (tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j ⊆ (↑i).source

Tactic:
contMDiffOn_iff_contDiffOn

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ContDiffOn 𝕜 n ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm)
    (↑((↑i).extend I) '' ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j))

𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ (tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j ⊆ (↑i).source
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
⊢ t ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x))

Tactic:
Filter.inter_mem_iff

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
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
⊢ ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x)) ∧
    range ↑I ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x))