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

Goal state before:
pp: case left
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
h3 :
  ContDiffOn 𝕜 n (Prod.map (↑I ∘ ↑e ∘ ↑I.symm) (↑I' ∘ ↑e' ∘ ↑I'.symm))
    ((fun p ↦ (↑I p.1, ↑I' p.2)) '' e.source ×ˢ e'.source)
⊢ ContDiffOn 𝕜 n (↑(I.prod I') ∘ ↑(e.prod e') ∘ ↑(I.prod I').symm)
    (↑(I.prod I').symm ⁻¹' (e.prod e'.toPartialEquiv).source ∩ range ↑(I.prod I'))

Tactic:
← (I.prod I').image_eq

Goal state after:
case left
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
h3 :
  ContDiffOn 𝕜 n (Prod.map (↑I ∘ ↑e ∘ ↑I.symm) (↑I' ∘ ↑e' ∘ ↑I'.symm))
    ((fun p ↦ (↑I p.1, ↑I' p.2)) '' e.source ×ˢ e'.source)
⊢ ContDiffOn 𝕜 n (↑(I.prod I') ∘ ↑(e.prod e') ∘ ↑(I.prod I').symm) (↑(I.prod I') '' (e.prod e'.toPartialEquiv).source)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case right
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
h3 :
  ContDiffOn 𝕜 n (Prod.map (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I' ∘ ↑e'.symm ∘ ↑I'.symm))
    ((fun p ↦ (↑I p.1, ↑I' p.2)) '' e.target ×ˢ e'.target)
⊢ ContDiffOn 𝕜 n (↑(I.prod I') ∘ ↑(e.prod e').symm ∘ ↑(I.prod I').symm)
    (↑(I.prod I').symm ⁻¹' (e.prod e'.toPartialEquiv).target ∩ range ↑(I.prod I'))

Tactic:
← (I.prod I').image_eq

Goal state after:
case right
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
h3 :
  ContDiffOn 𝕜 n (Prod.map (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I' ∘ ↑e'.symm ∘ ↑I'.symm))
    ((fun p ↦ (↑I p.1, ↑I' p.2)) '' e.target ×ˢ e'.target)
⊢ ContDiffOn 𝕜 n (↑(I.prod I') ∘ ↑(e.prod e').symm ∘ ↑(I.prod I').symm)
    (↑(I.prod I') '' (e.prod e'.toPartialEquiv).target)
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✝
𝕜 : Type u_5
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_6
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type u_7
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H : Type u_8
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_9
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_10
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I n M
M' : Type u_11
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' n M'
f1 : OpenPartialHomeomorph M H
hf1 : f1 ∈ atlas H M
f2 : OpenPartialHomeomorph M' H'
hf2 : f2 ∈ atlas H' M'
g1 : OpenPartialHomeomorph M H
hg1 : g1 ∈ atlas H M
g2 : OpenPartialHomeomorph M' H'
hg2 : g2 ∈ atlas H' M'
h1 : f1.symm ≫ₕ g1 ∈ contDiffGroupoid n I
⊢ (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')

Tactic:
have h2 := (contDiffGroupoid n I').compatible hf2 hg2

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✝
n : ℕ∞ω
M✝ : Type u_4
inst✝¹⁴ : TopologicalSpace M✝
inst✝¹³ : ChartedSpace H✝ M✝
𝕜 : Type u_5
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_6
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type u_7
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H : Type u_8
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_9
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_10
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I n M
M' : Type u_11
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' n M'
f1 : OpenPartialHomeomorph M H
hf1 : f1 ∈ atlas H M
f2 : OpenPartialHomeomorph M' H'
hf2 : f2 ∈ atlas H' M'
g1 : OpenPartialHomeomorph M H
hg1 : g1 ∈ atlas H M
g2 : OpenPartialHomeomorph M' H'
hg2 : g2 ∈ atlas H' M'
h1 : f1.symm ≫ₕ g1 ∈ contDiffGroupoid n I
h2 : f2.symm ≫ₕ g2 ∈ contDiffGroupoid n I'
⊢ (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')
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 : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
| μ (f '' s)

Tactic:
rw [A, image_iUnion]

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 : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
| μ (⋃ i, f '' (s ∩ u i))
Module: Mathlib.Analysis.Normed.Operator.Prod

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ ‖snd 𝕜 E F‖ * ‖f‖
⊢ 1 ≤ ‖snd 𝕜 E F‖

Tactic:
rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul]

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.LieGroup

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
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
inst✝ : IsTopologicalGroup G
⊢ LieGroup I 0 G

Tactic:
constructor
  rw [contMDiff_zero_iff]
  exact continuous_inv

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 : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffWithinAt I I' n f s x ↔ ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'

Tactic:
refine ⟨?_, fun h ↦ mem_of_mem_nhdsWithin (mem_insert x s) 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
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 : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffWithinAt I I' n f s x → ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s

Tactic:
have hc' : ContMDiffOn I I n c'.symm _ := contMDiffOn_chart_symm

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
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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
hc' : ContMDiffOn I I n (↑c'.symm) (chartAt H (↑f x)).target
⊢ ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: case mp
𝕜 : 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 : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source X

Tactic:
let c' := chartAt H X

Goal state after:
case mp
𝕜 : 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 : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source X
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, (a.coordChange he he' b) v).1 = (↑e' { proj := b, snd := e.symm b v }).1

pp: case snd
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, (a.coordChange he he' b) v).2 = (↑e' { proj := b, snd := e.symm b v }).2

Tactic:
· rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]
    rw [e.proj_symm_apply' hb.1]
    exact hb.2

Goal state after:
case snd
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, (a.coordChange he he' b) v).2 = (↑e' { proj := b, snd := e.symm b v }).2
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁹ : (x : B) → AddCommMonoid (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜₁
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst✝¹³ : TopologicalSpace B'
inst✝¹² : NormedSpace 𝕜₁ F
inst✝¹¹ : (x : B) → Module 𝕜₁ (E x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
F' : Type u_8
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst✝⁷ : (x : B') → AddCommMonoid (E' x)
inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)
inst✝⁵ : TopologicalSpace (TotalSpace F' E')
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜₁ F E
inst✝² : (x : B') → TopologicalSpace (E' x)
inst✝¹ : FiberBundle F' E'
inst✝ : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : E x →SL[σ] E' y
hx : x ∈ (trivializationAt F E x₀).baseSet
hy : y ∈ (trivializationAt F' E' y₀).baseSet
⊢ inCoordinates F E F' E' x₀ x y₀ y ϕ =
    ↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy) ∘SL
      ϕ ∘SL ↑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm

Tactic:
by
  ext
  simp_rw [inCoordinates, ContinuousLinearMap.coe_comp, ContinuousLinearEquiv.coe_coe,
    Trivialization.coe_continuousLinearEquivAt_eq, Trivialization.symm_continuousLinearEquivAt_eq]

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 𝕜
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✝⁵ : 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
x : B × F
hx : x ∈ e.target
⊢ (↑e (↑e.symm x)).2 = x.2

Tactic:
e.apply_symm_apply hx

Goal state after:
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✝⁵ : 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
x : B × F
hx : x ∈ e.target
⊢ x.2 = x.2
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: case hg
𝕜 : Type u_1
inst✝²⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²³ : NormedAddCommGroup E'
inst✝²² : NormedSpace 𝕜 E'
F : Type u_4
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹⁹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁸ : TopologicalSpace H'
G : Type u_7
inst✝¹⁷ : TopologicalSpace G
G' : Type u_8
inst✝¹⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J✝¹ : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : ChartedSpace H M
M'✝ : Type u_10
inst✝¹³ : TopologicalSpace M'✝
inst✝¹² : ChartedSpace H' M'✝
N✝ : Type u_11
inst✝¹¹ : TopologicalSpace N✝
inst✝¹⁰ : ChartedSpace G N✝
N'✝ : Type u_12
inst✝⁹ : TopologicalSpace N'✝
inst✝⁸ : ChartedSpace G' N'✝
n : ℕ∞ω
M' : Type u_13
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H M'
M'' : Type u_14
inst✝⁵ : TopologicalSpace M''
inst✝⁴ : ChartedSpace H M''
N : Type u_15
J✝ : Type u_16
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace H N'
⊢ ContMDiff I I n (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)

Tactic:
· exact ContMDiff.inr.sumMap contMDiff_id

Goal state after:
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
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen[inst✝²] (s a)
hu : ⋃ a, s a = univ
T : Finset ι
hT : univ ⊆ ⋃ i ∈ T, s i
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Tactic:
refine ⟨(T : Set ι), fun t ↦ s t, fun t ↦ ho _, ?_, locallyFinite_of_finite _,
    fun t ↦ ⟨t, Subset.rfl⟩⟩

Goal state after:
ι✝ : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen[inst✝²] (s a)
hu : ⋃ a, s a = univ
T : Finset ι
hT : univ ⊆ ⋃ i ∈ T, s i
⊢ ⋃ b, (fun t ↦ s ↑t) b = univ
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ¬∃ v ∈ c, i ∈ v.carrier
⊢ i ∈ ne.some.carrier ↔ i ∈ chainSupCarrier c

Tactic:
push Not at h
    refine iff_of_false (h _ ne.some_mem) ?_
    simpa only [chainSupCarrier, mem_iUnion₂, not_exists]

Goal state after:
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_3
X : Type v
inst✝³ : TopologicalSpace X
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed[inst✝³] s
hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := K'.shiftr.shiftr
Kdiff : ℕ → Set X := fun n ↦ K (n + 1) \ interior (K n)
hKcov : ∀ (x : X), x ∈ Kdiff (K'.find x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT : ∀ (n : ℕ), Kdiff (n + 1) ∩ s ⊆ ⋃ x ∈ T n, B (↑x) (r n ⟨↑x, ⋯⟩)
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ ↑(T n)
x✝ : X
this : (⋃ k, ⋃ (_ : k ≤ K'.find x✝ + 2), range (Sigma.mk k)).Finite
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
x : X
hxB : x ∈ B (↑c) (r k c)
hxK : x ∈ interior (K (K'.find x✝ + 3))
hnk : K'.find x✝ + 2 < k
⊢ x ∈ K k

Tactic:
exact K.subset hnk (interior_subset hxK)

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
⊢ ∃ t, f.toPOUFun i =ᶠ[𝓝 x] ⇑(f i) * ⇑(∏ j ∈ t with WellOrderingRel j i, (1 - f j))

Tactic:
rcases f.locallyFinite x with ⟨U, hU, hf⟩

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : {i | ((fun i ↦ support ⇑(f i)) i ∩ U).Nonempty}.Finite
⊢ ∃ t, f.toPOUFun i =ᶠ[𝓝 x] ⇑(f i) * ⇑(∏ j ∈ t with WellOrderingRel j i, (1 - f j))