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
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)

Tactic:
simp only [mfld_simps] at hy
-- 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
y : E
hy : (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)
⊢ ((↑I' : H' → E') ∘ g ∘ (↑I.symm : E → H)) y = ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y

Tactic:
simp only [h, hy, 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 g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
⊢ ((↑I' : H' → E') ∘ g ∘ (↑I.symm : E → H)) ((↑I : H → E) x) =
    ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')

Tactic:
have A : (I' ∘ f ∘ I.symm) (I x) ∈ I'.symm ⁻¹' e'.source ∩ 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
⊢ ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))

Tactic:
have := (mem_groupoid_of_pregroupoid.2 he').1.contDiffWithinAt A
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
⊢ ContDiffWithinAt 𝕜 m
    (((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
(this.of_le hmn).comp _ h _

Premises used: ContDiffWithinAt.of_le, ContDiffWithinAt.comp
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
h₁ :
  (↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)
convert! :
  MapsTo ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
convert! (this.of_le hmn).comp _ h _

Premises used: ContDiffWithinAt.of_le, ContDiffWithinAt.comp
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
h₁ :
  ∀ (y : E),
    ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H)) y =
      (((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y
⊢ (↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
y : E
⊢ ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H)) y =
    (((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)

Tactic:
simp only [mfld_simps] at hy
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
y : E
hy : (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)
⊢ ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y ∈ (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')

Tactic:
simpa only [hy, mfld_simps] using hs hy.1

Premises used: And.left
-- 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 : ℕ∞ω
⊢ (contDiffGroupoid n I).LocalInvariantProp (contDiffGroupoid n I') (ContDiffWithinAtProp I I' n)

Tactic:
contDiffWithinAt_localInvariantProp_of_le n n le_rfl

Premises used: le_rfl, contDiffWithinAt_localInvariantProp_of_le
-- 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 : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ContDiffWithinAtProp I I' n f t x

Tactic:
h.mono_of_mem_nhdsWithin ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, 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 : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
refine : (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x
⊢ ContDiffWithinAtProp I I' n f t x

Tactic:
refine h.mono_of_mem_nhdsWithin ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin
-- 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 : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x

Tactic:
inter_mem ?_ (mem_of_superset self_mem_nhdsWithin inter_subset_right)

Premises used: Filter.inter_mem, self_mem_nhdsWithin, Set.inter_subset_right, Filter.mem_of_superset
-- 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 : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
refine : (↑I.symm : E → H) ⁻¹' s ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x
⊢ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x

Tactic:
refine inter_mem ?_ (mem_of_superset self_mem_nhdsWithin inter_subset_right)

Premises used: Filter.inter_mem, self_mem_nhdsWithin, Set.inter_subset_right, Filter.mem_of_superset
-- 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 : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
rwa : s ∈ map (↑I.symm : E → H) (𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x)
rwa₁ : s ∈ map (↑I.symm : E → H) (𝓝[(↑I : H → E) '' t] (↑I : H → E) x)
rwa₂ rwa₃ rwa₄ rwa₅ : s ∈ 𝓝[t] x
⊢ (↑I.symm : E → H) ⁻¹' s ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x

Tactic:
rwa [← Filter.mem_map, ← I.image_eq, I.symm_map_nhdsWithin_image]

Premises used: ModelWithCorners.image_eq, ModelWithCorners.symm_map_nhdsWithin_image, Filter.mem_map
-- 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
n : ℕ∞ω
x : H
simp : ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
⊢ ContDiffWithinAtProp I I n id univ x

Tactic:
simp only [ContDiffWithinAtProp, id_comp, preimage_univ, univ_inter]

Premises used: Set.univ_inter, Set.preimage_univ, ContDiffWithinAtProp, Function.id_comp
-- 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
n : ℕ∞ω
x : H
⊢ ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
have : ContDiffWithinAt 𝕜 n id (range I) (I x) := contDiff_id.contDiffAt.contDiffWithinAt
-- 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
n : ℕ∞ω
x : H
this : ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
this.congr (fun y hy => ?_) ?_

Premises used: ContDiffWithinAt.congr
-- 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
n : ℕ∞ω
x : H
this : ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)
refine_1 : ∀ (y : E) (hy : y ∈ range (↑I : H → E)), ((↑I : H → E) ∘ (↑I.symm : E → H)) y = id y
refine_2 : ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = id ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
refine this.congr (fun y hy => ?_) ?_

Premises used: ContDiffWithinAt.congr
-- 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
n : ℕ∞ω
x : H
this : ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)
y : E
hy : y ∈ range (↑I : H → E)
⊢ ((↑I : H → E) ∘ (↑I.symm : E → H)) y = id y

Tactic:
simp only [ModelWithCorners.right_inv I hy, mfld_simps]

Premises used: ModelWithCorners.right_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
n : ℕ∞ω
x : H
this : ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)
⊢ ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = id ((↑I : H → E) x)

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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f : M → M'
x : M
rw :
  ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n
        ((↑I' : H' → E') ∘
          ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘
            (↑I.symm : E → H))
        (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) ↔
    ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousAt f x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [ContDiffWithinAtProp, preimage_univ, univ_inter]

Premises used: Set.univ_inter, Set.preimage_univ, 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f : M → M'
x : M
⊢ ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n
        ((↑I' : H' → E') ∘
          ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘
            (↑I.symm : E → H))
        (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) ↔
    ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
rfl