mathlib-initiative/mathlib-tactics huggingface dataset:
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 (g x) (f' x) ≤ ε

Tactic:
hx2,

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
ε : ℝ
ε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 (A n) (f' x) ≤ ε
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x, (chartAt H ↑x).source = univ
hsc : s.Countable
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source
this : Encodable ↑s
⊢ SecondCountableTopology M

Tactic:
exact secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs

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

Goal state before:

Tactic:
‖B - A‖ ≤ (min δ δ'' : ℝ≥0) := hB
        _ ≤ δ'' := by simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]
        _ < δ' := half_lt_self δ'pos

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
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := ⋯
⊢ ↑e ↑x ∈ (e.subtypeRestr ⋯).target

Tactic:
exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

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
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := ⋯
⊢ ↑e ↑x ∈ (e.subtypeRestr ⋯).target

Tactic:
exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

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
ε : ℝ≥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) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ 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))
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
⊢ |(A n).det| = |(f' x).det - ((f' x).det - (A n).det)|

Tactic:
congr 1; abel

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
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 ↦ ?_
  refine (continuousWithinAt_congr_set ?_).trans
    (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)
  rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin_eq_image_of_subset,
    ← map_extend_nhdsWithin]
  exacts [hs hx, hs hx, hs]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (extendCoordChange e e').symm.source = ↑I '' (e.symm ≫ₕ e').symm.source

Tactic:
exact I.extendCoordChange_source

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

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

Tactic:
intro t g htg
      rcases eq_or_ne (μ t) ∞ with (ht | ht)
      · simp only [ht, εpos.ne', ENNReal.mul_top, ENNReal.coe_eq_zero, le_top, Ne,
          not_false_iff, _root_.add_top]
      have := h t g (htg.mono_num (min_le_left _ _))
      rwa [ENNReal.coe_sub, ENNReal.sub_mul, tsub_le_iff_right] at this
      simp only [ht, imp_true_iff, Ne, not_false_iff]

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

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : y ∈ ↑(chartAt H x).symm ⁻¹' t
⊢ y ∈ ↑(chartAt H x).symm ⁻¹' s

Tactic:
simp only [mfld_simps] at hy

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : ↑(chartAt H x).symm y ∈ t
⊢ y ∈ ↑(chartAt H x).symm ⁻¹' s
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case right
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 = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.target
right✝ : x ∈ range ↑I
this : f.target = ∅
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I) x

Tactic:
simp_all

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 < ε
δ : (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
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
⊢ |(f' x).det| = |(A n).det + ((f' x).det - (A n).det)|

Tactic:
congr 1; abel

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

Goal state before:
pp: case refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : ↑e' x ∈ ↑e'.symm ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ ↑e'.symm ⁻¹' s ∩ (e'.symm ≫ₕ e).source
⊢ (f ∘ ↑e'.symm) y = ↑(e'.symm ≫ₕ e).toPartialEquiv y

Tactic:
simp only [mfld_simps] at hy

Goal state after:
case refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : ↑e' x ∈ ↑e'.symm ⁻¹' s
hxs : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : ↑e'.symm y ∈ s ∧ y ∈ e'.target ∧ ↑e'.symm y ∈ e.source
⊢ (f ∘ ↑e'.symm) y = ↑(e'.symm ≫ₕ e).toPartialEquiv y
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ s ∩ (e ≫ₕ e').source
⊢ (↑e' ∘ f) y = ↑(e ≫ₕ e').toPartialEquiv y

Tactic:
simp only [mfld_simps] at hy

Goal state after:
case refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ s ∧ y ∈ e.source ∧ ↑e y ∈ e'.source
⊢ (↑e' ∘ f) y = ↑(e ≫ₕ e').toPartialEquiv 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 ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x).target)

Tactic:
by
  intro y hy
  rw [mem_closure_iff_nhds]
  intro t ht
  have A : t ∩ ((extChartAt I x).target ∪ (range I)ᶜ) ∈ 𝓝 y :=
    inter_mem ht (extChartAt_target_union_compl_range_mem_nhds_of_mem hy)
  have B : y ∈ closure (interior (range I)) := by
    apply I.range_subset_closure_interior (extChartAt_target_subset_range x hy)
  obtain ⟨z, ⟨tz, h'z⟩, hz⟩ :
      (t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∩ interior (range I)).Nonempty :=
    mem_closure_iff_nhds.1 B _ A
  refine ⟨z, ⟨tz, ?_⟩⟩
  have h''z : z ∈ (extChartAt I x).target := by simpa [interior_subset hz] using h'z
  exact (extChartAt_target_eventuallyEq_of_mem h''z).symm.mem_interior hz

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

Goal state before:
pp: case mpr
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ᶜ
⊢ (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source) →
    G.IsLocalStructomorphWithinAt (↑f) s x

Tactic:
intro hf hx

Goal state after:
case mpr
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 : x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source
hx : x ∈ s
⊢ ∃ e ∈ G, EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : OpenPartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : OpenPartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : OpenPartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
⊢ (e ≫ₕ f).symm ≫ₕ e' ≫ₕ f' ∈ G₁

Tactic:
apply G₁.locality

Goal state after:
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ⋯
e : OpenPartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : OpenPartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : OpenPartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : OpenPartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
⊢ ∀ x ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source, ∃ s, IsOpen[inst✝⁷] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : f' ∈ atlas H M'
he'f' : e' = f'.lift_openEmbedding ⋯
x : H
x✝ : x ∈ ((f.lift_openEmbedding ⋯).symm ≫ₕ f'.lift_openEmbedding ⋯).source
hx₁ : x ∈ (f.lift_openEmbedding ⋯).symm.symm.target
hx₂ : x ∈ ↑(f.lift_openEmbedding ⋯).symm.symm.symm ⁻¹' (f'.lift_openEmbedding ⋯).source
⊢ x ∈ ∅

Tactic:
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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : f ∈ atlas H M'
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : f' ∈ atlas H M
he'f' : e' = f'.lift_openEmbedding ⋯
x : H
x✝ : x ∈ ((f.lift_openEmbedding ⋯).symm ≫ₕ f'.lift_openEmbedding ⋯).source
hx₁ : x ∈ (f.lift_openEmbedding ⋯).symm.symm.target
hx₂ : x ∈ ↑(f.lift_openEmbedding ⋯).symm.symm.symm ⁻¹' (f'.lift_openEmbedding ⋯).source
⊢ x ∈ ∅

Tactic:
simp_all

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

Goal state before:
pp: case h₁
𝕜 : 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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
y : E
hy : y ∈ ↑I.symm ⁻¹' s ∩ range ↑I
⊢ (↑I' ∘ g ∘ ↑I.symm) y = (↑I' ∘ f ∘ ↑I.symm) y

Tactic:
simp only [mfld_simps] at hy

Goal state after:
case h₁
𝕜 : 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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
y : E
hy : ↑I.symm y ∈ s ∧ y ∈ range ↑I
⊢ (↑I' ∘ g ∘ ↑I.symm) y = (↑I' ∘ f ∘ ↑I.symm) y
Module: Mathlib.Geometry.Manifold.ContMDiff.Basic

Goal state before:
pp: case succ
𝕜 : 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
s : Set M
n : ℕ∞ω
f : M → M
hf : ContMDiffOn I I n f s
hmaps : MapsTo f s s
k : ℕ
h : ContMDiffOn I I n f^[k] s
⊢ ContMDiffOn I I n f^[k + 1] s

Tactic:
simpa using h.comp hf hmaps

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
M' : Type u_16
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
n : WithTop ℕ∞
⊢ ContMDiff I I n Sum.inl

Tactic:
intro x
  rw [contMDiffAt_iff]
  refine ⟨continuous_inl.continuousAt, ?_⟩
  -- In extended charts, .inl equals the identity (on the chart sources).
  apply contDiffWithinAt_id.congr_of_eventuallyEq; swap
  · simp [ChartedSpace.sum_chartAt_inl, Sum.inl_injective.extend_apply (chartAt _ x)]
  set C := chartAt H x with hC
  have : I.symm ⁻¹' C.target ∩ range I ∈ 𝓝[range I] (extChartAt I x) x := by
    rw [← I.image_eq (chartAt H x).target]
    exact (chartAt H x).extend_image_target_mem_nhds (mem_chart_source _ x)
  filter_upwards [this] with y hy
  simp [extChartAt, sum_chartAt_inl, ← hC, Sum.inl_injective.extend_apply C, C.right_inv hy.1,
    I.right_inv hy.2]

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 n (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
y : E
hy : y ∈ ↑I.symm ⁻¹' s ∩ range ↑I
⊢ (↑I' ∘ f ∘ ↑I.symm) y ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'

Tactic:
simp only [mfld_simps] at hy

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 n (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
y : E
hy : ↑I.symm y ∈ s ∧ y ∈ range ↑I
⊢ (↑I' ∘ f ∘ ↑I.symm) y ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
x : M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ ContinuousWithinAt (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' ((f ∘ ↑e.symm) (↑e x))) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    ContinuousWithinAt (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      ContDiffWithinAtProp 𝓘(𝕜, E) I' n
        (↑(chartAt H' ((f ∘ ↑(e.extend I).symm) (↑(e.extend I) x))) ∘ f ∘ ↑(e.extend I).symm)
        (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)

Tactic:
contDiffWithinAtProp_self_source,

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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
x : M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ ContinuousWithinAt (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' ((f ∘ ↑e.symm) (↑e x))) ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    ContinuousWithinAt (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ∧
      ContDiffWithinAt 𝕜 n (↑I' ∘ ↑(chartAt H' ((f ∘ ↑(e.extend I).symm) (↑(e.extend I) x))) ∘ f ∘ ↑(e.extend I).symm)
        (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x)