mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: case refine_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x | (fun i ↦ f i x) = fun i ↦ f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 : ((LinearEquiv.piRing ℝ ℝ ι ℝ).symm Λ, Λ₀) ≠ 0
hsum : ∀ (x : E), ((LinearEquiv.piRing ℝ ℝ ι ℝ).symm Λ) ((ContinuousLinearMap.pi f') x) + Λ₀ • φ' x = 0
⊢ (Λ, Λ₀) ≠ 0

Tactic:
simpa only [Ne, Prod.ext_iff, LinearEquiv.map_eq_zero_iff, Prod.fst_zero] using! h0

Goal state after:
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
A : f '' a ∪ (f '' b ∪ f '' c) =ᵐ[volume] f '' b ∪ f '' c
B : f '' b ∪ f '' c =ᵐ[volume] f '' c
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᵐ[volume] f '' c

Tactic:
exact A.trans B

Goal state after:
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
A : f '' a ∪ (f '' b ∪ f '' c) =ᵐ[volume] f '' b ∪ f '' c
B : f '' b ∪ f '' c =ᵐ[volume] f '' c
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᵐ[volume] f '' c

Tactic:
exact A.trans B

Goal state after:
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) atBot l
⊢ Tendsto (fun x ↦ f x / g x) atBot l

Tactic:
by
  have hdg : ∀ᶠ x in atBot, DifferentiableAt ℝ g x :=
    hg'.mono fun _ hg' => by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h)
  have hdf' : ∀ᶠ x in atBot, HasDerivAt f (deriv f x) x :=
    hdf.mono fun _ => DifferentiableAt.hasDerivAt
  have hdg' : ∀ᶠ x in atBot, HasDerivAt g (deriv g x) x :=
    hdg.mono fun _ => DifferentiableAt.hasDerivAt
  exact HasDerivAt.lhopital_zero_atBot hdf' hdg' hg' hfbot hgbot hdiv

Goal state after:
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
I : ∫ (x : ℝ) in s, f' x • g (f x) = ∫ (x : ℝ) in c, f' x • g (f x)
A : f '' a ∪ (f '' b ∪ f '' c) =ᵐ[volume] f '' b ∪ f '' c
B : f '' b ∪ f '' c =ᵐ[volume] f '' c
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᵐ[volume] f '' c

Tactic:
exact A.trans B

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f f' : ℝ → ℝ
g g' : ℝ → E
inst✝ : CompleteSpace E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a

Tactic:
rw [integral_deriv_smul_comp'' hf hff' hf' hg',
    integral_eq_sub_of_hasDeriv_right hg hgg' (hg'.mono _).intervalIntegrable]
  exacts [rfl, intermediate_value_uIcc hf]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ Icc (f b) (f a) =ᵐ[volume] f '' Ioo a b

Tactic:
rw [← hf.image_Icc_of_antitoneOn hab M]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ f '' Icc a b =ᵐ[volume] f '' Ioo a b
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‖}
⊢ ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε

Tactic:
have B₂ : ∀ᶠ r in 𝓝[>] (0 : ℝ), {x} + r • closedBall z ε ⊆ ball x ρ := by
    apply nhdsWithin_le_nhds
    exact eventually_singleton_add_smul_subset isBounded_closedBall (ball_mem_nhds x ρpos)

Goal state after:
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 ρ
⊢ ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
⊢ Tendsto f atBot (𝓝 0)

Tactic:
have A : Tendsto (F ∘ f) atBot (𝓝 (limUnder atBot (F ∘ f))) := by
    apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic Fderiv F'int

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (atBot.limUnder (⇑F ∘ f)))
⊢ Tendsto f atBot (𝓝 0)
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
hf : DifferentiableOn ℝ f s
hs : μ s = 0
A : E →L[ℝ] E
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t

Tactic:
let m : ℝ≥0 := Real.toNNReal |A.det| + 1

Goal state after:
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
hf : DifferentiableOn ℝ f s
hs : μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + 1
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
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
x : ℝ
hx : x < a
⊢ (u * v) x = f x

Tactic:
exact (Function.update_of_ne (ne_of_lt hx) a' (u * v)).symm

Goal state after:
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'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
⊢ ∃ s, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
let f₁ := e.toHomeomorph.toOpenPartialHomeomorph

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'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
⊢ ∃ s, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
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
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ ↑(f.extend I).symm ⁻¹' t ∈ 𝓝 (↑(f.extend I) x)

Tactic:
apply (continuousAt_extend_symm f h).preimage_mem_nhds
  rwa [(f.extend I).left_inv]
  rwa [f.extend_source]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv))
  else range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv) = univ

Tactic:
PartialEquiv.pi_apply,

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (Pi.map fun i ↦ ↑(I i).toPartialEquiv))
  else range (Pi.map fun i ↦ ↑(I i).toPartialEquiv) = univ
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ (interior (range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv))).Nonempty

Tactic:
PartialEquiv.pi_apply,

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ (interior (range (Pi.map fun i ↦ ↑(I i).toPartialEquiv))).Nonempty
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
inst✝ : ChartedSpace H M
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝[range ↑I] y ⊔ 𝓝[(range ↑I)ᶜ] y

Tactic:
exact Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin_of_mem hy) self_mem_nhdsWithin

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

Goal state before:
pp: case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩

Goal state after:
case mp.refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ (e.restr f.source).source ⊆ f.source

case mp.refine_2
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ EqOn (↑f) (↑(e.restr f.source)) (s ∩ (e.restr f.source).source)

case mp.refine_3
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ x ∈ interior f.source
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
⊢ (↑(extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty

Tactic:
by
    have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
      apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
    refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)
    apply (isOpen_extChartAt_source x₀).mem_nhds h'x

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

Goal state before:
pp: H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
x✝¹ : x ∈ s
e : OpenPartialHomeomorph H H
x✝ : e ∈ G
h2e : e.source ⊆ f.source
⊢ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source ↔ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source

Tactic:
inter_eq_right.mpr (h2e.trans hs)

Goal state after:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
x✝¹ : x ∈ s
e : OpenPartialHomeomorph H H
x✝ : e ∈ G
h2e : e.source ⊆ f.source
⊢ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source ↔ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case h
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 : ℕ
⊢ MeasurableSet (f '' (s ∩ t i))

Tactic:
exact
          measurable_image_of_fderivWithin (hs.inter (t_meas i))
            (fun x hx => (hf' x hx.1).mono inter_subset_left)
            (hf.mono inter_subset_left)

Goal state after:
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_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 : Type u_8
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_9
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_11
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_12
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
s : Set M
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
t : Set (M' × N')
ha : ContMDiffWithinAt (I'.prod J') J n h t y
fa : ContMDiffWithinAt I I' n f s x
ga : ContMDiffWithinAt I J' n g s x
e : (f x, g x) = y
st : MapsTo (fun x ↦ (f x, g x)) s t
⊢ ContMDiffWithinAt I J n (fun x ↦ h (f x, g x)) s x

Tactic:
by
  rw [← e] at ha
  exact ha.comp₂ fa ga st

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

Goal state before:
pp: case mpr
𝕜 : 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
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContinuousOn f s
⊢ (∀ (y : M'),
      ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          ContDiffOn 𝕜 n
            (↑𝓘(𝕜, E').toPartialEquiv ∘
              (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) ∘
                ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
            (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
              ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
                (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))) →
    ∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n
        (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
          f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
        (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
          ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
            (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))

Tactic:
· exact fun h' x y => (h' y).2 x 0

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'
f : M → M'
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ ContMDiffOn I I' n f univ ↔
    Continuous[inst✝⁸, inst✝³] f ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)

Tactic:
contMDiffOn_iff_target

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'
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ (ContinuousOn f univ ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (univ ∩ f ⁻¹' (extChartAt I' y).source)) ↔
    Continuous[inst✝⁸, inst✝³] f ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)