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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
⊢ ↑(extChartAt I x₀) x ∈ o → (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
ho

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : ↑(extChartAt I x₀) x ∈ o
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
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'
x x' : M
n : ℕ∞ω
inst✝ : IsManifold I n M
hx' : x' ∈ (chartAt H x).source
⊢ ContMDiffAt I I' n f x' ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')

Tactic:
by
  simp_rw [ContMDiffAt, contMDiffWithinAt_iff_source_of_mem_source hx', preimage_univ, univ_inter]

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

Goal state before:
pp: case some
𝕜 : 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 : ℕ
h : ∀ (m : ℕ), ↑m ≤ some n → ContMDiffWithinAt I I' (↑m) f s x
⊢ ContMDiffWithinAt I I' (↑(some n)) f s x

Tactic:
exact h n le_rfl

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, E).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n fun p ↦ p.1 + p.2

Tactic:
← modelWithCornersSelf_prod,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiff 𝓘(𝕜, E × E) 𝓘(𝕜, E) n fun p ↦ p.1 + p.2
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

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

Tactic:
rw [hΦφ ⟨x, hx⟩ y hy]

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

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

Tactic:
rw [hΦφ ⟨x, hx⟩ y hy]

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

Goal state before:
pp: 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✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
y : E b
⊢ (Pretrivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
by
  rw [coe_linearMapAt]

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

Goal state before:
pp: 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 : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
y : E b
⊢ (Trivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
by
  rw [coe_linearMapAt]

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'
x : M × M'
⊢ HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I x Prod.fst)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I'))
    (↑(extChartAt (I.prod I') x) x)

Tactic:
have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I x.1 ∘ Prod.fst ∘ (extChartAt (I.prod I') x).symm) y = y.1 := by
    /- porting note: was
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
    mfld_set_tac
    -/
    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
    rw [extChartAt_prod] at hy
    exact (extChartAt I x.1).right_inv hy.1

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'
x : M × M'
this :
  ∀ᶠ (y : E × E') in 𝓝[range ↑(I.prod I')] ↑(extChartAt (I.prod I') x) x,
    (↑(extChartAt I x.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod I') x).symm) y = y.1
⊢ HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I x Prod.fst)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I'))
    (↑(extChartAt (I.prod I') x) x)
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
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
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
x₀ : M
⊢ ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔
    ContMDiffAt IM IB n (fun x ↦ (f x).proj) x₀ ∧
      ContMDiffAt IM 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Tactic:
by
  simp_rw [← contMDiffWithinAt_univ]; exact contMDiffWithinAt_totalSpace

Goal state after:
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:
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.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₀).prod (mfderiv% id y₀) = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Tactic:
rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
x : E
hx : x ∈ ((↑i).extend I).symm.source ∩ ↑((↑i).extend I).symm ⁻¹' (((↑i).extend I).symm.target ∩ ((↑j).extend I).source)
⊢ fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) (↑((↑i).extend I).symm x)) =
    fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x

Tactic:
(i.1.extend I).right_inv hx.1

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ContDiffOn 𝕜 n ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm)
    (↑((↑i).extend I) '' ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j))

Tactic:
refine ((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_
    · rw [PartialEquiv.trans_source'] at hx
      simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]
    · exact (i.1.extend_image_source_inter j.1).subset

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_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiff[s]
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
⊢ UniqueMDiff[s ∩ f ⁻¹' (extChartAt I' y).source]

Tactic:
intro z hz
    apply (hs z hz.1).inter'
    apply (hf z hz.1).preimage_mem_nhdsWithin
    exact (isOpen_extChartAt_source y).mem_nhds hz.2

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

Goal state before:
pp: case refine_2
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ⋃ i, (fun i ↦ ⋃ a, ⋃ (_ : ind a = i), t a) i = univ

Tactic:
simp only [eq_univ_iff_forall, mem_iUnion]
    exact fun x ↦ ⟨ind (t_inv x), _, rfl, ht_inv _⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀

Tactic:
classical
  induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using! contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
k : ℕ
ih : ⇑(k • s) = k • ⇑s
⊢ ⇑((k + 1) • s) = (k + 1) • ⇑s

Tactic:
simp_rw [succ_nsmul, ← ih]

Goal state after:
case succ
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
k : ℕ
ih : ⇑(k • s) = k • ⇑s
⊢ ⇑((k + 1) • s) = ⇑(k • s) + ⇑s
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case pos
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✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x c : M
Hx : x ∈ tsupport ⇑(f c)
hx : x ∈ ↑(chartAt H c) ⁻¹' (chartAt H c).target ∩ ↑(chartAt H c) ⁻¹' ↑(chartAt H c).symm ⁻¹' s
⊢ x ∈ s

Tactic:
simp only [mem_inter_iff, mem_preimage, (chartAt H c).left_inv (hf c Hx)] at hx

Goal state after:
case pos
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✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x c : M
Hx : x ∈ tsupport ⇑(f c)
hx : ↑(chartAt H c) x ∈ (chartAt H c).target ∧ x ∈ s
⊢ x ∈ s
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: 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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
c x : M
hx : x ∈ tsupport ⇑(f c)
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) (↑n) (fun x ↦ g c (↑(chartAt H c) x)) x

Tactic:
apply (g_diff c (chartAt H c x)).comp

Goal state after:
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
c x : M
hx : x ∈ tsupport ⇑(f c)
⊢ ContMDiffAt I I (↑n) (↑(chartAt H c)) x
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
⊢ f =ᵐ[μ] g

Tactic:
by
  rw [← sub_ae_eq_zero]
  have hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs),
      sub_eq_zero.mpr (hfg_eq s hs hμs)]
  have hfg_int : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn (f - g) s μ := fun s hs hμs =>
    (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
  exact (hf.sub hg).ae_eq_zero_of_forall_setIntegral_eq_zero hfg_int hfg

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

Goal state before:
pp: E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
⊢ f =ᵐ[μ] 0

Tactic:
by
  rw [← μ.restrict_univ, ← iUnion_closure_compactCovering]
  apply (ae_restrict_iUnion_iff _ _).2 (fun n ↦ ?_)
  apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero
  · exact hf.integrableOn_isCompact (isCompact_compactCovering β n).closure
  · intro s hs
    rw [Measure.restrict_restrict' measurableSet_closure]
    exact h'f _ (hs.inter_right isClosed_closure)

Goal state after: