awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
rw : u ∈ 𝓝 x
⊢ u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))

Tactic:
rw [ModelWithCorners.left_inv]

Premises used: ModelWithCorners.left_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ u ∈ 𝓝 x

Tactic:
u_open.mem_nhds xu

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ u ∈ 𝓝 x

Tactic:
exact u_open.mem_nhds xu

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))

Tactic:
have : u ∈ 𝓝 (I.symm (I x)) := by
      rw [ModelWithCorners.left_inv]
      exact u_open.mem_nhds xu
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this_1 :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
this : u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))
⊢ (↑I.symm : E → H) ⁻¹' u ∈ 𝓝 ((↑I : H → E) x)

Tactic:
apply ContinuousAt.preimage_mem_nhds I.continuous_symm.continuousAt this

Premises used: ContinuousAt.preimage_mem_nhds, Continuous.continuousAt, ModelWithCorners.continuous_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h : ContDiffWithinAtProp I I' m f s x
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)

Tactic:
rw [ContDiffWithinAtProp] at h ⊢

Premises used: ContDiffWithinAtProp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
⊢ (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
⊢ (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
have : I x = (I ∘ e.symm ∘ I.symm) (I (e x)) := by simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))

Tactic:
rw [this] at h
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
h₁ :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
⊢ (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
rw [this] at h
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
⊢ (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
⊢ (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)

Tactic:
have : I (e x) ∈ I.symm ⁻¹' e.target ∩ range I := by simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
have := (mem_groupoid_of_pregroupoid.2 he).2.contDiffWithinAt this
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
⊢ ContDiffWithinAt 𝕜 m
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
(h.comp_inter _ (this.of_le hmn)).mono_of_mem_nhdsWithin _

Premises used: ContDiffWithinAt.of_le, ContDiffWithinAt.mono_of_mem_nhdsWithin, ContDiffWithinAt.comp_inter
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
h₁ :
  (↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)
convert_2 :
  (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E) ∩
      (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ∈
    𝓝[(↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)] (↑I : H → E) ((↑e : H → H) x)
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
convert! (h.comp_inter _ (this.of_le hmn)).mono_of_mem_nhdsWithin _ using 1

Premises used: ContDiffWithinAt.of_le, ContDiffWithinAt.mono_of_mem_nhdsWithin, ContDiffWithinAt.comp_inter
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
h₁ :
  ∀ (y : E),
    ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H)) y =
      (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) y
⊢ (↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)

Tactic:
ext y
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
y : E
⊢ ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H)) y =
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) y

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
simp_rw : (↑I.symm : E → H) ((↑I : H → E) ((↑e : H → H) x)) ∈ e.target
simp_rw₁ : (↑e : H → H) x ∈ e.target
⊢ (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target

Tactic:
simp_rw [mem_preimage, I.left_inv, e.mapsTo hx]

Premises used: OpenPartialHomeomorph.mapsTo, ModelWithCorners.left_inv, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
convert_2 :
  (↑I.symm : E → H) ⁻¹' e.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ⊆
    (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E) ∩
      (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
⊢ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E) ∩
      (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ∈
    𝓝[(↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)] (↑I : H → E) ((↑e : H → H) x)

Tactic:
refine mem_nhdsWithin.mpr
      ⟨I.symm ⁻¹' e.target, e.open_target.preimage I.continuous_symm, by
        simp_rw [mem_preimage, I.left_inv, e.mapsTo hx], ?_⟩

Premises used: Iff.mpr, PartialEquiv.target, mem_nhdsWithin, ModelWithCorners.continuous_symm, Set.preimage, And.intro, Exists.intro, ModelWithCorners.symm, PartialEquiv.toFun, OpenPartialHomeomorph.open_target, IsOpen.preimage, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
convert_2 convert_2₁ convert_2₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) →
      my_y ∈
        (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E) ∩
          (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
convert_2₃ convert_2₄ :
  ∀ ⦃my_y : E⦄,
    (↑I.symm : E → H) my_y ∈ e.target ∧ (↑e.symm : H → H) ((↑I.symm : E → H) my_y) ∈ s ∧ my_y ∈ range (↑I : H → E) →
      my_y ∈
        (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E) ∩
          (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
⊢ (↑I.symm : E → H) ⁻¹' e.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ⊆
    (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E) ∩
      (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
h₁ :
  ∀ y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E),
    ((↑I' : H' → E') ∘ g ∘ (↑I.symm : E → H)) y = ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y
hx₁ :
  ((↑I' : H' → E') ∘ g ∘ (↑I.symm : E → H)) ((↑I : H → E) x) =
    ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x)
⊢ ContDiffWithinAtProp I I' m g s x

Tactic:
apply hf.congr

Premises used: ContDiffWithinAt.congr