mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
⊢ IntegrableOn (fun x ↦ |(F' x).det| • g (f x)) c volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume

Tactic:
apply integrableOn_congr_fun (fun x hx ↦ ?_) hc

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
⊢ |(F' x).det| • g (f x) = f' x • g (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto (fun i ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x✝ : ι
⊢ ∫ (x : α) in φ x✝, f x ∂μ = ∫ (x : α), (φ x✝).indicator f x ∂μ

Tactic:
integral_indicator (hφ.measurableSet _)

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto (fun i ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x✝ : ι
⊢ ∫ (x : α) in φ x✝, f x ∂μ = ∫ (x : α) in φ x✝, f x ∂μ
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
⊢ {x | (fun δ ↦ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0

Tactic:
have L2 :
    ∀ᶠ δ in 𝓝 (0 : ℝ≥0), ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀ := by
    have :
      Tendsto (fun δ => ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
        (𝓝 (‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0)) := by
      rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
      · simpa only [H, zero_mul] using tendsto_const_nhds
      refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id
      refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_
      simpa only [tsub_zero, inv_eq_zero, Ne] using H
    simp only [mul_zero] at this
    exact (tendsto_order.1 this).2 δ₀ δ₀pos

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
⊢ {x | (fun δ ↦ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case hderiv
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε
B : ∀ᶠ (n : ℕ) in atTop, a < ↑n
N : ℕ
hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε
h'N : a < ↑N
x : ℝ
hx : x ≥ ↑N
⊢ ∀ x_1 ∈ [[↑N, x]], HasDerivAt f (f' x_1) x_1

pp: case hint
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε
B : ∀ᶠ (n : ℕ) in atTop, a < ↑n
N : ℕ
hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε
h'N : a < ↑N
x : ℝ
hx : x ≥ ↑N
⊢ IntervalIntegrable f' volume (↑N) x

Tactic:
· intro y hy
        simp only [hx, uIcc_of_le, mem_Icc] at hy
        exact hderiv _ (h'N.trans_le hy.1)

Goal state after:
case hint
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε
B : ∀ᶠ (n : ℕ) in atTop, a < ↑n
N : ℕ
hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε
h'N : a < ↑N
x : ℝ
hx : x ≥ ↑N
⊢ IntervalIntegrable f' volume (↑N) x
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
⊢ ∫ (x : ℝ) in Iic b, deriv f x = f b

Tactic:
have := fun x (_ : x ∈ Iio b) ↦ hf.differentiable one_ne_zero x |>.hasDerivAt

Goal state after:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ ∫ (x : ℝ) in Iic b, deriv f x = f b
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ Tendsto f atTop (𝓝 b')

Tactic:
apply h_infty.congr'

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : ℝ → A := ⋯
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ u * v =ᶠ[atTop] f
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'

Tactic:
← Iic_sdiff_right

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ Tendsto f atBot (𝓝 b')

Tactic:
apply h_infty.congr'

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := ⋯
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ u * v =ᶠ[atBot] f
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Tactic:
have h1 : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K) := by
    filter_upwards [hF] with n h using h.continuousOn.mono hKU
  have h2 : IsCompact (cthickening δ K) := hK.cthickening
  have h3 : TendstoUniformlyOn F f φ (cthickening δ K) :=
    (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).mp hf (cthickening δ K) hKU h2
  apply (h3.cderiv hδ h1).congr
  filter_upwards [hF] with n h z hz
  exact cderiv_eq_deriv hU h hδ ((closedBall_subset_cthickening hz δ).trans hKU)

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

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
S : Set (StructureGroupoid H)
e e' : OpenPartialHomeomorph H H
he : ∀ i ∈ S, e ∈ i.members
he'e : e' ≈ e
⊢ ∀ i ∈ S, e' ∈ i.members

Tactic:
exact fun i hi => i.mem_of_eqOnSource' e e' (he i hi) he'e

Goal state after:
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 y : M
this : Nonempty H
⊢ ↑(chartAt H (Sum.inl x)) (Sum.inl y) = ↑(chartAt H x) y

Tactic:
ChartedSpace.sum_chartAt_inl

Goal state after:
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 y : M
this : Nonempty H
⊢ ↑((chartAt H x).lift_openEmbedding ⋯) (Sum.inl y) = ↑(chartAt H x) y
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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
⊢ e.symm ≫ₕ e' ∈ G

Tactic:
by
  refine G.locality fun x hx ↦ ?_
  set f := chartAt (H := H) (e.symm x)
  let s := e.target ∩ e.symm ⁻¹' f.source
  have hs : IsOpen s := by
    apply e.symm.continuousOn_toFun.isOpen_inter_preimage <;> apply open_source
  have xs : x ∈ s := by
    simp only [s, f, mem_inter_iff, mem_preimage, mem_chart_source, and_true]
    exact ((mem_inter_iff _ _ _).1 hx).1
  refine ⟨s, hs, xs, ?_⟩
  have A : e.symm ≫ₕ f ∈ G := (mem_maximalAtlas_iff.1 he f (chart_mem_atlas _ _)).1
  have B : f.symm ≫ₕ e' ∈ G := (mem_maximalAtlas_iff.1 he' f (chart_mem_atlas _ _)).2
  have C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G := G.trans A B
  have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s := calc
    (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
    _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
      EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _))
    _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
    _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl
    _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]
  exact G.mem_of_eqOnSource C (Setoid.symm D)

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
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst✝] s
ts : t = ↑e' ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
⊢ IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)

Tactic:
simpa [f, inter_comm] using (continuousOn_open_iff (c.open_source e e' he e'_atlas)).1
          (c.continuousOn_toFun e e' he e'_atlas) s s_open

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
conv_rhs => rw [A]

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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∫⁻ (x : E) in ⋃ n, s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case mpr
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
⊢ P f s x → P (↑e' ∘ f) s x

Tactic:
hG.is_local_nhds h2f

Goal state after:
case mpr
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
⊢ P f (s ∩ f ⁻¹' e'.source) x → P (↑e' ∘ f) (s ∩ f ⁻¹' e'.source) x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 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)

pp: 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)

Tactic:
· let : RCLike 𝕜 := h.rclike
    have W := I.convex_range'
    simp only [h, ↓reduceDIte, toPartialEquiv_coe] at W
    simp only [Convex, StarConvex] at W ⊢
    intro u hu v hv a b ha hb hab
    convert! W hu hv ha hb hab using 2
    · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
      rfl
    · rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
      rfl

Goal state after:
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.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
⊢ LiftPropAt Q (↑e.symm) x

Tactic:
suffices h : Q (e ∘ e.symm) univ x by
    have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]
    rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]
    refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩
    simp only [h, mfld_simps]
  exact hG.congr' (e.eventually_right_inverse hx) (hQ x)

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

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hx : ↑I x = y
hy1 : x ∈ u
v : Set H✝
v_open : IsOpen[inst✝¹] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ ↑I.symm ⁻¹' v)
this : ↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I = ↑I.symm ⁻¹' u ∩ range ↑I ∩ ↑I.symm ⁻¹' v
⊢ ↑I x ∈ ↑I.symm ⁻¹' v

Tactic:
by simpa

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
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
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 y

Tactic:
exact mem_interior_iff_mem_nhds.mp ys

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'
n : ℕ∞ω
f : M → M'
x : M
⊢ ContinuousAt f x ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x) ↔
    ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
by rw [ContDiffWithinAtProp, preimage_univ, univ_inter]; rfl

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : 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
n : ℕ
⊢ ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' (s ∩ u n))

Tactic:
apply
        lintegral_abs_det_fderiv_le_addHaar_image_aux2 μ (hs.inter (u_meas n)) _
          (fun x hx => (hf' x hx.1).mono inter_subset_left) (hf.mono inter_subset_left)

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 := ⋯
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
n : ℕ
⊢ μ (s ∩ u n) ≠ ∞
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'
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
he' : e' ∈ maximalAtlas I' n M'
hy : f x ∈ e'.source
⊢ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) ∈ e'.source

Tactic:
by simpa

Goal state after: