mathlib-initiative/mathlib-tactics huggingface dataset:
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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
y : M'
hg : MDiffAt g y
hf : MDiffAt[s] f x
hy : f x = y
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
subst hy

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hf : MDiffAt[s] f x
hg : MDiffAt g (f x)
⊢ MDiffAt[s] (g ∘ 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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
y : M'
hg : MDiffAt g y
hf : MDiffAt[s] f x
hy : f x = y
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
by
  subst hy; exact hg.comp_mdifferentiableWithinAt _ hf

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
u : Set M'
x : M
y : M'
hg : MDiffAt[u] g y
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffAt[s] x
hy : f x = y
⊢ mfderiv[s] (g ∘ f) x = mfderiv[u] g y ∘SL mfderiv[s] f x

Tactic:
subst hy

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
u : Set M'
x : M
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffAt[s] x
hg : MDiffAt[u] g (f x)
⊢ mfderiv[s] (g ∘ f) x = mfderiv[u] g (f x) ∘SL mfderiv[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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
y : M'
hg : MDiffAt[u] g y
hf : MDiffAt[s] f x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffAt[s] x
hy : f x = y
⊢ mfderiv[s] (g ∘ f) x = mfderiv[u] g y ∘SL mfderiv[s] f x

Tactic:
subst hy

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hf : MDiffAt[s] f x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffAt[s] x
hg : MDiffAt[u] g (f x)
⊢ mfderiv[s] (g ∘ f) x = mfderiv[u] g (f x) ∘SL mfderiv[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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
x : M
y : M'
hg : MDiffAt g y
hf : MDiffAt[s] f x
hxs : UniqueMDiffAt[s] x
hy : f x = y
⊢ mfderiv[s] (g ∘ f) x = mfderiv% g y ∘SL mfderiv[s] f x

Tactic:
subst hy

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
x : M
hf : MDiffAt[s] f x
hxs : UniqueMDiffAt[s] x
hg : MDiffAt g (f x)
⊢ mfderiv[s] (g ∘ f) x = mfderiv% g (f x) ∘SL mfderiv[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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
x : M
y : M'
hg : MDiffAt g y
hf : MDiffAt f x
hy : f x = y
⊢ mfderiv% (g ∘ f) x = mfderiv% g (f x) ∘SL mfderiv% f x

Tactic:
subst hy

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
x : M
hf : MDiffAt f x
hg : MDiffAt g (f x)
⊢ mfderiv% (g ∘ f) x = mfderiv% g (f x) ∘SL mfderiv% 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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
y : M'
hg : MDiffAt g y
hf : MDiffAt f x
hy : f x = y
v : TangentSpace I x
⊢ (mfderiv% (g ∘ f) x) v = (mfderiv% g y) ((mfderiv% f x) v)

Tactic:
subst hy

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hf : MDiffAt f x
v : TangentSpace I x
hg : MDiffAt g (f x)
⊢ (mfderiv% (g ∘ f) x) v = (mfderiv% g (f x)) ((mfderiv% f x) v)
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' : F
⊢ Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b' = 1

Tactic:
by
  rw [TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, coordChange_model_space]
  apply mem_univ

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✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝¹¹] a
ha' : a ⊆ e.baseSet
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a ↔
    ContMDiffOn IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) a

Tactic:
by
  refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩ <;>
  have := (h x hx).contMDiffAt <| ha.mem_nhds hx
  · exact ((e.contMDiffAt_section_iff (ha' hx)).mp this).contMDiffWithinAt
  · exact ((e.contMDiffAt_section_iff (ha' hx)).mpr this).contMDiffWithinAt

Goal state after:
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
v : E
⊢ ((tangentBundleCore I H).coordChange (achart H x) (achart H x') z) v = (ContinuousLinearMap.id 𝕜 E) v

Tactic:
exact (tangentBundleCore I H).coordChange_self (achart _ z) z (mem_univ _) v

Goal state after:
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
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
p : TangentBundle I H := ⟨↑I.symm 0, 0⟩
⊢ ContinuousOn (↑(chartAt (ModelProd H E) p)) univ

Tactic:
convert! (chartAt (ModelProd H E) p).continuousOn

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
p : TangentBundle I H := ⟨↑I.symm 0, 0⟩
⊢ univ = (chartAt (ModelProd H E) p).source
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 y : M
hy : y ∈ (extChartAt I x).source
⊢ mfderiv% ↑(extChartAt I x) y ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) y))

Tactic:
by
  have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
  convert! mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm ((extChartAt I x).map_source hy)

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
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)
      v =
    (contMDiffCoordChange n IB a he he' b) v

Tactic:
a.contMDiffCoordChange_apply he he' hb 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 =
    (↑e' { proj := b, snd := e.symm b v }).2
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

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
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        ((fun p ↦ (↑(chartAt H x).symm p.1, id p.2)) ((fun p ↦ (↑I.symm p.1, id p.2)) (z, w)))).proj =
    ↑(chartAt H x).symm (↑I.symm z)

Tactic:
apply Trivialization.proj_symm_apply'

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
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ ↑(chartAt H x).symm ((fun p ↦ (↑I.symm p.1, id p.2)) (z, w)).1 ∈ (trivializationAt F Z x).baseSet
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
h : ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, 𝕜 × E) n id
⊢ ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n fun p ↦ p.1 • p.2

Tactic:
exact contDiff_smul.contMDiff.comp h

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
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt (f i) z
⊢ MDiffAt (∏ i ∈ t, f i) z

Tactic:
by
  simp_all only [← mdifferentiableWithinAt_univ]
  exact MDifferentiableWithinAt.prod hf

Goal state after:
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_2
X : Type v
inst✝ : TopologicalSpace X
ι : X → Sort u_1
p : (x : X) → ι x → Prop
s : (x : X) → ι x → Set X
hb : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h :
  ∀ (f : (x : X) → ι x),
    (∀ (x : X), p x (f x)) →
      ∃ β t, (∀ (b : β), IsOpen[inst✝] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ x, t b ⊆ s x (f x)
α : Type v
S : α → Set X
ho : ∀ (a : α), IsOpen[inst✝] (S a)
hu : ⋃ a, S a = univ
a : X → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst✝] (t b)
ht : ⋃ b, t b = univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ x, t b ⊆ s x (f x)
b : β
x : X
hx : t b ⊆ s x (f x)
⊢ ∃ a, ↑⟨t b, ⋯⟩ ⊆ S a

Tactic:
exact ⟨_, hx.trans (hsub _)⟩

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
⊢ ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1

Tactic:
rw [← ρ.sum_eq_one hx₀, finsum_eq_sum_of_support_subset _ (ρ.coe_finsupport x₀).superset]

Goal state after: