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
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
h2δ : ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : PartialEquiv E E := hf'.toPartialEquiv h1δ
H : μ (↑F.symm '' F.target) ≤ ↑m⁻¹ * μ F.target
⊢ ↑m * μ s ≤ μ (f '' s)

Tactic:
change (m : ℝ≥0∞) * μ F.source ≤ μ F.target

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹
h2δ : ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : PartialEquiv E E := hf'.toPartialEquiv h1δ
H : μ (↑F.symm '' F.target) ≤ ↑m⁻¹ * μ F.target
⊢ ↑m * μ F.source ≤ μ F.target
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case e'_2
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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
A : ∫ (x : ℝ) in e '' s, g (n x) = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
B : ∫ (x : ℝ) in n ∘ e '' s, g x = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
⊢ f '' s = n ∘ e '' s

Tactic:
simp [n, e]

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

Goal state before:
pp: case e'_3
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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
A : ∫ (x : ℝ) in e '' s, g (n x) = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
B : ∫ (x : ℝ) in n ∘ e '' s, g x = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
x : ℝ
⊢ -f' x • g (f x) = -f' x • (g ∘ n) (e x)

Tactic:
simp [n, e]

Goal state after:
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 ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
s : Set ℝ
hs : s ∈ atTop
b : ℝ
hb : ∀ (b_1 : ℝ), b ≤ b_1 → b_1 ∈ s
⊢ volume s = ∞

Tactic:
← top_le_iff,

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
s : Set ℝ
hs : s ∈ atTop
b : ℝ
hb : ∀ (b_1 : ℝ), b ≤ b_1 → b_1 ∈ s
⊢ ∞ ≤ volume s
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 ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
s : Set ℝ
hs : s ∈ atTop
b : ℝ
hb : ∀ (b_1 : ℝ), b ≤ b_1 → b_1 ∈ s
⊢ volume s = ∞

Tactic:
rw [← top_le_iff, ← volume_Ici (a := b)]

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
s : Set ℝ
hs : s ∈ atTop
b : ℝ
hb : ∀ (b_1 : ℝ), b ≤ b_1 → b_1 ∈ s
⊢ volume (Ici b) ≤ volume s
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

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

Tactic:
have : 0 ≤ c ^ p⁻¹ := by positivity

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

Goal state before:
pp: case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
      ?_ hc).differentiableAt.differentiableWithinAt

Goal state after:
case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] x, DifferentiableAt ℂ f z
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✝ : LocallyCompactSpace H
this :
  ∀ (x : M),
    (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 (↑(chartAt H x) x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target) fun s ↦
      ↑(chartAt H x).symm '' s
⊢ ∀ (x : M) (i : Set H),
    i ∈ 𝓝 (↑(chartAt H x) x) ∧ IsCompact i ∧ i ⊆ (chartAt H x).target → IsCompact (↑(chartAt H x).symm '' i)

Tactic:
rintro x s ⟨_, h₂, h₃⟩

Goal state after:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyCompactSpace H
this :
  ∀ (x : M),
    (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 (↑(chartAt H x) x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target) fun s ↦
      ↑(chartAt H x).symm '' s
x : M
s : Set H
left✝ : s ∈ 𝓝 (↑(chartAt H x) x)
h₂ : IsCompact s
h₃ : s ⊆ (chartAt H x).target
⊢ IsCompact (↑(chartAt H x).symm '' s)
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
⊢ OpenPartialHomeomorph.refl H ≈ ofSet univ ⋯

Tactic:
simp only [mfld_simps, refl]

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
⊢ UniqueDiffOn 𝕜 (extendCoordChange e e').target

Tactic:
by
  rw [← extendCoordChange_symm, PartialEquiv.symm_target]
  exact uniqueDiffOn_extendCoordChange_source

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
s : Set H
x : H
⊢ ∀ {u : Set H} {f : H → H},
    IsOpen[inst✝¹] u → x ∈ u → (G.IsLocalStructomorphWithinAt f s x ↔ G.IsLocalStructomorphWithinAt f (s ∩ u) x)

Tactic:
u

Goal state after:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
⊢ ∀ {f : H → H},
    IsOpen[inst✝¹] u → x ∈ u → (G.IsLocalStructomorphWithinAt f s x ↔ G.IsLocalStructomorphWithinAt f (s ∩ u) x)
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
hx : x ∈ f.source ∪ sᶜ
⊢ G.IsLocalStructomorphWithinAt (↑f) s x ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
by
  constructor
  · intro hf h2x
    obtain ⟨e, he, hfe, hxe⟩ := hf h2x
    refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩
    · simp_rw [OpenPartialHomeomorph.restr_source]
      exact inter_subset_right.trans interior_subset
    · intro x' hx'
      exact hfe ⟨hx'.1, hx'.2.1⟩
    · rw [f.open_source.interior_eq]
      exact Or.resolve_right hx (not_not.mpr h2x)
  · intro hf hx
    obtain ⟨e, he, _, hfe, hxe⟩ := hf hx
    exact ⟨e, he, hfe, hxe⟩

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

Goal state before:
pp: case hn
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 : ℕ
⊢ ∀ ⦃j : ℕ⦄, i ≠ j → (Disjoint on fun i ↦ f '' (s ∩ t i)) i j

Tactic:
j

Goal state after:
case hn
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 j : ℕ
⊢ i ≠ j → (Disjoint on fun i ↦ f '' (s ∩ t i)) i j
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case hn
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 j : ℕ
hij : i ≠ j
⊢ (Disjoint on fun i ↦ f '' (s ∩ t i)) i j

Tactic:
apply Disjoint.image _ hf inter_subset_left inter_subset_left

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 < ε
δ : (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 j : ℕ
hij : i ≠ j
⊢ Disjoint (s ∩ t i) (s ∩ t j)
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 (↑(extChartAt I x).symm y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
⊢ LocallyCompactSpace E

Tactic:
have : IsCompact <| (extChartAt I x) '' s :=
    hcom.image_of_continuousOn <| (continuousOn_extChartAt x).mono hss

Goal state after:
E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 (↑(extChartAt I x).symm y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact (↑(extChartAt I x) '' s)
⊢ LocallyCompactSpace E
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:
rw [← e] at ha
  exact ha.comp₂ fa ga st

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 ℕ∞
x : M'
⊢ ContinuousAt Sum.inr x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I (Sum.inr x)) ∘ Sum.inr ∘ ↑(extChartAt I x).symm) (range ↑I)
      (↑(extChartAt I x) x)

Tactic:
refine ⟨continuous_inr.continuousAt, ?_⟩

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
M' : Type u_16
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
n : WithTop ℕ∞
x : M'
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt I (Sum.inr x)) ∘ Sum.inr ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case hn
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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
i : ℕ
⊢ ∀ ⦃j : ℕ⦄, i ≠ j → (Disjoint on fun i ↦ f '' (s ∩ u i)) i j

Tactic:
j

Goal state after:
case hn
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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
i j : ℕ
⊢ i ≠ j → (Disjoint on fun i ↦ f '' (s ∩ u i)) i j
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case hn
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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
i j : ℕ
hij : i ≠ j
⊢ (Disjoint on fun i ↦ f '' (s ∩ u i)) i j

Tactic:
apply Disjoint.image _ hf inter_subset_left inter_subset_left

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
u : ℕ → Set E := ⋯
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
i j : ℕ
hij : i ≠ j
⊢ Disjoint (s ∩ u i) (s ∩ u j)
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_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J n (Sum.inr ∘ g)
⊢ ContMDiff I J n g

Tactic:
nontriviality N'
  inhabit N'
  let aux : N ⊕ N' → N' := Sum.elim (fun _ ↦ inhabited_h.default) (@id N')
  have : aux ∘ (@Sum.inr N N') ∘ g = g := by ext; simp [aux]
  rw [← this]
  rw [← contMDiffOn_univ] at h ⊢
  apply ((contMDiff_const.sumElim contMDiff_id).contMDiffOn (s := Sum.inr '' univ)).comp h
  intro x _hx
  rw [mem_preimage, Function.comp_apply]
  use g x, trivial

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 : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst✝ : Nonempty M
⊢ ContMDiff I I n e

Tactic:
have := h.isManifold_singleton (I := I) (n := ω)
  rw [@contMDiff_iff _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace]
  use h.continuous
  intro x y
  -- show the function is actually the identity on the range of I ∘ e
  apply contDiffOn_id.congr
  intro z hz
  -- factorise into the chart `e` and the model `id`
  simp only [mfld_simps]
  rw [h.toOpenPartialHomeomorph_right_inv]
  · rw [I.right_inv]
    apply mem_of_subset_of_mem _ hz.1
    exact letI := h.singletonChartedSpace; extChartAt_target_subset_range (I := I) x
  · -- `hz` implies that `z ∈ range (I ∘ e)`
    have := hz.1
    rw [@extChartAt_target _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace] at this
    have := this.1
    rw [mem_preimage, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq,
      h.toOpenPartialHomeomorph_target] at this
    exact this

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
⊢ ∀ {u : Set H} {f : H → H'},
    IsOpen[inst✝³] u → x ∈ u → (DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x)

Tactic:
u

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'
s : Set H
x : H
u : Set H
⊢ ∀ {f : H → H'},
    IsOpen[inst✝³] u → x ∈ u → (DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x)