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

Goal state before:
pp: H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
⊢ G.IsLocalStructomorphWithinAt (↑f) s x ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source

Tactic:
rw [f.isLocalStructomorphWithinAt_iff hx]

Goal state after:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
⊢ (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source) ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
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_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
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 : M → M'
x : M
n : WithTop ℕ∞
g : N → N'
y : N
hf : ContMDiffAt I I' n f x
hg : ContMDiffAt J J' n g y
⊢ ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)

Tactic:
simp only [← contMDiffWithinAt_univ, ← univ_prod_univ] at *
  exact hf.prodMap hg

Goal state after:
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
n : ℕ∞ω
⊢ ContMDiffWithinAt I I' n f s x ↔
    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)

Tactic:
by
  simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff']; rfl

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
⊢ (Measure.map f ((μ.restrict s).withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) t = (μ.restrict (f '' s)) t

Tactic:
have h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s) := h'f.nullMeasurableSet_preimage ht

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
⊢ (Measure.map f ((μ.restrict s).withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) t = (μ.restrict (f '' s)) t
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: case mk
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : ContMDiffMul I n G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : ContMDiffMul I' n G'
g : ContMDiffMonoidMorphism I I' n G G'
toMonoidHom✝ : G →* G'
contMDiff_toFun✝ : ContMDiff I I' n (↑toMonoidHom✝).toFun
h :
  (fun a ↦ (↑a.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, contMDiff_toFun := contMDiff_toFun✝ } =
    (fun a ↦ (↑a.toMonoidHom).toFun) g
⊢ { toMonoidHom := toMonoidHom✝, contMDiff_toFun := contMDiff_toFun✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : ContMDiffMul I n G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : ContMDiffMul I' n G'
toMonoidHom✝¹ : G →* G'
contMDiff_toFun✝¹ : ContMDiff I I' n (↑toMonoidHom✝¹).toFun
toMonoidHom✝ : G →* G'
contMDiff_toFun✝ : ContMDiff I I' n (↑toMonoidHom✝).toFun
h :
  (fun a ↦ (↑a.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, contMDiff_toFun := contMDiff_toFun✝¹ } =
    (fun a ↦ (↑a.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, contMDiff_toFun := contMDiff_toFun✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, contMDiff_toFun := contMDiff_toFun✝¹ } =
    { toMonoidHom := toMonoidHom✝, contMDiff_toFun := contMDiff_toFun✝ }
Module: Mathlib.Geometry.Manifold.Algebra.Structures

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ (Continuous fun p ↦ p.1 * p.2) ∧
    ∀ (x : 𝕜 × 𝕜) (y : 𝕜),
      ContDiffOn 𝕜 n (↑(extChartAt 𝓘(𝕜, 𝕜) y) ∘ (fun p ↦ p.1 * p.2) ∘ ↑(extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).symm)
        ((extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).target ∩
          ↑(extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).symm ⁻¹' (fun p ↦ p.1 * p.2) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source)

Tactic:
refine ⟨continuous_mul, fun x y => ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 n (↑(extChartAt 𝓘(𝕜, 𝕜) y) ∘ (fun p ↦ p.1 * p.2) ∘ ↑(extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).symm)
    ((extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).target ∩
      ↑(extChartAt (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, 𝕜)) x).symm ⁻¹' (fun p ↦ p.1 * p.2) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source)
Module: Mathlib.Geometry.Manifold.Algebra.Structures

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 n (fun p ↦ p.1 * p.2) Set.univ

Tactic:
contDiffOn_univ

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiff 𝕜 n fun p ↦ p.1 * p.2
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: case a
𝕜 : 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)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen[inst✝⁷] (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ
hu' : ∀ (p : ↑e.source), (↑p).1 ∈ u p
heu : ∀ (p : ↑e.source) (q : B × F), q.1 ∈ u p → q ∈ e.source
p : B × F
hp : p ∈ e.source
⊢ p ∈ (Prod.fst '' e.source) ×ˢ univ

Tactic:
exact ⟨⟨p, hp, rfl⟩, trivial⟩

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
⊢ (if MDiffAt[univ] f x then
      fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I)
        (↑I (↑(chartAt H x) x))
    else 0) =
    if MDiffAt f x then
      fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I)
        (↑I (↑(chartAt H x) x))
    else 0

Tactic:
rw [mdifferentiableWithinAt_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
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[univ ∩ s] f x f'
hs : s ∈ 𝓝 x
⊢ HasMFDerivAt% f x f'

Tactic:
hasMFDerivWithinAt_inter hs,

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 : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[univ] f x f'
hs : s ∈ 𝓝 x
⊢ HasMFDerivAt% f x f'
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case fst
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ b ∈ e'.baseSet

Tactic:
exact hb.2

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

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
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)
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x) ↔
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
apply hasFDerivWithinAt_congr_set' (extChartAt I x x)

Goal state after:
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
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)
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝[≠] ↑(extChartAt I x) x] ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case fst
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ e'.baseSet

Tactic:
exact hb.2

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'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffAt[s] x
⊢ mfderiv% Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
exact mfderiv_fst

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

Goal state before:
pp: case fst
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ e'.baseSet

Tactic:
exact hb.2

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
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst✝²] s
hs : s ⊆ support ↑f
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑e '' s)
⊢ ∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r

Tactic:
rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs

Goal state after:
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
hsc : IsClosed[inst✝²] s
hs : s ⊆ (chartAt H c).source ∧ ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑e '' s)
⊢ ∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
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✝ : 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
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj : x ∈ v.toFun j
⊢ x ∈ update v.toFun i vi j

Tactic:
rwa [update_of_ne hji]

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: case mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f g : PartitionOfUnity ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), (toFun✝ i) x ≤ 1
h :
  { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
        sum_le_one' := sum_le_one'✝ }.toFun =
    g.toFun
⊢ { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
      sum_le_one' := sum_le_one'✝ } =
    g

Tactic:
cases g

Goal state after:
case mk.mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i ↦ support ⇑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
sum_eq_one'✝¹ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝¹ i) x = 1
sum_le_one'✝¹ : ∀ (x : X), ∑ᶠ (i : ι), (toFun✝¹ i) x ≤ 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), (toFun✝ i) x ≤ 1
h :
  { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, sum_eq_one' := sum_eq_one'✝¹,
        sum_le_one' := sum_le_one'✝¹ }.toFun =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
        sum_le_one' := sum_le_one'✝ }.toFun
⊢ { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, sum_eq_one' := sum_eq_one'✝¹,
      sum_le_one' := sum_le_one'✝¹ } =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
      sum_le_one' := sum_le_one'✝ }
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy : {i | y ∈ closure[inst✝] (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure[inst✝] (support ⇑(ρ i))}
z : ι
hz : y ∈ tsupport ⇑(ρ z)
⊢ x₀ ∈ tsupport ⇑(ρ z)

Tactic:
exact hy hz

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: case mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f g : BumpCovering ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ x ∈ s, ∃ i, ⇑(toFun✝ i) =ᶠ[𝓝 x] 1
h :
  { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
        eventuallyEq_one' := eventuallyEq_one'✝ }.toFun =
    g.toFun
⊢ { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
      eventuallyEq_one' := eventuallyEq_one'✝ } =
    g

Tactic:
cases g

Goal state after:
case mk.mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i ↦ support ⇑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
le_one'✝¹ : toFun✝¹ ≤ 1
eventuallyEq_one'✝¹ : ∀ x ∈ s, ∃ i, ⇑(toFun✝¹ i) =ᶠ[𝓝 x] 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ x ∈ s, ∃ i, ⇑(toFun✝ i) =ᶠ[𝓝 x] 1
h :
  { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, le_one' := le_one'✝¹,
        eventuallyEq_one' := eventuallyEq_one'✝¹ }.toFun =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
        eventuallyEq_one' := eventuallyEq_one'✝ }.toFun
⊢ { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, le_one' := le_one'✝¹,
      eventuallyEq_one' := eventuallyEq_one'✝¹ } =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
      eventuallyEq_one' := eventuallyEq_one'✝ }
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 := ⋯
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
j : ι
hji : j ≠ i
hj : x ∈ v.toFun j
⊢ x ∈ update v.toFun i vi j

Tactic:
rwa [update_of_ne hji]

Goal state after: