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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.extend I).target

Tactic:
rw [extend_target, I.range_eq_univ, inter_univ]
  exact I.continuous_symm.isOpen_preimage _ f.open_target

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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : Convex ℝ s
⊢ Convex ℝ s

Tactic:
let := h.rclike
  let := NormedSpace.restrictScalars ℝ 𝕜 E
  simp only [Convex, StarConvex] at hs ⊢
  intro u hu v hv a b ha hb hab
  convert! hs hu hv ha hb hab using 2
  · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]
  · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]

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
inst✝ : NormedSpace ℝ E
⊢ Convex ℝ (range ↑I)

Tactic:
by_cases h : IsRCLikeNormedField 𝕜

Goal state after:
case pos
𝕜 : 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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (range ↑I)

case neg
𝕜 : 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
inst✝ : NormedSpace ℝ E
h : ¬IsRCLikeNormedField 𝕜
⊢ Convex ℝ (range ↑I)
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
⊢ UniqueDiffOn 𝕜 (range ↑I)

Tactic:
by_cases h : IsRCLikeNormedField 𝕜

Goal state after:
case pos
𝕜 : 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
h : IsRCLikeNormedField 𝕜
⊢ UniqueDiffOn 𝕜 (range ↑I)

case neg
𝕜 : 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
h : ¬IsRCLikeNormedField 𝕜
⊢ UniqueDiffOn 𝕜 (range ↑I)
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
⊢ range ↑I ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))

Tactic:
by_cases h : IsRCLikeNormedField 𝕜

Goal state after:
case pos
𝕜 : 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
h : IsRCLikeNormedField 𝕜
⊢ range ↑I ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))

case neg
𝕜 : 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
h : ¬IsRCLikeNormedField 𝕜
⊢ range ↑I ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case pos.hs'
𝕜 : 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
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ (interior (range ↑I)).Nonempty

Tactic:
apply I.nonempty_interior

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case refine_1.hf
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ.symm) φ.target (↑φ x)

Tactic:
exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case refine_2.hg
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ.symm) φ.target (↑φ x)

Tactic:
exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn

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

Goal state before:
pp: H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : OpenPartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : OpenPartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : OpenPartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f')) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
⊢ ∃ s, IsOpen[inst✝⁷] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Tactic:
have hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source :=
        (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source

Goal state after:
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : OpenPartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : OpenPartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : OpenPartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f')) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst✝⁷] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ ∃ s, IsOpen[inst✝⁷] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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✝² : ChartedSpace H' M'
inst✝¹ : T2Space M
inst✝ : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x✝ : M
x : ↥U
h : ↑x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContMDiffAt I I' n (extend Subtype.val f 1 ∘ Subtype.val) x

Tactic:
extend_comp Subtype.val_injective

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
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✝² : ChartedSpace H' M'
inst✝¹ : T2Space M
inst✝ : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x✝ : M
x : ↥U
h : ↑x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContMDiffAt I I' n f x
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: case hf
𝕜 : 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
h : ContinuousOn f s
x : M
y : M'
⊢ ContinuousOn (f ∘ ↑(extChartAt I x).symm)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
apply h.comp ((continuousOn_extChartAt_symm _).mono inter_subset_left) (fun z hz ↦ ?_)

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
h : ContinuousOn f s
x : M
y : M'
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)
⊢ ↑(extChartAt I x).symm z ∈ s
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: case pos.hs
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ ↑(extChartAt I' (f₁ x)) ∘
      f₁ ∘ ↑(extChartAt I x).symm =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    ↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm

Tactic:
filter_upwards [extChartAt_preimage_mem_nhdsWithin (I := I) hL] 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
y : E
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' {x | f₁ x = f x}
⊢ (↑(extChartAt I' (f₁ x)) ∘ f₁ ∘ ↑(extChartAt I x).symm) y = (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) y
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
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'
h : IsManifold I 2 M
⊢ ContMDiffVectorBundle 1 E (TangentSpace I) I

Tactic:
have : IsManifold I (1 + 1) M := h

Goal state after:
𝕜 : 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'
h : IsManifold I 2 M
this : IsManifold I (1 + 1) M
⊢ ContMDiffVectorBundle 1 E (TangentSpace I) I
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (i : ι), (f i) x ≤ 0
⊢ ∑ᶠ (i : ι), (f i) x ≠ 1

Tactic:
simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ↑(ρ.finsupport x₀) = support fun i ↦ (ρ i) x₀

Tactic:
by
  ext
  rw [Finset.mem_coe, mem_finsupport]

Goal state after:
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
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier
h : ¬j = i
⊢ IsCompact (closure (update v.toFun i vi j))

Tactic:
· apply hj.elim
      · intro hji
        exact False.elim (h hji)
      · intro hjmemv
        rw [update_of_ne h]
        exact v.pred_of_mem hjmemv

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
⊢ ∃ v,
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))

Tactic:
have : ∀ c : Set (PartialRefinement u s (fun w => IsCompact (closure w))),
      IsChain (· ≤ ·) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub :=
    fun c hc ne => ⟨.chainSup c hc ne uf us, fun v hv => PartialRefinement.le_chainSup _ _ _ _ hv⟩

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
⊢ ∃ v,
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
obtain ⟨u, u_op, hsu, hut⟩ := normal_exists_closure_subset hs ht.isOpen_compl
    (subset_compl_iff_disjoint_left.mpr hd.symm)

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
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hut : closure[inst✝⁶] u ⊆ tᶜ
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
hd : s ⊆ interior t
⊢ s ⊆ (interior ?m.105)ᶜᶜ

Tactic:
compl_compl

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
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
hd : s ⊆ interior t
⊢ s ⊆ interior ?m.105
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝ : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν

Tactic:
obtain ⟨T, hT⟩ : ∃ T : Submodule 𝕜 E, IsCompl S T := Submodule.exists_isCompl S

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝ : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, c (f x) ∂μ = 0

Tactic:
ContinuousLinearMap.integral_comp_comm c (hf_int_finite s hs hμs),

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ c (∫ (x : α) in s, f x ∂μ) = 0
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f f' : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x

Tactic:
by
  have : ∀ᵐ x ∂μ, (f - f') x = 0 := by
    apply ae_eq_zero_of_integral_contMDiff_smul_eq_zero I (hf.sub hf')
    intro g g_diff g_supp
    simp only [Pi.sub_apply, smul_sub]
    rw [integral_sub, sub_eq_zero]
    · exact h g g_diff g_supp
    · exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
    · exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
  filter_upwards [this] with x hx
  simpa [sub_eq_zero] using hx

Goal state after: