mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 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
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
this✝ : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
this : (extChartAt I x).target ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' insert x s ∩ range ↑I] ↑(extChartAt I x) x
z : E
h'z : z ∈ (extChartAt I x).target
hz : ↑(extChartAt I x).symm z = x ∨ ↑(extChartAt I x).symm z ∈ s
h2z : ∃ y, ↑I y = z
⊢ z = ↑(extChartAt I x) x ∨ ↑(extChartAt I x).symm z ∈ s ∧ ∃ y, ↑I y = z

Tactic:
rcases hz with xz | h'z

Goal state after:
case inl.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
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
this✝ : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
this : (extChartAt I x).target ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' insert x s ∩ range ↑I] ↑(extChartAt I x) x
z : E
h'z : z ∈ (extChartAt I x).target
h2z : ∃ y, ↑I y = z
xz : ↑(extChartAt I x).symm z = x
⊢ z = ↑(extChartAt I x) x ∨ ↑(extChartAt I x).symm z ∈ s ∧ ∃ y, ↑I y = z

case inl.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
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
this✝ : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
this : (extChartAt I x).target ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' insert x s ∩ range ↑I] ↑(extChartAt I x) x
z : E
h'z✝ : z ∈ (extChartAt I x).target
h2z : ∃ y, ↑I y = z
h'z : ↑(extChartAt I x).symm z ∈ s
⊢ z = ↑(extChartAt I x) x ∨ ↑(extChartAt I x).symm z ∈ s ∧ ∃ y, ↑I y = z
Module: Mathlib.Topology.VectorBundle.Constructions

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
⊢ Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F

Tactic:
ext v

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b) v = (ContinuousLinearEquiv.refl 𝕜 F) v
Module: Mathlib.Topology.VectorBundle.Constructions

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
x : B
⊢ Trivialization.linearMapAt 𝕜 (trivialization B F) x = LinearMap.id

Tactic:
ext v

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
x : B
v : Trivial B F x
⊢ (Trivialization.linearMapAt 𝕜 (trivialization B F) x) v = LinearMap.id v
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁰ : NontriviallyNormedField R
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module R (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace R F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → TopologicalSpace (E x)
inst✝² : FiberBundle F E
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ (continuousLinearEquivAt R e b ⋯).symm.trans (continuousLinearEquivAt R e' b ⋯) = coordChangeL R e e' b

Tactic:
ext v

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁰ : NontriviallyNormedField R
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module R (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace R F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → TopologicalSpace (E x)
inst✝² : FiberBundle F E
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((continuousLinearEquivAt R e b ⋯).symm.trans (continuousLinearEquivAt R e' b ⋯)) v = (coordChangeL R e e' b) v
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k
⊢ Z.coordChange j k x ∘SL Z.coordChange i j x = Z.coordChange i k x

Tactic:
ext v

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k
v : F
⊢ (Z.coordChange j k x ∘SL Z.coordChange i j x) v = (Z.coordChange i k x) v
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i✝ j i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
⊢ ↑(Trivialization.coordChangeL R (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i') b) =
    Z.coordChange i i' b

Tactic:
ext v

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i✝ j i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
v : F
⊢ ↑(Trivialization.coordChangeL R (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i') b) v =
    (Z.coordChange i i' b) v
Module: Mathlib.Topology.VectorBundle.Constructions

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹² : TopologicalSpace B'
inst✝¹¹ : TopologicalSpace (TotalSpace F E)
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : (x : B) → AddCommMonoid (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝⁴ : FunLike K B' B
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : f b ∈ e.baseSet ∩ e'.baseSet
⊢ (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 (e.pullback f) (e'.pullback f) b)) b =
    ((fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ⇑f) b

Tactic:
ext v

Goal state after:
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹² : TopologicalSpace B'
inst✝¹¹ : TopologicalSpace (TotalSpace F E)
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : (x : B) → AddCommMonoid (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝⁴ : FunLike K B' B
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((fun b ↦ ↑(Trivialization.coordChangeL 𝕜 (e.pullback f) (e'.pullback f) b)) b) v =
    (((fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ⇑f) b) v
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
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
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
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝[≠] ↑(extChartAt I x) x] ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I

Tactic:
exact preimage_extChartAt_eventuallyEq_compl_singleton y h

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

Goal state before:
pp: case pos
𝕜 : 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : MDiffAt[s] f x
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝[≠] ↑(extChartAt I x) x] ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I

Tactic:
exact preimage_extChartAt_eventuallyEq_compl_singleton y h

Goal state after:
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
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
        (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) =
    a.coordChange he he' b

Tactic:
ext v

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
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)
      v =
    (a.coordChange he he' b) v
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: 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
e e' : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
he' : MemTrivializationAtlas e'
⊢ ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) 0 (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
contMDiffOn_zero_iff

Goal state after:
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
e e' : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
he' : MemTrivializationAtlas e'
⊢ ContinuousOn (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: 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
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst✝ : Z.IsContMDiff IB n
i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
⊢ ↑(Trivialization.coordChangeL 𝕜 (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i') b) =
    Z.coordChange i i' b

Tactic:
ext v

Goal state after:
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
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst✝ : Z.IsContMDiff IB n
i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i') b) v =
    (Z.coordChange i i' b) v
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x x' z : H
⊢ (tangentBundleCore I H).coordChange (achart H x) (achart H x') z = ContinuousLinearMap.id 𝕜 E

Tactic:
ext v

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x x' z : H
v : E
⊢ ((tangentBundleCore I H).coordChange (achart H x) (achart H x') z) v = (ContinuousLinearMap.id 𝕜 E) v
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 𝕜
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✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
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, (contMDiffCoordChange n IB a he he' b) v) = ↑e' { proj := b, snd := e.symm b v }

Tactic:
by
  ext
  · rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]
    rw [e.proj_symm_apply' hb.1]; exact hb.2
  · exact a.contMDiffCoordChange_apply he he' hb v

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 𝕜
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✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this✝ : FiberBundle F E := a.toFiberBundle
this : VectorBundle 𝕜 F E := toVectorBundle a
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
        (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) =
    contMDiffCoordChange n IB a he he' b

Tactic:
ext v

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this✝ : FiberBundle F E := a.toFiberBundle
this : VectorBundle 𝕜 F E := toVectorBundle a
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)
      v =
    (contMDiffCoordChange n IB a he he' b) v
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: case hf
𝕜 : 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
⊢ ContMDiff I.tangent (I.prod 𝓘(𝕜, E)) n ⇑(tangentBundleModelSpaceHomeomorph I)

Tactic:
· exact contMDiff_tangentBundleModelSpaceHomeomorph

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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : TangentSpace I z →L[𝕜] E'
hf : HasMFDerivAt% (-f) z (-f')
⊢ HasMFDerivAt% f z f'

Tactic:
convert! hf.neg <;> rw [neg_neg]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.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
inst✝ : IsManifold I 1 M
x : M
⊢ (tangentBundleCore I M).coordChange (achart H x) (achart H x) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Tactic:
ext v

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
inst✝ : IsManifold I 1 M
x : M
v : E
⊢ ((tangentBundleCore I M).coordChange (achart H x) (achart H x) x) v = (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) v
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
⊢ ⋃ a, ↑a = univ

Tactic:
by rwa [← sUnion_range, Subtype.range_coe]

Goal state after: