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

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
this✝ : ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0
this : ∫⁻ (x : ℝ) in b, ENNReal.ofReal (f' x) * u (f x) = 0
⊢ 0 + ∫⁻ (a : ℝ) in c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
zero_add

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
this✝ : ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0
this : ∫⁻ (x : ℝ) in b, ENNReal.ofReal (f' x) * u (f x) = 0
⊢ ∫⁻ (a : ℝ) in c, ENNReal.ofReal (f' a) * u (f a) ∂volume = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
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
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
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
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
this : ∫ (x : ℝ) in a, f' x • g (f x) = 0
⊢ 0 + ∫ (x : ℝ) in b ∪ c, f' x • g (f x) ∂volume = ∫ (x : ℝ) in c, f' x • g (f x)

Tactic:
zero_add

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
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
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
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
this : ∫ (x : ℝ) in a, f' x • g (f x) = 0
⊢ ∫ (x : ℝ) in b ∪ c, f' x • g (f x) ∂volume = ∫ (x : ℝ) in c, f' x • g (f x)
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
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
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
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
this✝ : ∫ (x : ℝ) in a, f' x • g (f x) = 0
this : ∫ (x : ℝ) in b, f' x • g (f x) = 0
⊢ 0 + ∫ (x : ℝ) in c, f' x • g (f x) ∂volume = ∫ (x : ℝ) in c, f' x • g (f x)

Tactic:
zero_add

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
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
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
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
this✝ : ∫ (x : ℝ) in a, f' x • g (f x) = 0
this : ∫ (x : ℝ) in b, f' x • g (f x) = 0
⊢ ∫ (x : ℝ) in c, f' x • g (f x) ∂volume = ∫ (x : ℝ) in c, f' x • g (f x)
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, 1 + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)

Tactic:
gcongr with x hx

Goal state after:
case h
p : ℝ[X]
x : ℝ
hx : x ∈ (derivative p).roots.toFinset \ p.roots.toFinset
⊢ 1 ≤ Multiset.count x (derivative p).roots
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, rootMultiplicity x (derivative p) +
      (((derivative p).roots.toFinset \ p.roots.toFinset).card + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)

Tactic:
simp only [← count_roots, Finset.card_eq_sum_ones]
      gcongr with x hx
      rw [Nat.succ_le_iff, Multiset.count_pos, ← Multiset.mem_toFinset]
      exact (Finset.mem_sdiff.1 hx).1

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1) =
    (derivative p).roots.card + 1

Tactic:
by
      rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
        Multiset.toFinset_sum_count_eq, ← Finset.sum_subset Finset.subset_union_right]
      intro x _ hx₂
      simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
c : ℝ
hc : 0 ≤ c
this : 0 ≤ c ^ p⁻¹
⊢ ∫ (x : ℝ) in Ioi (c ^ p⁻¹), (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi c, g y

Tactic:
have : Ioi c = (· ^ p) '' Ioi (c ^ p⁻¹) := by
    rw [(continuous_rpow_const hp.le).continuousOn.image_Ioi_of_strictMonoOn
          ((strictMonoOn_rpow_Ici_of_exponent_pos hp).mono (by grind)) (tendsto_rpow_atTop hp)]
    simp [← rpow_mul hc, hp.ne.symm]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
c : ℝ
hc : 0 ≤ c
this✝ : 0 ≤ c ^ p⁻¹
this : Ioi c = (fun x ↦ x ^ p) '' Ioi (c ^ p⁻¹)
⊢ ∫ (x : ℝ) in Ioi (c ^ p⁻¹), (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi c, g y
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
a b : StructureGroupoid H
h : a.members = b.members
⊢ a = b

Tactic:
by
    cases a
    cases b
    dsimp at h
    induction h
    rfl

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

Goal state before:
pp: case inr
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
x : H
hx : x ∈ e.source
⊢ e ∈ {OpenPartialHomeomorph.refl H}

Tactic:
rcases he x hx with ⟨s, open_s, xs, hs⟩

Goal state after:
case inr
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst✝] s
xs : x ∈ s
hs : e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
⊢ e ∈ {OpenPartialHomeomorph.refl H}
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
U : Opens M
x : ↥U
⊢ ↑(chartAt H ↑x).symm =ᶠ[𝓝 (↑(chartAt H ↑x) ↑x)] Subtype.val ∘ ↑(chartAt H x).symm

Tactic:
by
  set e := chartAt H x.val
  have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn ⟨x⟩)

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

Goal state before:
pp: case left
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
he' : e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑(e ≫ₕ e')) (e ≫ₕ e').source

pp: case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
he' : e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑(e ≫ₕ e').symm) (e ≫ₕ e').target

Tactic:
· apply PG.comp he.1 he'.1 e.open_source e'.open_source
      apply e.continuousOn_toFun.isOpen_inter_preimage e.open_source e'.open_source

Goal state after:
case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
he' : e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑(e ≫ₕ e').symm) (e ≫ₕ e').target
Module: Mathlib.Geometry.Manifold.HasGroupoid

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
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : c ∈ atlas H M'
hc' : c' ∈ atlas H M
this : (c'.symm ≫ₕ e.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
trans_symm_eq_symm_trans_symm,

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : c ∈ atlas H M'
hc' : c' ∈ atlas H M
this : (e.toOpenPartialHomeomorph ≫ₕ c).symm ≫ₕ c'.symm.symm ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
Module: Mathlib.Geometry.Manifold.HasGroupoid

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
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : c ∈ atlas H M'
hc' : c' ∈ atlas H M
this : (e.toOpenPartialHomeomorph ≫ₕ c).symm ≫ₕ c'.symm.symm ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
trans_symm_eq_symm_trans_symm,

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : c ∈ atlas H M'
hc' : c' ∈ atlas H M
this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c'.symm.symm ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
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
h : Q (↑e ∘ ↑e.symm) univ x
⊢ LiftPropAt Q (↑e.symm) x

Tactic:
have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]

Goal state after:
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
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ LiftPropAt Q (↑e.symm) x
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)
⊢ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)

Tactic:
apply contDiffOn_of_locally_contDiffOn

Goal state after:
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)
⊢ ∀ x ∈ ↑I.symm ⁻¹' u ∩ range ↑I,
    ∃ u_1,
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
        x ∈ u_1 ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ u_1)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
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
g : E → F
⊢ IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun x ↦ |(f' x).det| • g (f x)) s μ

Tactic:
by
  rw [IntegrableOn, ← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
    (measurableEmbedding_of_fderivWithin hs hf' hf).integrable_map_iff]
  simp only [Set.domRestrict_eq, ← Function.comp_assoc, ENNReal.ofReal]
  rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs,
    restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀]
  · simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply]
  · exact aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf'

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
⊢ MDifferentiableWithinAt I I' f s x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)

Tactic:
rw [MDifferentiableWithinAt, liftPropWithinAt_iff']; rfl

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source
hex : ↑c x ∈ e.source
⊢ ↑c' X = ↑c' (↑f (↑c.symm (↑c x)))

Tactic:
have hfX : f.symm X ∈ c.source := by simp only [c, x, mfld_simps]

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source
hex : ↑c x ∈ e.source
hfX : ↑f.symm X ∈ c.source
⊢ ↑c' X = ↑c' (↑f (↑c.symm (↑c x)))
Module: Mathlib.Geometry.Manifold.MFDeriv.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
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
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
⊢ MDiffAt[s] f x ↔ ContinuousWithinAt f s x ∧ MDiffAt[s] (↑(extChartAt I' y) ∘ f) x

Tactic:
simp_rw [MDifferentiableWithinAt]
  rw [differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart_target
      (chart_mem_maximalAtlas y) hy, and_congr_right]
  intro hf
  simp_rw [StructureGroupoid.liftPropWithinAt_self_target]
  simp_rw [((chartAt H' y).continuousAt hy).comp_continuousWithinAt hf]
  rw [← extChartAt_source I'] at hy
  simp_rw [(continuousAt_extChartAt' hy).comp_continuousWithinAt hf]
  rfl

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

Goal state before:
pp: case pos
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] (TotalSpace.mk b ∘ e.symm b)

Tactic:
exact e.continuousOn_symm.comp_continuous (.prodMk_right _) fun x ↦
          mk_mem_prod hb (mem_univ x)

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
⊢ (fun b ↦ ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b)) b =
    (fun x ↦ (↑(coordChangeL 𝕜 e₁ e₁' x)).prodMap ↑(coordChangeL 𝕜 e₂ e₂' x)) b

Tactic:
rw [ContinuousLinearMap.ext_iff]

Goal state after:
case refine_3
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
⊢ ∀ (x : F₁ × F₂),
    ((fun b ↦ ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b)) b) x =
      ((fun x ↦ (↑(coordChangeL 𝕜 e₁ e₁' x)).prodMap ↑(coordChangeL 𝕜 e₂ e₂' x)) b) x