mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : CommMonoid α
f : ι → β → α
g : β → α
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
h : ∀ (x : β), ∃ t ∈ 𝓝 x, HasProdUniformlyOn f g t
⊢ ∀ (x : β), ∃ t ∈ 𝓝 x, TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop t

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : CommMonoid α
f : ι → β → α
g : β → α
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
h : ∀ (x : β), ∃ t ∈ 𝓝 x, HasProdUniformlyOn f g t
⊢ ∀ (x : β), ∃ t ∈ 𝓝 x, TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop t
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop K

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop K
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 ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (a : ℝ) in Ioi a, u a * v' a + u' a * v a = b' - a'

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (a : ℝ) in Ioi a, u a * v' a + u' a * v a = b' - a'
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : HasProdLocallyUniformly f g
⊢ TendstoLocallyUniformly (fun x1 x2 ↦ ∏ i ∈ Finset.range x1, f i x2) g atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : HasProdLocallyUniformly f g
⊢ TendstoLocallyUniformly (fun x1 x2 ↦ ∏ i ∈ Finset.range x1, f i x2) g atTop
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 + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
htendsto : Tendsto f atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'

Tactic:
simpa using

Goal state after:
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 + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
htendsto : Tendsto f atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
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 (fun i ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (a : ℝ) in Iic a, u a * v' a + u' a * v a = a' - b'

Tactic:
simpa using

Goal state after:
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 (fun i ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (a : ℝ) in Iic a, u a * v' a + u' a * v a = a' - b'
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case inl
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M
⊢ Sum.inl x ∈ ((ChartedSpace.chartAt x).lift_openEmbedding ⋯).source

Tactic:
lift_openEmbedding_source,

Goal state after:
case inl
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M
⊢ Sum.inl x ∈ Sum.inl '' (ChartedSpace.chartAt x).source
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case inr
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M'
⊢ Sum.inr x ∈ ((ChartedSpace.chartAt x).lift_openEmbedding ⋯).source

Tactic:
lift_openEmbedding_source,

Goal state after:
case inr
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M'
⊢ Sum.inr x ∈ Sum.inr '' (ChartedSpace.chartAt x).source
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✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
⊢ ChartedSpace H (M ⊕ M')

Tactic:
by
  by_cases! h : Nonempty H
  · exact ChartedSpace.sumOfNonempty
  have : IsEmpty M := isEmpty_of_chartedSpace H
  have : IsEmpty M' := isEmpty_of_chartedSpace H
  exact empty H (M ⊕ M')

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
E : e.target ∩ ↑e.symm ⁻¹' e.source = e.target
⊢ IsOpen[inst✝] e.target

Tactic:
simpa using

Goal state after:
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
E : e.target ∩ ↑e.symm ⁻¹' e.source = e.target
⊢ IsOpen[inst✝] e.target
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
f : PartialEquiv H H := e.symm ≫ e'
⊢ IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)

Tactic:
simpa using

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
f : PartialEquiv H H := e.symm ≫ e'
⊢ IsOpen[inst✝] (↑e' ∘ ↑e.symm ⁻¹' s ∩ (e.target ∩ ↑e.symm ⁻¹' e'.source))
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
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)
A : ↑e' ∘ ↑e.symm ⁻¹' s ∩ (e.target ∩ ↑e.symm ⁻¹' e'.source) = e.target ∩ (↑e' ∘ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source)
⊢ IsOpen[inst✝] (e.target ∩ e.invFun ⁻¹' (↑e' ⁻¹' s ∩ e'.source))

Tactic:
simpa using

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
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)
A : ↑e' ∘ ↑e.symm ⁻¹' s ∩ (e.target ∩ ↑e.symm ⁻¹' e'.source) = e.target ∩ (↑e' ∘ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source)
⊢ IsOpen[inst✝] (e.target ∩ (↑e' ∘ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' 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
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ Tendsto (fun ε ↦ 2 * ↑ε) (𝓝 0) (𝓝 (2 * ↑0))

Tactic:
exact ENNReal.Tendsto.const_mul (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr ENNReal.coe_ne_top)

Goal state after:
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}
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst✝] s'
hes' : e.restr s ≈ ofSet s' hs'
hes : x ∈ (e.restr s).source
⊢ ↑e x = ↑(ofSet e.source ⋯) x

Tactic:
simpa using

Goal state after:
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}
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst✝] s'
hes' : e.restr s ≈ ofSet s' hs'
hes : x ∈ (e.restr s).source
⊢ ↑e x = x
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

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

Tactic:
by
  rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe]

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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑φ
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ↑φ.symm
⊢ (interior (range ↑φ)).Nonempty

Tactic:
by
    have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
    simp [this, htarget]

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
h : ¬IsRCLikeNormedField 𝕜
⊢ range ↑I = univ

Tactic:
simpa using

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
h : ¬IsRCLikeNormedField 𝕜
⊢ range ↑I = univ
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: 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

Tactic:
simpa using

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 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
⊢ ¬A.det = 0
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
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto (↑(f.extend I) ∘ g) l (𝓝 (↑(f.extend I) y))
u : Set M
hu : u ∈ 𝓝 y
this : Tendsto (↑(f.extend I).symm ∘ ↑(f.extend I) ∘ g) l (𝓝 y)
z : α
hz : g z ∈ f.source
hzu : z ∈ ↑(f.extend I).symm ∘ ↑(f.extend I) ∘ g ⁻¹' u
⊢ z ∈ g ⁻¹' u

Tactic:
simpa using

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
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto (↑(f.extend I) ∘ g) l (𝓝 (↑(f.extend I) y))
u : Set M
hu : u ∈ 𝓝 y
this : Tendsto (↑(f.extend I).symm ∘ ↑(f.extend I) ∘ g) l (𝓝 y)
z : α
hz : g z ∈ f.source
hzu : z ∈ ↑(f.extend I).symm ∘ ↑(f.extend I) ∘ g ⁻¹' u
⊢ g z ∈ u
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
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := ⋯
this : NormedSpace ℝ E := ⋯
⊢ Convex ℝ (range ↑I)

Tactic:
simpa using

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
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := ⋯
this : NormedSpace ℝ E := ⋯
⊢ Convex ℝ (range ↑I)
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
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
⊢ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    P (↑(chartAt H' ((g ∘ ↑e.symm) (↑e x))) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
rw [Function.comp_apply, e.left_inv xe, ← Function.comp_assoc,
    hG.liftPropWithinAt_indep_chart_source_aux (chartAt _ (g x) ∘ g) he xe, Function.comp_assoc]

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'
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
h : ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
h1 : ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e.symm.symm x)
this : ContinuousAt (↑f) ((g ∘ ↑e.symm) (↑e x))
⊢ ContinuousWithinAt (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
exact this.comp_continuousWithinAt h1

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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F)

Tactic:
by ext1 <;> simp

Goal state after:
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
this : s ∩ u ∩ e.source = s ∩ (e.source ∩ u)
⊢ EqOn f (↑(e.restr (interior u)).toPartialEquiv) (s ∩ (e.restr (interior u)).source)

Tactic:
simpa using

Goal state after:
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
this : s ∩ u ∩ e.source = s ∩ (e.source ∩ u)
⊢ EqOn f (↑e) (s ∩ (e.source ∩ u))
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 y : M
hx : y ∈ (extChartAt I x).source
h'x : ↑(extChartAt I x) y ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 y
⊢ y ∈ (chartAt H x).source

Tactic:
simpa using

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
x y : M
hx : y ∈ (extChartAt I x).source
h'x : ↑(extChartAt I x) y ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 y
⊢ y ∈ (chartAt H x).source
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
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
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
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
⊢ x ∈ s
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_2
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
⊢ x ∈ (e ≫ₕ e').source

Tactic:
simpa using

Goal state after:
case refine_2
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
⊢ ↑e x ∈ e'.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
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
⊢ z ∈ (extChartAt I x).target

Tactic:
simpa using

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
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
⊢ ↑I.symm z ∈ (chartAt H x).target
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
s : Set E
x x' : M
hx : x' ∈ (extChartAt I x).source
hs : s ∈ 𝓝[range ↑I] ↑(extChartAt I x) x'
⊢ x' ∈ (chartAt H x).source

Tactic:
simpa using

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
s : Set E
x x' : M
hx : x' ∈ (extChartAt I x).source
hs : s ∈ 𝓝[range ↑I] ↑(extChartAt I x) x'
⊢ x' ∈ (chartAt H x).source