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

Goal state before:
pp: case hst
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
⊢ Ioc (↑N) x ≤ᵐ[volume] Ici ↑N

Tactic:
· have : Ioc (↑N) x ⊆ Ici ↑N := Ioc_subset_Ioi_self.trans Ioi_subset_Ici_self
        exact this.eventuallyLE

Goal state after:
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x ↦ (B (f x)) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y ↦ (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y ↦ (B (f (x, y))) (g' (x, y))) volume
⊢ Integrable (fun y ↦ (B (f (x, y))) (g (x, y))) volume →
    ∫ (t : ℝ), (B (f (x, t))) (g' (x, t)) = -∫ (t : ℝ), (B (f' (x, t))) (g (x, t))

Tactic:
hfgx

Goal state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x ↦ (B (f x)) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y ↦ (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y ↦ (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y ↦ (B (f (x, y))) (g (x, y))) volume
⊢ ∫ (t : ℝ), (B (f (x, t))) (g' (x, t)) = -∫ (t : ℝ), (B (f' (x, t))) (g (x, t))
Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E → F
v : E
inst✝ : SecondCountableTopologyEither E F
hf : Continuous f
⊢ StronglyMeasurable fun x ↦ lineDeriv 𝕜 f x v

Tactic:
by
  borelize 𝕜
  let g : E → 𝕜 → F := fun x t ↦ f (x + t • v)
  have hg : Continuous g.uncurry := by fun_prop
  exact (stronglyMeasurable_deriv_with_param hg).comp_measurable measurable_prodMk_right

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))

Tactic:
have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c}) := fun z hz =>
    (hz.1 hz.2).differentiableWithinAt

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))
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
⊢ ∀ᵐ (x : E) ∂μ.restrict s, dist (g x) (f' x) ≤ ε

Tactic:
suffices H : ∀ᵐ x : E ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε by
    have : μ.restrict s ≤ sum fun n => μ.restrict (s ∩ t n) := by
      have : s = ⋃ n, s ∩ t n := by
        rw [← inter_iUnion]
        exact Subset.antisymm (subset_inter Subset.rfl t_cover) inter_subset_left
      conv_lhs => rw [this]
      exact restrict_iUnion_le
    exact ae_mono this H

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
⊢ ∀ᵐ (x : E) ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case refine_1
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
⊢ ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members

Tactic:
rcases hx x hex with ⟨s, hs⟩

Goal state after:
case refine_1
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case refine_2
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
⊢ ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G'.members

Tactic:
rcases hx x hex with ⟨s, hs⟩

Goal state after:
case refine_2
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
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, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
⊢ ↑|A.det|.toNNReal - ↑ε < ↑|A.det|.toNNReal

Tactic:
apply ENNReal.sub_lt_self ENNReal.coe_ne_top

Goal state after:
case ha₀
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 := ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := ⋯
⊢ ↑|A.det|.toNNReal ≠ 0

case hb
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 := ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := ⋯
⊢ ↑ε ≠ 0
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
⊢ I.target = range ↑I

Tactic:
rw [← image_univ, ← I.source_eq]

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
⊢ I.target = ↑I '' I.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ interior (↑I.symm ⁻¹' f.target ∩ range ↑I) ⊆ interior (range ↑I)

Tactic:
interior_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
⊢ interior (↑I.symm ⁻¹' f.target) ∩ interior (range ↑I) ⊆ interior (range ↑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
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I y ∈ interior (↑I.symm ⁻¹' f.target ∩ range ↑I)

Tactic:
interior_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
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I y ∈ interior (↑I.symm ⁻¹' f.target) ∩ interior (range ↑I)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
H' : Type u_3
M' : Type u_4
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt (↑(chartAt H' (g x)) ∘ g) s x
⊢ (↑(chartAt H' (g x)) ∘ g) x ∈ ((chartAt H' (g x)).symm ≫ₕ f).source

Tactic:
simp [xf, mfld_simps]

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

Goal state before:
pp: H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ P (↑(chartAt H' (g x)) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
← hG.liftPropWithinAt_indep_chart_target_aux2 (g ∘ e.symm) hf xf

Goal state after:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ P (↑(chartAt H' (g x)) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    P (↑(chartAt H' ((g ∘ ↑e.symm) (↑e x))) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hgs : ContinuousWithinAt g s x
⊢ P ((↑(chartAt H' (g x)) ∘ g) ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
Function.comp_assoc,

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hgs : ContinuousWithinAt g s x
⊢ P (↑(chartAt H' (g x)) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

Tactic:
← liftPropWithinAt_indep_chart_aux' hG he' xe' hf' xf' hgs,

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
    P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) 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
s : Set H
⊢ s ⊆ I.source

Tactic:
rw [I.source_eq]; exact subset_univ _

Goal state after:
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) s x
⊢ ContinuousWithinAt f s x

Tactic:
Function.comp_assoc,

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 x
⊢ ContinuousWithinAt f 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
hx : x ∈ ↑I '' (e.symm ≫ₕ e').source
⊢ ↑I '' (e.symm ≫ₕ e').source ∈ 𝓝[range ↑I] x

Tactic:
obtain ⟨z, hz, rfl⟩ := hx

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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
z : H
hz : z ∈ (e.symm ≫ₕ e').source
⊢ ↑I '' (e.symm ≫ₕ e').source ∈ 𝓝[range ↑I] ↑I z
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ ∀ (o : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o →
      ↑(extChartAt I x₀) x ∈ o → (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target)).Nonempty

Tactic:
interior_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
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ ∀ (o : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o →
      ↑(extChartAt I x₀) x ∈ o →
        (o ∩ (interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target)).Nonempty
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
t : Set M
inst✝ : ChartedSpace H M
x : M
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))

Tactic:
rwa [(extChartAt I x).left_inv (mem_extChartAt_source _)]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
x x' : M
n : ℕ∞ω
inst✝ : IsManifold I n M
hx' : x' ∈ (chartAt H x).source
⊢ ContMDiffAt I I' n f x' ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')

Tactic:
simp_rw [ContMDiffAt, contMDiffWithinAt_iff_source_of_mem_source hx', preimage_univ, univ_inter]

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

Goal state before:
pp: case coe
𝕜 : 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
x : M
n : ℕ∞
h : ∀ m ≤ ↑n, m ≠ ∞ → ContMDiffWithinAt I I' m f s x
⊢ ContMDiffWithinAt I I' (↑n) f s x

Tactic:
exact contMDiffWithinAt_iff_nat.2 (fun m hm ↦ h _ (mod_cast hm) (by simp))

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.LieGroup

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜
hx : x ≠ 0
⊢ ContMDiffAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) n Inv.inv x

Tactic:
rw [contMDiffAt_iff_contDiffAt]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜
hx : x ≠ 0
⊢ ContDiffAt 𝕜 n Inv.inv x