mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen[inst✝⁷] (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q ↦ (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
hU' : IsOpen[inst✝⁷] U
Φ₀ : ↑U → F ≃L[𝕜] F := iUnionLift u (fun x ↦ φ x ∘ Subtype.val) huφ U ⋯
Φ : B → F ≃L[𝕜] F := fun y ↦ if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
hΦ✝ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩
hΦφ : ∀ (x : ↑U), ∀ y ∈ u x, Φ y = φ x y
hΦ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y ↦ ↑(Φ y)) U
h2Φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y ↦ ↑(Φ y).symm) U
p : B × F
hp : p ∈ e.source
⊢ ↑e p = ↑(FiberwiseLinear.openPartialHomeomorph Φ hU' ⋯ ⋯) p

Tactic:
hU

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen[inst✝⁷] (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q ↦ (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
hU' : IsOpen[inst✝⁷] U
Φ₀ : ↑U → F ≃L[𝕜] F := iUnionLift u (fun x ↦ φ x ∘ Subtype.val) huφ U ⋯
Φ : B → F ≃L[𝕜] F := fun y ↦ if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
hΦ✝ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩
hΦφ : ∀ (x : ↑U), ∀ y ∈ u x, Φ y = φ x y
hΦ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y ↦ ↑(Φ y)) U
h2Φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y ↦ ↑(Φ y).symm) U
p : B × F
hp : p ∈ U ×ˢ univ
⊢ ↑e p = ↑(FiberwiseLinear.openPartialHomeomorph Φ hU' ⋯ ⋯) p
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt f (s ∩ t) x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' t) (↑(extChartAt I x) x) ↔
    ContinuousWithinAt f s x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)

Tactic:
hasFDerivWithinAt_inter',

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)
h : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt f (s ∩ t) x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x) ↔
    ContinuousWithinAt f s x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)

𝕜 : 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)
h : t ∈ 𝓝[s] x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ OpenPartialHomeomorph.refl (B × F) ∈
    ⋃ φ,
      ⋃ U,
        ⋃ (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),
              {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)}

Tactic:
mem_aux

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∃ φ U,
    ∃ (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),
      (OpenPartialHomeomorph.refl (B × F)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ ↑(extChartAt I x).symm z ∈ s ↔ ↑(extChartAt I x).symm z ∈ t

Tactic:
rw [← eq_iff_iff]

Goal state after:
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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ (↑(extChartAt I x).symm z ∈ s) = (↑(extChartAt I x).symm z ∈ t)
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case refine_1
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
this : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)
⊢ (fun y ↦ e.coordChange e' (f y) (g y)) =ᶠ[𝓝[s] x] fun x ↦ ↑(Trivialization.coordChangeL 𝕜 e e' (f x)) (g x)

Tactic:
filter_upwards [hf.continuousWithinAt this] with y hy

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
this : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)
y : M
hy : y ∈ f ⁻¹' (e.baseSet ∩ e'.baseSet)
⊢ e.coordChange e' (f y) (g y) = ↑(Trivialization.coordChangeL 𝕜 e e' (f y)) (g y)
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'
p : M × M'
f : M → N
g : M' → N'
hf : MDiffAt f p.1
hg : MDiffAt g p.2
⊢ mfderiv[univ ×ˢ univ] (Prod.map f g) p = (mfderiv[univ] f p.1).prodMap (mfderiv[univ] g p.2)

Tactic:
exact mfderivWithin_prodMap hf.mdifferentiableWithinAt hg.mdifferentiableWithinAt
    (uniqueMDiffWithinAt_univ I) (uniqueMDiffWithinAt_univ I')

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
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
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
f : M → TotalSpace F E
s : Set M
he : MapsTo f s e.source
⊢ ContMDiffOn IM (IB.prod 𝓘(𝕜, F)) n f s ↔
    ContMDiffOn IM IB n (fun x ↦ (f x).proj) s ∧ ContMDiffOn IM 𝓘(𝕜, F) n (fun x ↦ (↑e (f x)).2) s

Tactic:
simp only [ContMDiffOn, ← forall_and]

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
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
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
f : M → TotalSpace F E
s : Set M
he : MapsTo f s e.source
⊢ (∀ x ∈ s, ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x) ↔
    ∀ x ∈ s,
      ContMDiffWithinAt IM IB n (fun x ↦ (f x).proj) s x ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x ↦ (↑e (f x)).2) s x
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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

Tactic:
let t := I.symm ⁻¹' (chartAt H x).target ∩ range I
      have : EqOn (writtenInExtChartAt I I (Sum.inl x) (@Sum.swap M M')) id t := by
        intro y hy
        simp only [writtenInExtChartAt, extChartAt, Sum.swap_inl,
          ChartedSpace.sum_chartAt_inl, ChartedSpace.sum_chartAt_inr]
        dsimp
        rw [Sum.inr_injective.extend_apply, (chartAt H x).right_inv (by grind)]
        exact I.right_inv (by grind)
      apply Filter.eventually_of_mem ?_ this
      rw [Filter.inter_mem_iff]
      refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩
      exact (chartAt H x).open_target.mem_nhds (by simp)

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
⊢ ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'

Tactic:
rw [← I.image_eq (chartAt H q').target]

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'
q' : M'
⊢ ↑I '' (chartAt H q').target ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'
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
p : TotalSpace F Z
hs : UniqueMDiffAt[s] p.proj
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
⊢ UniqueMDiffAt[TotalSpace.proj ⁻¹' s] p

Tactic:
by
  suffices ((extChartAt I p.proj).symm ⁻¹' s ∩ range I) ×ˢ univ ⊆
      (extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' (TotalSpace.proj ⁻¹' s) ∩ range (I.prod 𝓘(𝕜, F)) by
    let w := (extChartAt (I.prod 𝓘(𝕜, F)) p p).2
    have A : extChartAt (I.prod 𝓘(𝕜, F)) p p = (extChartAt I p.1 p.1, w) := by
      ext
      · simp [FiberBundle.chartedSpace_chartAt]
      · rfl
    simp only [UniqueMDiffWithinAt, A] at hs ⊢
    exact (hs.prod (uniqueDiffWithinAt_univ (x := w))).mono this
  rcases p with ⟨x, v⟩
  dsimp
  rintro ⟨z, w⟩ ⟨hz, -⟩
  simp only [mem_inter_iff, mem_preimage, Function.comp_apply,
    mem_range] at hz
  simp only [FiberBundle.chartedSpace_chartAt, OpenPartialHomeomorph.coe_trans_symm, mem_inter_iff,
    mem_preimage, Function.comp_apply, mem_range]
  constructor
  · rw [PartialEquiv.prod_symm, PartialEquiv.refl_symm, PartialEquiv.prod_coe,
      ModelWithCorners.toPartialEquiv_coe_symm, PartialEquiv.refl_coe,
      OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.refl_symm,
      OpenPartialHomeomorph.prod_apply, OpenPartialHomeomorph.refl_apply]
    convert! hz.1
    apply Trivialization.proj_symm_apply'
    exact h's hz.1
  · rcases hz.2 with ⟨u, rfl⟩
    exact ⟨(u, w), rfl⟩

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

Goal state before:
pp: case h₁.refine_2
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ (extChartAt I c).target ∩ ↑(extChartAt I c).symm ⁻¹' s ⊆ ↑(extChartAt I c).symm ⁻¹' s

Tactic:
exact inter_subset_right

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
s t : (x : M) → V x
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) x₀
ht : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (s + t) x⟩) x₀

Tactic:
rw [← contMDiffWithinAt_univ] at hs ⊢
  exact hs.add_section ht

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
⊢ Injective ContMDiffSection.toFun

Tactic:
rintro ⟨⟩ ⟨⟩ h

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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
toFun✝¹ : (x : M) → V x
contMDiff_toFun✝¹ : ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x ↦ ⟨x, toFun✝¹ x⟩
toFun✝ : (x : M) → V x
contMDiff_toFun✝ : ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x ↦ ⟨x, toFun✝ x⟩
h :
  { toFun := toFun✝¹, contMDiff_toFun := contMDiff_toFun✝¹ }.toFun =
    { toFun := toFun✝, contMDiff_toFun := contMDiff_toFun✝ }.toFun
⊢ { toFun := toFun✝¹, contMDiff_toFun := contMDiff_toFun✝¹ } = { toFun := toFun✝, contMDiff_toFun := contMDiff_toFun✝ }
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: case convert_4
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i ↦ f.toPOUFun i x) ⊆ ↑s
B : (mulSupport fun i ↦ 1 - (f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝¹ : i ∈ s
j : ι
x✝ : WellOrderingRel j i
hj : (f j) x ≠ 0
⊢ j ∈ s

Tactic:
rwa [Finite.mem_toFinset]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
t_meas : MeasurableSet t
t_lt_top : μ t < ∞
s : Set α
s_meas : MeasurableSet s
a✝ : μ (s ∩ t) < ∞
⊢ 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ

Tactic:
exact
    hf_zero _ (s_meas.inter t_meas)
      (lt_of_le_of_lt (measure_mono (Set.inter_subset_right)) t_lt_top)

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst✝²] s → ∫ (x : β) in s, f x ∂μ = 0
A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0 → ∫ (x : β) in tᶜ, f x ∂μ = 0
⊢ ∀ (s : Set β), MeasurableSet s → ∫ (x : β) in s, f x ∂μ = 0

Tactic:
intro s hs

Goal state after:
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst✝²] s → ∫ (x : β) in s, f x ∂μ = 0
A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0 → ∫ (x : β) in tᶜ, f x ∂μ = 0
s : Set β
hs : MeasurableSet s
⊢ ∫ (x : β) in s, f x ∂μ = 0