mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IsManifold.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
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty M
e e' : OpenPartialHomeomorph M H
a✝¹ : e ∈ atlas H M
a✝ : e' ∈ atlas H M
x : E
t : Set E := ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
hx : x ∈ t
⊢ (e.symm ≫ₕ e').source = e.symm.source ∩ ↑e.symm ⁻¹' e'.source

Tactic:
rw [← OpenPartialHomeomorph.trans_source]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.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
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty M
e e' : OpenPartialHomeomorph M H
a✝¹ : e ∈ atlas H M
a✝ : e' ∈ atlas H M
x : E
t : Set E := ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
hx : x ∈ t
this : (e.symm ≫ₕ e').source = ∅
⊢ ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I = ∅ ∩ range ↑I

Tactic:
by rw [this, preimage_empty]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

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'
s : Set M
x : M
n : WithTop ℕ∞
f : M → M'
g : M → N'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt J' (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)
⊢ ContinuousWithinAt (fun x ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt (I'.prod J') (f x, g x)) ∘ (fun x ↦ (f x, g x)) ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
exact ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

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'
F' : Type u_11
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E') (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, F') (g x)) ∘ g ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
⊢ ContinuousWithinAt (fun x ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) ∘ (fun x ↦ (f x, g x)) ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
exact ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) (↑(extChartAt (I.prod J) p) p) =
    (↑(extChartAt (I.prod J) p) p).2

Tactic:
exact (extChartAt J p.2).right_inv <| (extChartAt J p.2).map_source (mem_extChartAt_source _)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Prod

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
⊢ 1 ≤ ‖fst 𝕜 E F‖

Tactic:
have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ ‖fst 𝕜 E F‖ * max ‖e‖ ‖0‖
⊢ 1 ≤ ‖fst 𝕜 E F‖
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 x' : M
y : M'
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
hc : ContinuousWithinAt f s x'
⊢ f ⁻¹' (extChartAt I' y).source ∈ 𝓝[s] x'

Tactic:
exact hc (extChartAt_source_mem_nhds' hy)

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
⊢ MDiffAt f x ↔ ContinuousAt f x ∧ MDiffAt (↑(extChartAt I' (f x)) ∘ f) x

Tactic:
rw [← mdifferentiableWithinAt_univ, ← mdifferentiableWithinAt_univ,
    mdifferentiableWithinAt_iff_target, continuousWithinAt_univ]

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
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x' : M
y : M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
hc : ContinuousWithinAt f s x'
⊢ f ⁻¹' (extChartAt I' y).source ∈ 𝓝[s] x'

Tactic:
exact hc (extChartAt_source_mem_nhds' hy)

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
⊢ tangentMap I I id = id

Tactic:
ext1 ⟨x, v⟩; simp [tangentMap]

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

Goal state before:
pp: case hs
𝕜 : 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'
this : IsManifold I (0 + 1) M
i j k : ↑(atlas H M)
x : M
hxk : x ∈ (↑k).source
hxi : x ∈ (↑i).source
hxj : x ∈ (↑j).source
v : E
⊢ (↑((↑k).extend I) ∘ ↑((↑j).extend I).symm) ∘
      ↑((↑j).extend I) ∘ ↑((↑i).extend I).symm =ᶠ[𝓝[range ↑I] ↑((↑i).extend I) x]
    ↑((↑k).extend I) ∘ ↑((↑i).extend I).symm

Tactic:
have := i.1.extend_preimage_mem_nhds (I := I) hxi (j.1.extend_source_mem_nhds (I := I) hxj)

Goal state after:
case hs
𝕜 : 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'
this✝ : IsManifold I (0 + 1) M
i j k : ↑(atlas H M)
x : M
hxk : x ∈ (↑k).source
hxi : x ∈ (↑i).source
hxj : x ∈ (↑j).source
v : E
this : ↑((↑i).extend I).symm ⁻¹' ((↑j).extend I).source ∈ 𝓝 (↑((↑i).extend I) x)
⊢ (↑((↑k).extend I) ∘ ↑((↑j).extend I).symm) ∘
      ↑((↑j).extend I) ∘ ↑((↑i).extend I).symm =ᶠ[𝓝[range ↑I] ↑((↑i).extend I) x]
    ↑((↑k).extend I) ∘ ↑((↑i).extend I).symm
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'
x₀ : M
y₀ : M'
⊢ (mfderiv% fun x ↦ (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Tactic:
refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_
  rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]

Goal state after:
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
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
⊢ writtenInExtChartAt I I (Sum.inl x) Sum.swap =ᶠ[𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x))] id

Tactic:
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)

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

Tactic:
filter_upwards [hmem] with y 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
hmem : ↑I.symm ⁻¹' (chartAt H q).target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q) q
y : E
hy : y ∈ ↑I.symm ⁻¹' (chartAt H q).target ∩ range ↑I
⊢ writtenInExtChartAt I I q Sum.inl y = id 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
hmem : ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'
⊢ writtenInExtChartAt I I q' Sum.inr =ᶠ[𝓝[range ↑I] ↑(extChartAt I q') q'] id

Tactic:
filter_upwards [hmem] with y 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
hmem : ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'
y : E
hy : y ∈ ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I
⊢ writtenInExtChartAt I I q' Sum.inr y = id 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'
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 : 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'
F₁ : Type u_17
inst✝⁷ : NormedAddCommGroup F₁
inst✝⁶ : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst✝¹ : NormedAddCommGroup F₄
inst✝ : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : TangentSpace I z →L[𝕜] E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, E') ((f + g) z)

Tactic:
by exact mfderiv% f z

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'
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 : 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'
F₁ : Type u_17
inst✝⁷ : NormedAddCommGroup F₁
inst✝⁶ : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst✝¹ : NormedAddCommGroup F₄
inst✝ : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : TangentSpace I z →L[𝕜] E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, E') ((f - g) z)

Tactic:
by exact mfderiv% f z

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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivAt[s] p z p'
hq : HasMFDerivAt[s] q z q'
⊢ HSMul.hSMul (q z) = HSMul.hSMul (MulOpposite.op (q z))

Tactic:
ext _

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
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivAt[s] p z p'
hq : HasMFDerivAt[s] q z q'
x✝¹ : TangentSpace I z →L[𝕜] F'
x✝ : TangentSpace I z
⊢ (q z • x✝¹) x✝ = (MulOpposite.op (q z) • x✝¹) x✝
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
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
⊢ ∃ β t,
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Tactic:
have : ∀ (x : X) (y : Y), ∃ (a : α) (U : Set X) (V : Set Y),
        IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a := fun x y ↦
      (iUnion_eq_univ_iff.1 hu (x, y)).imp fun a ha ↦ isOpen_prod_iff.1 (ho a) x y ha

Goal state after:
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
this : ∀ (x : X) (y : Y), ∃ a U V, IsOpen[inst✝³] U ∧ IsOpen[inst✝²] V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a
⊢ ∃ β t,
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
ι : Type uι
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
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst✝⁵] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst✝⁵] (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∀ (s t : Set M),
    IsClosed[inst✝⁵] s →
      IsClosed[inst✝⁵] t →
        Disjoint s t → ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
intro s t hs ht hd

Goal state after:
case refine_1
ι : Type uι
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
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed[inst✝⁵] s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst✝⁵] (U i)
hU : s✝ ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
hd : Disjoint s t
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1