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

Goal state before:
pp: case mpr.refine_2.convert_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
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H✝ M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H✝ := chartAt H✝ x
c' : OpenPartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy :
  (↑I.symm y ∈ c'.target ∧ ↑c'.symm (↑I.symm y) ∈ f.target ∧ ↑f.symm (↑c'.symm (↑I.symm y)) ∈ c.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f.symm) (f.symm ≫ₕ c).source (↑(extChartAt I (↑f x)).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑f.symm ∘ ↑(extChartAt I (↑f x)).symm)
      (↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I)
      (↑(extChartAt I (↑f x)) (↑(extChartAt I (↑f x)).symm y))
hy' : ↑(extChartAt I (↑f x)).symm y ∈ c'.source
hy'' : ↑f.symm (↑(extChartAt I (↑f x)).symm y) ∈ c.source
⊢ ↑I.symm ⁻¹' (chartAt H✝ (↑f x)).target ∩
        (↑I.symm ⁻¹' ↑(chartAt H✝ (↑f x)).symm ⁻¹' f.target ∩
          ↑I.symm ⁻¹' ↑(chartAt H✝ (↑f x)).symm ⁻¹' ↑f.symm ⁻¹' (chartAt H✝ x).source) ∩
      range ↑I ⊆
    ↑(chartAt H✝ (↑f x)).symm ∘ ↑I.symm ⁻¹' f.target ∩
        ↑(chartAt H✝ (↑f x)).symm ∘ ↑I.symm ⁻¹' ↑f.symm ⁻¹' (chartAt H✝ x).source ∩
      range ↑I

Tactic:
mfld_set_tac

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

Goal state before:
pp: case mp.convert_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'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
h : MDiffAt[s] f w
this : w ∈ s
w1 : w ∈ (chartAt H x).source
w2 : f w ∈ (chartAt H' y).source
⊢ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
    ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I

Tactic:
mfld_set_tac

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

Goal state before:
pp: case e'_12
𝕜 : 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
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ ↑I.symm ⁻¹' (chartAt H x).target ∩
        (↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ ↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' f ⁻¹' (chartAt H' (f x)).source) ∩
      range ↑I =
    (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
mfld_set_tac

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'
f : M → M'
x : M
s : Set M
n : WithTop ℕ∞
hf : ContMDiffWithinAt I I' n f s x
hn : n ≠ 0
⊢ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I ⊆
    ↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ range ↑I

Tactic:
mfld_set_tac

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'
x : M
s : Set M
g : M' → M''
h : ContinuousWithinAt f s x
⊢ f ∘ ↑(extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source ⊆
    {x_1 |
      (fun x_2 ↦
          writtenInExtChartAt I I'' x (g ∘ f) x_2 =
            (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
        x_1}

Tactic:
mfld_set_tac

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁.baseSet ∩ e₁'.baseSet

Tactic:
mfld_set_tac

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet

Tactic:
mfld_set_tac

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
x : M
⊢ (extChartAt I x).target ⊆ {x_1 | (fun y ↦ (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y) x_1}

Tactic:
mfld_set_tac

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'
f f₁ : M → M'
s : Set M
h : ∀ x ∈ s, f x = f₁ x
p : TangentBundle I M
hp : p.proj ∈ s
⊢ tangentMapWithin I I' f s p = tangentMapWithin I I' f₁ s p

Tactic:
refine TotalSpace.ext (h p.1 hp) ?_
  rw [tangentMapWithin, h p.1 hp, tangentMapWithin, mfderivWithin_congr h (h _ hp)]

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
inst✝ : Subsingleton F
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) univ x

Tactic:
apply contMDiffWithinAt_section_of_subsingleton

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'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle I' M'
x₀ : M
⊢ tangentMap I' (I.prod I') (fun y ↦ (x₀, y)) p = ⟨(x₀, p.proj), (0, p.snd)⟩

Tactic:
simp only [tangentMap, mfderiv_prod_right]

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'
p : TangentBundle I' M'
x₀ : M
⊢ ⟨(x₀, p.proj), (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' p.proj)) p.snd⟩ =
    ⟨(x₀, p.proj), (0, p.snd)⟩
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
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 : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this✝¹ : mfderiv% (↑e.symm ∘ ↑e) x = mfderiv% ↑e.symm (↑e x) ∘SL mfderiv% ↑e x
this✝ : mfderiv% id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
this : e.source ∈ 𝓝 x
⊢ e.source ⊆ {x | (fun x ↦ (↑e.symm ∘ ↑e) x = id x) x}

Tactic:
mfld_set_tac

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

Goal state before:
pp: case e_a
𝕜 : 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' → M''
p : M × M'
hf : MDiffAt f p
⊢ (mfderiv% fun z ↦ f (p.1, z.2)) p = (mfderiv% fun z ↦ f (p.1, z)) p.2 ∘SL id (ContinuousLinearMap.snd 𝕜 E E')

Tactic:
have : (fun z : M × M' ↦ f (p.1, z.2)) = (fun z : M' ↦ f (p.1, z)) ∘ Prod.snd := rfl

Goal state after:
case e_a
𝕜 : 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' → M''
p : M × M'
hf : MDiffAt f p
this : (fun z ↦ f (p.1, z.2)) = (fun z ↦ f (p.1, z)) ∘ Prod.snd
⊢ (mfderiv% fun z ↦ f (p.1, z.2)) p = (mfderiv% fun z ↦ f (p.1, z)) p.2 ∘SL id (ContinuousLinearMap.snd 𝕜 E E')
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case refine_1
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝³⁸ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝³⁷ : NormedAddCommGroup EB
inst✝³⁶ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³⁵ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝³⁴ : TopologicalSpace B
inst✝³³ : ChartedSpace HB B
EM : Type u_9
inst✝³² : NormedAddCommGroup EM
inst✝³¹ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝³⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝²⁹ : TopologicalSpace M
inst✝²⁸ : ChartedSpace HM M
inst✝²⁷ : (x : B) → AddCommMonoid (E x)
inst✝²⁶ : (x : B) → Module 𝕜 (E x)
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
inst✝²³ : TopologicalSpace (TotalSpace F E)
inst✝²² : (x : B) → TopologicalSpace (E x)
inst✝²¹ : FiberBundle F E
inst✝²⁰ : VectorBundle 𝕜 F E
inst✝¹⁹ : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹⁵ : (x : B) → AddCommMonoid (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
F₂ : Type u_13
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁰ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁸ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : VectorBundle 𝕜 F₂ E₂
inst✝² : ContMDiffVectorBundle n F₁ E₁ IB
inst✝¹ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝ : IsManifold IB n B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
i₁ : MemTrivializationAtlas e₁
i₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
i₁' : MemTrivializationAtlas e₁'
i₂' : MemTrivializationAtlas e₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁.baseSet ∩ e₁'.baseSet

Tactic:
mfld_set_tac

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

Goal state before:
pp: case refine_2
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
F₁ : Type u_11
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹⁵ : (x : B) → AddCommMonoid (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
F₂ : Type u_13
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁰ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁸ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : VectorBundle 𝕜 F₂ E₂
inst✝² : ContMDiffVectorBundle n F₁ E₁ IB
inst✝¹ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝ : IsManifold IB n B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
i₁ : MemTrivializationAtlas e₁
i₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
i₁' : MemTrivializationAtlas e₁'
i₂' : MemTrivializationAtlas e₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet

Tactic:
mfld_set_tac

Goal state after:
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
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'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivAt[s] f x f'
hd : DenseRange ⇑f'
this : UniqueMDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] x
⊢ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I ⊆
    ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I

Tactic:
mfld_set_tac

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

Goal state before:
pp: 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
⊢ (𝓝[range ↑I] ↑(extChartAt I c) c).HasBasis (fun x ↦ True) fun f ↦ closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I

Tactic:
refine ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset
    (extChartAt_target_mem_nhdsWithin _)).to_hasBasis' ?_ ?_

Goal state after:
case refine_1
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
⊢ ∀ (i : ℝ),
    0 < i ∧ closedBall (↑(extChartAt I c) c) i ∩ range ↑I ⊆ (extChartAt I c).target →
      ∃ i', True ∧ closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ⊆ closedBall (↑(extChartAt I c) c) i ∩ range ↑I

case 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
⊢ ∀ (i' : SmoothBumpFunction I c),
    True → closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I c) c
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
⊢ ParacompactSpace X

Tactic:
by
  -- the proof is trivial: we choose a finite subcover using compactness, and use it
  refine ⟨fun ι s ho hu ↦ ?_⟩
  rcases isCompact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩
  refine ⟨(T : Set ι), fun t ↦ s t, fun t ↦ ho _, ?_, locallyFinite_of_finite _,
    fun t ↦ ⟨t, Subset.rfl⟩⟩
  simpa only [iUnion_coe_set, ← univ_subset_iff]

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → x ∉ v.toFun j
⊢ x ∈ s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ

Tactic:
exact ⟨hx, mem_iInter₂_of_mem h⟩

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

Goal state before:
pp: 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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
n : ℕ∞
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate fun x ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity
x : M
hx : x ∈ s
i : ι
⊢ ↑(f.toFun i) x = 0

Tactic:
exact notMem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : ↑d
hx : dist a ↑x < ‖a‖ / 2
I : ‖a‖ / 2 < ‖↑x‖
h : (s x) a = 0
⊢ ‖↑x‖ = ‖(s x) ↑x‖

Tactic:
simp [(hs x).2]

Goal state after: