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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m✝ n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
this✝ : IsManifold I (↑m) M
this : IsManifold I' (↑m) M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' (↑m) f t
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m) f (insert x s ∩ u)

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩

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 : Set M
x : M
m✝ n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
this✝ : IsManifold I (↑m) M
this : IsManifold I' (↑m) M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' (↑m) f t
u : Set M
u_open : IsOpen[inst✝⁸] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ t
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m) f (insert x s ∩ u)
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : ω = ∞ → n = ω
this✝ : IsManifold I ω M
this : IsManifold I' ω M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' ω f t
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩

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 : Set M
x : M
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : ω = ∞ → n = ω
this✝ : IsManifold I ω M
this : IsManifold I' ω M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' ω f t
u : Set M
u_open : IsOpen[inst✝⁸] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ t
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : ∞ = ∞ → n = ω
this✝ : IsManifold I ∞ M
this : IsManifold I' ∞ M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' n f t
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩

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 : Set M
x : M
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : ∞ = ∞ → n = ω
this✝ : IsManifold I ∞ M
this : IsManifold I' ∞ M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' n f t
u : Set M
u_open : IsOpen[inst✝⁸] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ t
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContMDiffWithinAt I I' n f s x
this✝ : IsManifold I m M
this : IsManifold I' m M'
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u)

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

Goal state after:
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : f x.1 ∈ e.baseSet
⊢ (x.1, (↑e { proj := f x.1, snd := e.symm (f x.1) x.2 }).2) = x

Tactic:
e.apply_mk_symm h

Goal state after:
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 : M → M'
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : ¬MDiffAt[s] f x
⊢ mfderiv[s] f x = mfderiv[t] f x

Tactic:
simp [mfderivWithin, hx, ← mdifferentiableWithinAt_congr_set' y h]

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:
simp_rw [contMDiffAt_totalSpace, and_iff_right_iff_imp]; intro; exact contMDiffAt_id

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
f : M → F₁ × F₂
⊢ MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x

Tactic:
by
  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
  exact mdifferentiableAt_prod_iff f

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
f : M → F₁ × F₂
⊢ MDiff[s] f ↔ MDiff[s] (Prod.fst ∘ f) ∧ MDiff[s] (Prod.snd ∘ f)

Tactic:
exact mdifferentiableOn_prod_iff f

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
x : TotalSpace F E
this : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n TotalSpace.proj 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
x : TotalSpace F E
this :
  ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (fun x ↦ (id x).proj) x ∧
    ContMDiffAt (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) n (fun x_1 ↦ (↑(trivializationAt F E (id x).proj) (id x_1)).2) x
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n TotalSpace.proj 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'
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))
hg : HasMFDerivAt[u] g (f x) g'
hf : HasMFDerivAt[s] f x f'
hst : s ⊆ f ⁻¹' u
A :
  HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g' ∘SL f')
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
⊢ HasFDerivWithinAt (writtenInExtChartAt I I'' x (g ∘ f)) (g' ∘SL f') (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
    (↑(extChartAt I x) x)

Tactic:
apply A.congr_of_eventuallyEq (writtenInExtChartAt_comp hf.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'
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'
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))
hg : HasMFDerivAt[u] g (f x) g'
hf : HasMFDerivAt[s] f x f'
hst : s ⊆ f ⁻¹' u
A :
  HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g' ∘SL f')
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
⊢ writtenInExtChartAt I I'' x (g ∘ f) (↑(extChartAt I x) x) =
    (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (↑(extChartAt I x) 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 × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
⊢ ↑((chartAt H p.1).prod (chartAt H' p.2).toPartialEquiv).symm ∘ ↑(I.prod I'.toPartialEquiv).symm ⁻¹' s ∩
      range (Prod.map ↑I ↑I') ⊆
    (↑(chartAt H p.1).symm ∘ ↑I.symm ⁻¹' Prod.fst '' s ∩ range ↑I) ×ˢ
      (↑(chartAt H' p.2).symm ∘ ↑I'.symm ⁻¹' Prod.snd '' s ∩ range ↑I')

Tactic:
range_prodMap,

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 : 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 × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
⊢ ↑((chartAt H p.1).prod (chartAt H' p.2).toPartialEquiv).symm ∘ ↑(I.prod I'.toPartialEquiv).symm ⁻¹' s ∩
      range ↑I ×ˢ range ↑I' ⊆
    (↑(chartAt H p.1).symm ∘ ↑I.symm ⁻¹' Prod.fst '' s ∩ range ↑I) ×ˢ
      (↑(chartAt H' p.2).symm ∘ ↑I'.symm ⁻¹' Prod.snd '' s ∩ range ↑I')
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)
⊢ (tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j ⊆ (↑i).source

Tactic:
apply inter_subset_left

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

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
⊢ writtenInExtChartAt I I (Sum.inr x) Sum.swap =ᶠ[𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))] id

Tactic:
have : EqOn (writtenInExtChartAt I I (Sum.inr x) (@Sum.swap M M')) id t := by
        intro y hy
        simp only [writtenInExtChartAt, extChartAt, Sum.swap_inr,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]
        dsimp
        rw [Sum.inl_injective.extend_apply, (chartAt H x).right_inv (by grind)]
        exact I.right_inv (by grind)

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : EqOn (writtenInExtChartAt I I (Sum.inr x) Sum.swap) id t
⊢ writtenInExtChartAt I I (Sum.inr x) Sum.swap =ᶠ[𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))] id
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'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] (-f) z
⊢ MDiffAt[s] f z

Tactic:
by convert hf.neg; rw [neg_neg]

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_2
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ s ⊆ ⋃ i_1, update v.toFun i vi i_1

Tactic:
refine fun x hx => mem_iUnion.2 ?_
    by_cases! h : ∃ j ≠ i, x ∈ v j
    · rcases h with ⟨j, hji, hj⟩
      use j
      rwa [update_of_ne hji]
    · use i
      rw [update_self]
      exact hvi ⟨hx, mem_biInter h⟩

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

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
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀

Tactic:
by
  simp_rw [← contMDiffWithinAt_univ] at hs ⊢
  exact .sum_section hs

Goal state after:
Module: Mathlib.Analysis.Convex.PartitionOfUnity

Goal state before:
pp: X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate fun x ↦ interior (U x)
x i : X
hi : (f i) x ≠ 0
⊢ x ∈ U i

Tactic:
exact interior_subset (hf _ <| subset_closure hi)

Goal state after:
Module: Mathlib.Analysis.Convex.PartitionOfUnity

Goal state before:
pp: X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
H : ∀ (x : X), ∃ U ∈ 𝓝 x, ∃ g, ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ g, ∀ (x : X), g x ∈ t x

Tactic:
choose U hU g hgc hgt using H
  obtain ⟨f, hf⟩ := PartitionOfUnity.exists_isSubordinate isClosed_univ (fun x => interior (U x))
    (fun x => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
  refine ⟨⟨fun x => ∑ᶠ i, f i x • g i x,
    hf.continuous_finsum_smul (fun i => isOpen_interior) fun i => (hgc i).mono interior_subset⟩,
    fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ ?_) (ht _)⟩
  exact interior_subset (hf _ <| subset_closure hi)

Goal state after: