mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun i ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
i : ι
⊢ a ≤ b i → ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I

Tactic:
hbi

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun i ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
i : ι
hai : a i ≤ 0
⊢ 0 ≤ b i → ∫ (x : ℝ) in φ i, f x ∂μ = ∫ (x : ℝ) in a i..b i, f x ∂μ

Tactic:
hbi

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
⊢ ∫ (x : ℝ) in φ i, f x ∂μ = ∫ (x : ℝ) in a i..b i, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
i : ι
⊢ a ≤ b i → ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a) = ∫ (x : ℝ) in a..b i, f x ∂μ

Tactic:
hbi

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a) = ∫ (x : ℝ) in a..b i, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: 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
⊢ ‖f x - f ↑N‖ = ‖∫ (t : ℝ) in Ioc (↑N) x, f' t‖

Tactic:
← intervalIntegral.integral_of_le hx,

Goal state after:
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
⊢ ‖f x - f ↑N‖ = ‖∫ (x : ℝ) in ↑N..x, f' x‖
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
⊢ ∫ (x : ℝ) in Ioi a, f' x = m - f a

Tactic:
have hcont : ContinuousOn f (Ici a) := by
    intro x hx
    rcases hx.out.eq_or_lt with rfl | hx
    · exact hcont
    · exact (hderiv x hx).continuousAt.continuousWithinAt
  refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) ?_
  apply Tendsto.congr' _ (hf.sub_const _)
  filter_upwards [Ioi_mem_atTop a] with x hx
  have h'x : a ≤ id x := le_of_lt hx
  symm
  apply
    intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self)
      fun y hy => hderiv y hy.1
  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
  exact f'int.mono (fun y hy => hy.1) le_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
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 < ε
⊢ ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε

Tactic:
have B₁ : ∀ᶠ r in 𝓝[>] (0 : ℝ), (s ∩ ({x} + r • closedBall z ε)).Nonempty :=
    eventually_nonempty_inter_smul_of_density_one μ s x hx _ measurableSet_closedBall
      (measure_closedBall_pos μ z εpos).ne'

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
⊢ ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
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
⊢ ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε

Tactic:
have norm_a : ‖a‖ ≤ ‖z‖ + ε :=
    calc
      ‖a‖ = ‖z + (a - z)‖ := by simp only [add_sub_cancel]
      _ ≤ ‖z‖ + ‖a - z‖ := norm_add_le _ _
      _ ≤ ‖z‖ + ε := by grw [mem_closedBall_iff_norm.1 az]

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 ρ
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
norm_a : ‖a‖ ≤ ‖z‖ + ε
⊢ ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1

Tactic:
by
  rcases eq_or_ne (derivative p) 0 with hp' | hp'
  · rw [eq_C_of_derivative_eq_zero hp']
    simp
  have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
  refine Finset.card_le_sdiff_of_interleaved fun x hx y hy hxy hxy' => ?_
  rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
  obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)
  refine ⟨z, ?_, hz1⟩
  rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]

Goal state after:
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z = dslope f w₀ w₀
w : ℂ
hw : w ∈ sphere c R
h : (((fun x ↦ x) - fun x ↦ w₀) ^ 2) w = 0
⊢ False

Tactic:
exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))

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

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
S : Set (StructureGroupoid H)
⊢ ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ ⋂ s ∈ S, s.members) → e ∈ ⋂ s ∈ S, s.members

Tactic:
by
      simp only [mem_iInter]
      intro e he i hi
      refine i.locality' e ?_
      intro x hex
      rcases he x hex with ⟨s, hs⟩
      exact ⟨s, ⟨hs.left, ⟨hs.right.left, hs.right.right i hi⟩⟩⟩

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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H (↑e.symm x)
s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source
⊢ IsOpen[inst✝²] s

Tactic:
apply e.symm.continuousOn_toFun.isOpen_inter_preimage

Goal state after:
case hs
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
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := ⋯
s : Set H := ⋯
⊢ IsOpen[inst✝²] e.symm.source

case ht
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
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := ⋯
s : Set H := ⋯
⊢ IsOpen[inst✝¹] f.source
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
⊢ ↑(chartAt H (Sum.inl x)) (Sum.inl y) = ↑(chartAt H x) y

Tactic:
by
  have : Nonempty H := nonempty_of_chartedSpace x
  rw [ChartedSpace.sum_chartAt_inl]
  exact OpenPartialHomeomorph.lift_openEmbedding_apply _ _

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

Goal state before:
pp: case mp
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ idRestrGroupoid ≤ G

Tactic:
rw [StructureGroupoid.le_iff]

Goal state after:
case mp
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ ∀ e ∈ idRestrGroupoid, e ∈ G
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst✝] s
⊢ e.restr s ∈ G

Tactic:
← ofSet_trans (e : OpenPartialHomeomorph H H) hs

Goal state after:
case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst✝] s
⊢ ofSet s hs ≫ₕ e ∈ 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
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) '' s ∈ map (↑(f.extend I)) (𝓝 x)

Tactic:
Filter.mem_map

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) ⁻¹' ↑(f.extend I) '' s ∈ 𝓝 x
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
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) '' s ∈ map (↑(f.extend I)) (𝓝 x)

Tactic:
Filter.mem_map

Goal state after:
𝕜 : 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
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) ⁻¹' ↑(f.extend I) '' s ∈ 𝓝 x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case refine_1
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
this : ContinuousWithinAt ((f ∘ ↑I.symm) ∘ ↑I) ((fun x ↦ x) ⁻¹' s ∩ ↑I ⁻¹' range ↑I) x
⊢ ContinuousWithinAt f s x

Tactic:
preimage_id',

Goal state after:
case refine_1
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
this : ContinuousWithinAt ((f ∘ ↑I.symm) ∘ ↑I) (s ∩ ↑I ⁻¹' range ↑I) x
⊢ ContinuousWithinAt f s 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
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
⊢ idRestrGroupoid ≤ contDiffGroupoid n I

Tactic:
rw [StructureGroupoid.le_iff]

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
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
⊢ ∀ e ∈ idRestrGroupoid, e ∈ contDiffGroupoid n I
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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
x : M
f : M → M'
⊢ MapsTo (writtenInExtChartAt I I' x f)
    ((extChartAt I x).target ∩ f ∘ ↑(extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) (extChartAt I' (f x)).target

Tactic:
by
  intro x' hx'
  simpa using (chartAt H' (f x)).mapsTo (by simpa using hx'.2)

Goal state after:
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'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : ℕ∞ω
g : M' → M''
x : M
hf : ContMDiffAt I I' n f x
hg : ContMDiffAt I' I'' n g (f x)
⊢ ContMDiffAt I I'' n (g ∘ f) x

Tactic:
exact hg.comp x hf

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
E' : Type u_5
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H M
inst✝² : ChartedSpace H' M'
inst✝¹ : T2Space M
inst✝ : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x✝ : M
x : ↥U
h : ↑x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContMDiffAt I I' n (extend Subtype.val f 1) ↑x

Tactic:
← contMDiffAt_subtype_iff

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
E' : Type u_5
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H M
inst✝² : ChartedSpace H' M'
inst✝¹ : T2Space M
inst✝ : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x✝ : M
x : ↥U
h : ↑x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContMDiffAt I I' n (fun x ↦ extend Subtype.val f 1 ↑x) x
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'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
constructor
  · intro h
    refine ⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩
    simp only [mfld_simps] at hz
    let w := (extChartAt I x).symm z
    have : w ∈ s := by simp only [w, hz, mfld_simps]
    specialize h w this
    have w1 : w ∈ (chartAt H x).source := by simp only [w, hz, mfld_simps]
    have w2 : f w ∈ (chartAt H' y).source := by simp only [w, hz, mfld_simps]
    convert! ((contMDiffWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _
    · simp only [w, hz, mfld_simps]
    · mfld_set_tac
  · rintro ⟨hcont, hdiff⟩ x hx
    refine (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_iff.mpr ?_
    refine ⟨hcont x hx, ?_⟩
    dsimp [ContDiffWithinAtProp]
    convert! hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1
    mfld_set_tac

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 ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧ EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source ∧ ↑c x ∈ e.source

Tactic:
by
      have h1 : c' = chartAt H (f x) := by simp only [x, c', f.right_inv hX]
      have h2 : c' ∘ f ∘ c.symm = ⇑(c.symm ≫ₕ f ≫ₕ c') := rfl
      have hcx : c x ∈ c.symm ⁻¹' f.source := by simp only [c, hx, mfld_simps]
      rw [h2]
      rw [← h1, h2, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'] at hxf
      · exact hxf hcx
      · dsimp [x, c]; mfld_set_tac
      · apply Or.inl
        simp only [c, hx, h1, mfld_simps]

Goal state after:
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'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
hs : s ∈ 𝓝 x
⊢ HasMFDerivAt% f x f'

Tactic:
rwa [← univ_inter s, hasMFDerivWithinAt_inter hs, hasMFDerivWithinAt_univ] at h

Goal state after: