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

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

Tactic:
exact h2f.filter_mono _root_.atTop_le_cocompact |>.tendsto

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 < ε
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 ∈ closedBall z ε, y = x + r • a

Tactic:
simp only [mem_smul_set, image_add_left, mem_preimage, singleton_add] at hy
    rcases hy with ⟨a, az, ha⟩
    exact ⟨a, az, by simp only [ha, add_neg_cancel_left]⟩

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
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ ∑' (n : ℕ), ↑(|(A n).det|.toNNReal + 1) * μ (s ∩ t n) ≤ ∑' (n : ℕ), ↑(|(A n).det|.toNNReal + 1) * 0

Tactic:
gcongr with n
      exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi a, g (x * b) = b⁻¹ • ∫ (x : ℝ) in Ioi (a * b), g x

Tactic:
simpa [mul_comm] using integral_comp_mul_left_Ioi g a hb

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
    have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
    obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2
    exact ⟨‖f x‖, hfM x hx, hx'⟩

Goal state after:
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') (Iic a) volume
hu'v : IntegrableOn (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 = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x

Tactic:
by
  rw [Pi.mul_def] at huv' hu'v
  rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
  simpa only [add_comm] using integral_Iic_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty

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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := ⟨ε, ⋯⟩
δpos : 0 < δ
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) δ
right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), g x = A n
x : E
hx1 : nndist (f' x) (A n) ≤ δ
hx2 : g x = A n
⊢ dist (f' x) (A n) ≤ ε

Tactic:
exact hx1

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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
this : s = t ∪ s \ t
⊢ μ (f '' (s \ t)) = 0

Tactic:
apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _
      (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2

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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
this : s = t ∪ s \ t
x : E
hx : x ∈ s \ t
⊢ DifferentiableWithinAt ℝ f (s \ t) x
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✝
inst✝⁶ : TopologicalSpace M✝
inst✝⁵ : ChartedSpace H✝ M✝
H : Type u_5
inst✝⁴ : TopologicalSpace H
H' : Type u_6
inst✝³ : TopologicalSpace H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H H'
inst✝ : ChartedSpace H' M
p : M
⊢ p ∈ (chartAt H' p ≫ₕ chartAt H (↑(chartAt H' p) p)).source

Tactic:
simp only [mfld_simps]

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

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

Tactic:
← Real.dist_eq

Goal state after:
case refine_1
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑(min δ δ'')
⊢ dist B.det A.det ≤ ↑ε
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 e' : OpenPartialHomeomorph H H
he' : e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
he : e ∈ {e | e.source = ∅}
this : (e ≫ₕ e').source ⊆ ∅
⊢ e ≫ₕ e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}

Tactic:
have : e ≫ₕ e' ∈ { e : OpenPartialHomeomorph H H | e.source = ∅ } := eq_bot_iff.2 this

Goal state after:
case inr
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' : e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
he : e ∈ {e | e.source = ∅}
this✝ : (e ≫ₕ e').source ⊆ ∅
this : e ≫ₕ e' ∈ {e | e.source = ∅}
⊢ e ≫ₕ e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u_5
H' : Type u_6
α : Type u_7
f : H → α
⊢ (range fun p ↦ (f p.1, p.2)) = range f ×ˢ univ

Tactic:
rw [prod_range_univ_eq]
  rfl

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

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e✝ e : PartialEquiv M H
he : e ∈ c.atlas
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
⊢ IsOpen[inst✝] (e.target ∩ e.invFun ⁻¹' t)

Tactic:
ts

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
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
⊢ IsOpen[inst✝] (e.target ∩ e.invFun ⁻¹' (↑e' ⁻¹' s ∩ e'.source))
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
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
have u_meas : ∀ n, MeasurableSet (u n) := by
    intro n
    apply MeasurableSet.disjointed fun i => ?_
    exact measurableSet_spanningSets μ i

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)
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
h : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h}
⊢ e.source = (ofSet e.source ⋯).source

Tactic:
simp only [mfld_simps]

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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ |B.det - A.det| ≤ ↑ε

