mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, HasDerivAt (fun x ↦ F x t) (F' x t) x
⊢ IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
← ae_restrict_iff' measurableSet_uIoc

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun x_2 ↦ F x_2 x) (F' x_1 x) x_1
⊢ IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e = e'

Tactic:
refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_

Goal state after:
case refine_1
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e.source = univ

case refine_2
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e.target = univ
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
he' : e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e ≫ₕ e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}

Tactic:
constructor

Goal state after:
case left
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
he' : e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑(e ≫ₕ e')) (e ≫ₕ e').source

case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
he' : e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑(e ≫ₕ e').symm) (e ≫ₕ e').target
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}

Tactic:
constructor

Goal state after:
case left
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑e) e.source

case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑e.symm) e.target
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := ↑(c.symm ≫ₕ f₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ s

Tactic:
constructor

Goal state after:
case left
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := ⋯
f₂ : OpenPartialHomeomorph M' M'' := ⋯
f : OpenPartialHomeomorph M M'' := ⋯
feq : f = f₁ ≫ₕ f₂
y : M' := ⋯
g : OpenPartialHomeomorph M' H := ⋯
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := ⋯
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ (c.symm ≫ₕ f₁).source

case right
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := ⋯
f₂ : OpenPartialHomeomorph M' M'' := ⋯
f : OpenPartialHomeomorph M M'' := ⋯
feq : f = f₁ ≫ₕ f₂
y : M' := ⋯
g : OpenPartialHomeomorph M' H := ⋯
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := ⋯
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
⊢ e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}

Tactic:
constructor

Goal state after:
case left
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
⊢ PG.property (↑e') e'.source

case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
⊢ PG.property (↑e'.symm) e'.target
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
A : e'.symm ≈ e.symm
⊢ PG.property (↑e.symm) e'.symm.source

Tactic:
convert! he.2 using 1

Goal state after:
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
A : e'.symm ≈ e.symm
⊢ e'.symm.source = e.target
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := ↑(c.symm ≫ₕ f₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
open_s : IsOpen[inst✝⁶] s
this : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
⊢ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source ⋯) ≫ₕ f₂ ≫ₕ c' ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c'

Tactic:
by rw [trans_of_set']

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

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hse : e ≈ ofSet s hs
⊢ e.symm ≈ ofSet s hs

Tactic:
rw [← ofSet_symm]

Goal state after:
H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hse : e ≈ ofSet s hs
⊢ e.symm ≈ (ofSet s hs).symm
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G

Tactic:
constructor

Goal state after:
case mp
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G → idRestrGroupoid ≤ G

case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ idRestrGroupoid ≤ G → ClosedUnderRestriction G
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
⊢ ofSet s hs = (OpenPartialHomeomorph.refl H).restr s

Tactic:
ext

Goal state after:
case h
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑((OpenPartialHomeomorph.refl H).restr s) x✝

case hinv
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs).symm x✝ = ↑((OpenPartialHomeomorph.refl H).restr s).symm x✝

case hs
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).source ↔ x✝ ∈ ((OpenPartialHomeomorph.refl H).restr s).source
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ClosedUnderRestriction G

Tactic:
constructor

Goal state after:
case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ∀ {e : OpenPartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen[inst✝] s → e.restr s ∈ G
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
⊢ let s := { carrier := e.source, is_open' := ⋯ };
  let t := { carrier := e.target, is_open' := ⋯ };
  ∀ c' ∈ atlas H ↥t, e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c' ∈ maximalAtlas (↥s) G

Tactic:
intro s t c' hc'
  have : Nonempty t := nonempty_coe_sort.mpr (e.mapsTo.nonempty (nonempty_coe_sort.mp hs))
  obtain ⟨x, hc'⟩ := Opens.chart_eq this hc'
  -- As H has only one chart, `chartAt H x` is the identity: i.e., `c'` is the inclusion.
  rw [hc', (chartAt_self_eq)]
  -- Our expression equals this chart, at least on its source.
  rw [OpenPartialHomeomorph.subtypeRestr_def, OpenPartialHomeomorph.trans_refl]
  let goal :=
    e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ (t.openPartialHomeomorphSubtypeCoe this)
  have : goal ≈ e.subtypeRestr (s := s) hs :=
    (goal.eqOnSource_iff (e.subtypeRestr (s := s) hs)).mpr
      ⟨by
        simp only [trans_toPartialEquiv, PartialEquiv.trans_source,
          Homeomorph.toOpenPartialHomeomorph_source, toFun_eq_coe,
          Homeomorph.toOpenPartialHomeomorph_apply, Opens.openPartialHomeomorphSubtypeCoe_source,
          preimage_univ, inter_self, subtypeRestr_source, goal, s]
        exact Subtype.coe_preimage_self _ |>.symm, by intro _ _; rfl⟩
  exact G.mem_maximalAtlas_of_eqOnSource (M := s) this (G.subtypeRestr_mem_maximalAtlas he hs)

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

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P (↑e' ∘ f) s x ↔ P f s x

Tactic:
constructor

Goal state after:
case mp
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P (↑e' ∘ f) s x → P f s x

case mpr
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P f s x → P (↑e' ∘ f) s x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_2
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
this : P ((f ∘ ↑e.symm) ∘ ↑e) (↑e ⁻¹' ↑e.symm ⁻¹' s) x
x' : H
hx' : x' ∈ e.source
⊢ x' ∈ ↑e ⁻¹' ↑e.symm ⁻¹' s ↔ x' ∈ s

Tactic:
simp_rw [mem_preimage, e.left_inv hx']

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

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

Tactic:
inter_eq_self_of_subset_right

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

𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
hs : s ⊆ f.source
⊢ s ⊆ (f.extend I).source
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type w
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝⁴ : I.Boundaryless
E' : Type v'
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H' : Type w'
inst✝¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst✝ : I'.Boundaryless
⊢ (I.prod I').Boundaryless

Tactic:
constructor

Goal state after:
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type w
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝⁴ : I.Boundaryless
E' : Type v'
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H' : Type w'
inst✝¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst✝ : I'.Boundaryless
⊢ range ↑(I.prod I') = univ
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
u : OpenPartialHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑u ∘ ↑I.symm) (↑I.symm ⁻¹' u.source ∩ range ↑I) ∧
    ContinuousOn (↑I ∘ ↑u.symm ∘ ↑I.symm) (↑I.symm ⁻¹' u.target ∩ range ↑I)

Tactic:
constructor

Goal state after:
case left
𝕜 : 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
u : OpenPartialHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑u ∘ ↑I.symm) (↑I.symm ⁻¹' u.source ∩ range ↑I)

case right
𝕜 : 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
u : OpenPartialHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑u.symm ∘ ↑I.symm) (↑I.symm ⁻¹' u.target ∩ range ↑I)
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
hu : IsOpen[inst✝¹] u
hux : x ∈ u
⊢ G.IsLocalStructomorphWithinAt f s x ↔ G.IsLocalStructomorphWithinAt f (s ∩ u) x

Tactic:
constructor

Goal state after:
case mp
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
⊢ G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt f (s ∩ u) x

case mpr
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
⊢ G.IsLocalStructomorphWithinAt f (s ∩ u) x → G.IsLocalStructomorphWithinAt f s x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid n I

Tactic:
constructor

Goal state after:
case left
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 = ∅
⊢ (contDiffPregroupoid n I).property (↑f) f.source

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 = ∅
⊢ (contDiffPregroupoid n I).property (↑f.symm) f.target
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')

Tactic:
obtain ⟨he', he'_symm⟩ := he'

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')