mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
a : E
az : a ∈ closedBall z ε
ya : y = x + r • a
⊢ ‖a‖ = ‖z + (a - z)‖

Tactic:
by simp only [add_sub_cancel]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[coclosedCompact ℝ] 0
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

Tactic:
Filter.coclosedCompact_eq_cocompact

Goal state after:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[cocompact ℝ] 0
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ [[a, b]] ⊆ Ici a

Tactic:
uIcc_of_le hb.le

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ Icc a b ⊆ Ici a
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
this : finrank ℝ (E' × ℝ) = n
L₀ : E ≃L[ℝ] E' × ℝ
M : (E' × ℝ) ≃L[ℝ] E' × ℝ
hM : M (L₀ v) = (0, 1)
⊢ (L₀.trans M) v = (0, 1)

Tactic:
simp [hM]

Goal state after:
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: case pos.inr.hf'g
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := ⋯
E' : Type := ⋯
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := ⋯
L_emb : MeasurableEmbedding ⇑L
⊢ Integrable (fun x ↦ (B (f' (L.symm x))) (g (L.symm x))) ν

Tactic:
simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hf'g

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
⊢ IsOpen[inst✝²] {x}

Tactic:
have : IsOpen ((chartAt H x).source ∩ (chartAt H x) ⁻¹' {chartAt H x x}) :=
    isOpen_inter_preimage _ (isOpen_discrete _)

Goal state after:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen[inst✝²] ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ IsOpen[inst✝²] {x}
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x' : M'
⊢ chartAt H (Sum.inr x') = (chartAt H x').lift_openEmbedding ⋯

Tactic:
simp +instances only [chartAt, sum, nonempty_of_chartedSpace x', ↓reduceDIte]
  rfl

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

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e✝ e : PartialEquiv M H
he : e ∈ c.atlas
⊢ ContinuousOn (↑e) e.source

Tactic:
by
      let : TopologicalSpace M := c.toTopologicalSpace
      rw [continuousOn_open_iff (c.open_source' he)]
      intro s s_open
      rw [inter_comm]
      apply TopologicalSpace.GenerateOpen.basic
      simp only [exists_prop, mem_iUnion, mem_singleton_iff]
      exact ⟨e, he, ⟨s, s_open, rfl⟩⟩

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Opens M
hs : Nonempty ↥s
e : OpenPartialHomeomorph (↥s) H
he : e ∈ atlas H ↥s
⊢ ∃ x, e = (chartAt H ↑x).subtypeRestr hs

Tactic:
rcases he with ⟨xset, ⟨x, hx⟩, he⟩

Goal state after:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Opens M
hs : Nonempty ↥s
e : OpenPartialHomeomorph (↥s) H
xset : Set (OpenPartialHomeomorph (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun x ↦ {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ ∃ x, e = (chartAt H ↑x).subtypeRestr hs
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case mp
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P (↑e' ∘ f) (s ∩ ↑e' ∘ f ⁻¹' e'.symm.source) x
h2 : P (↑e'.symm ∘ ↑e' ∘ f) s x
⊢ ↑e'.symm ∘ ↑e' ∘ f =ᶠ[𝓝[s] x] f

Tactic:
exact eventually_of_mem h2f fun x' ↦ e'.left_inv

Goal state after:
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst✝] (f.source ∩ ↑(f.extend I) ⁻¹' s)

Tactic:
rw [← extend_source f (I := I)]; exact isOpen_extend_preimage' f hs

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

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e.symm.symm x) ∧
      P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      P (↑(chartAt H' ((g ∘ ↑e.symm) (↑e x))) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
e.symm_symm

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      P (↑(chartAt H' ((g ∘ ↑e.symm) (↑e x))) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
⊢ LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ LiftPropWithinAt P (↑f ∘ g) s x

Tactic:
liftPropWithinAt_self_target,

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
⊢ LiftPropWithinAt P g s x ↔
    ContinuousWithinAt g s x ∧
      ContinuousWithinAt (↑f ∘ g) s x ∧
        P ((↑f ∘ g) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inr.refine_2.inr
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : μ t ≠ ∞
this : (↑|A.det|.toNNReal - ↑ε) * μ t ≤ μ (g '' t)
⊢ ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t

Tactic:
ENNReal.sub_mul,

Goal state after:
case inr.refine_2.inr
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : μ t ≠ ∞
this : ↑|A.det|.toNNReal * μ t - ↑ε * μ t ≤ μ (g '' t)
⊢ ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t

case inr.refine_2.inr
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : μ t ≠ ∞
this : (↑|A.det|.toNNReal - ↑ε) * μ t ≤ μ (g '' t)
⊢ 0 < ↑ε → ↑ε < ↑|A.det|.toNNReal → μ t ≠ ∞
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ↑(chartAt H' (g' x)) (g' (↑(chartAt H x).symm (↑(chartAt H x) x))) =
    ↑(chartAt H' (g x)) (g (↑(chartAt H x).symm (↑(chartAt H x) x)))

Tactic:
(chartAt H x).left_inv (mem_chart_source H x),

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ↑(chartAt H' (g' x)) (g' x) = ↑(chartAt H' (g x)) (g x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  ContinuousWithinAt g s x ∧
    P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
⊢ s ∈ 𝓝[t] ↑(chartAt H x).symm (↑(chartAt H x) x)

Tactic:
(chartAt H x).left_inv (mem_chart_source H x),

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  ContinuousWithinAt g s x ∧
    P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
⊢ s ∈ 𝓝[t] x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_1
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
⊢ x ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source

Tactic:
simp only [hx, hφ_dom, mfld_simps]

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst✝³] u
xu : x ∈ u
⊢ ContDiffWithinAtProp I I' m f s x ↔ ContDiffWithinAtProp I I' m f (s ∩ u) x

Tactic:
have : I.symm ⁻¹' (s ∩ u) ∩ range I = I.symm ⁻¹' s ∩ range I ∩ I.symm ⁻¹' u := by
      simp only [inter_right_comm, preimage_inter]

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst✝³] u
xu : x ∈ u
this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u
⊢ ContDiffWithinAtProp I I' m f s x ↔ ContDiffWithinAtProp I I' m f (s ∩ u) x
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case e_f
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
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
s_eq : s = ⋃ n, s ∩ t n
i : ℕ
⊢ μ (f '' (s ∩ t i)) + ↑ε * μ (s ∩ t i) + ↑ε * μ (s ∩ t i) = μ (f '' (s ∩ t i)) + 2 * ↑ε * μ (s ∩ t i)

Tactic:
mul_assoc,

Goal state after:
case e_f
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
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
s_eq : s = ⋃ n, s ∩ t n
i : ℕ
⊢ μ (f '' (s ∩ t i)) + ↑ε * μ (s ∩ t i) + ↑ε * μ (s ∩ t i) = μ (f '' (s ∩ t i)) + 2 * (↑ε * μ (s ∩ t i))
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'
f : M → M'
n : ℕ∞ω
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n f x

Tactic:
Subsingleton.elim f fun _ => (f x)

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'
f : M → M'
n : ℕ∞ω
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n (fun x_1 ↦ f x) x
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_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J n (Sum.inr ∘ g)
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
⊢ ContMDiff I J n g

Tactic:
let aux : N ⊕ N' → N' := Sum.elim (fun _ ↦ inhabited_h.default) (@id N')

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_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J n (Sum.inr ∘ g)
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun x ↦ default) id
⊢ ContMDiff I J n g