Tactic:
← Real.dist_eq

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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ dist B.det A.det ≤ ↑ε
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 : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : OpenPartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
⊢ EqOn (↑goal.toPartialEquiv) (↑(e.subtypeRestr hs).toPartialEquiv) goal.source

Tactic:
intro _

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : OpenPartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
x✝ : ↑e.source
⊢ x✝ ∈ goal.source → ↑goal.toPartialEquiv x✝ = ↑(e.subtypeRestr hs).toPartialEquiv x✝
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: case pos
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 : OpenPartialHomeomorph M H
he : e ∈ atlas H M
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
h : Nonempty ↑e.source
⊢ Structomorph G ↥s ↥t

Tactic:
exact { e.toHomeomorphSourceTarget with
      mem_groupoid :=
        -- The atlas of H on itself has only one chart, hence c' is the inclusion.
        -- Then, compatibility of `G` *almost* yields our claim --- except that `e` is a chart
        -- on `M` and `c` is one on `s`: we need to show that restricting `e` to `s` and composing
        -- with `c'` yields a chart in the maximal atlas of `s`.
        fun c c' hc hc' ↦ G.compatible_of_mem_maximalAtlas (G.subset_maximalAtlas hc)
          (G.restriction_mem_maximalAtlas_subtype he h c' hc') }

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).target ⊆ range ↑I

Tactic:
simp only [mfld_simps]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ 𝓝[↑(f.extend I) '' ((f.extend I).source ∩ s)] ↑(f.extend I) y =
    𝓝[↑(f.extend I).symm ⁻¹' s] ↑(f.extend I) y ⊓ 𝓝[(f.extend I).target] ↑(f.extend I) y

Tactic:
← nhdsWithin_inter,

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
s : Set M
y : M
hy : y ∈ f.source
⊢ 𝓝[↑(f.extend I) '' ((f.extend I).source ∩ s)] ↑(f.extend I) y =
    𝓝[↑(f.extend I).symm ⁻¹' s ∩ (f.extend I).target] ↑(f.extend I) y
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
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I).symm) (𝓝[range ↑I] ↑(f.extend I) y) = 𝓝 y

Tactic:
← nhdsWithin_univ,

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
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I).symm) (𝓝[range ↑I] ↑(f.extend I) y) = 𝓝[univ] y
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
⊢ ContinuousOn (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) ↔ ContinuousOn g s

Tactic:
refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_

Goal state after:
𝕜 : 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ ContinuousWithinAt (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) (↑(f.extend I) x) ↔
    ContinuousWithinAt g 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
x : E
left✝ : x ∈ ↑I.symm ⁻¹' univ
hx2 : x ∈ range ↑I
y : H
hy : ↑I y = x
⊢ (↑I ∘ id ∘ ↑I.symm) (↑I y) = id (↑I y)

Tactic:
simp only [mfld_simps]

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

Goal state before:
pp: 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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid n I

Tactic:
constructor
  · intro x ⟨hx, _⟩
    rw [mem_preimage] at hx
    simp_all only [mem_empty_iff_false]
  · intro x ⟨hx, _⟩
    have : f.target = ∅ := by simp [← f.image_source_eq_target, hf]
    simp_all

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ continuousGroupoid H

Tactic:
← contDiffGroupoid_zero_eq (I := I)

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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid 0 I
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case mpr.refine_2
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst✝¹] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ EqOn f (↑(e.restr (interior u)).toPartialEquiv) (s ∩ (e.restr (interior u)).source)

pp: case mpr.refine_3
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst✝¹] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ x ∈ (e.restr (interior u)).source

Tactic:
· have : s ∩ u ∩ e.source = s ∩ (e.source ∩ u) := by mfld_set_tac
          simpa only [this, interior_interior, hu.interior_eq, mfld_simps] using hef

Goal state after:
case mpr.refine_3
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst✝¹] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f (s ∩ u) x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ u ∩ e.source)
hex : x ∈ e.source
⊢ x ∈ (e.restr (interior u)).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
inst✝ : ChartedSpace H M
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 y

Tactic:
← nhdsWithin_univ,

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
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝[univ] y
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
x : M
⊢ (extChartAt I x).target ⊆ range ↑I

Tactic:
simp only [mfld_simps]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E

Tactic:
simp only [mfld_simps]

Goal state after: