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
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'
f : M → M'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
refine : ContMDiffAt I I' n f x → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'
⊢ ContMDiffAt I I' n f x ↔ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
refine ⟨?_, fun h => h.self_of_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
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'
f : M → M'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
rw : (∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u) → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'
⊢ ContMDiffAt I I' n f x → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
rw [contMDiffAt_iff_contMDiffOn_nhds hn]

Premises used: contMDiffAt_iff_contMDiffOn_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
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'
f : M → M'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
⊢ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
(eventually_mem_nhds_iff.mpr hu).mono fun x' hx' => ?_

Premises used: Iff.mpr, eventually_mem_nhds_iff, Filter.Eventually.mono
-- 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'
f : M → M'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
refine : ∀ (x' : M) (hx' : u ∈ 𝓝 x'), ContMDiffAt I I' n f x'
⊢ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
refine (eventually_mem_nhds_iff.mpr hu).mono fun x' hx' => ?_

Premises used: Iff.mpr, eventually_mem_nhds_iff, Filter.Eventually.mono
-- 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'
f : M → M'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
x' : M
hx' : u ∈ 𝓝 x'
⊢ ContMDiffAt I I' n f x'

Tactic:
(h x' <| mem_of_mem_nhds hx').contMDiffAt hx'

Premises used: ContMDiffWithinAt.contMDiffAt, mem_of_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
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'
f : M → M'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
x' : M
hx' : u ∈ 𝓝 x'
⊢ ContMDiffAt I I' n f x'

Tactic:
exact (h x' <| mem_of_mem_nhds hx').contMDiffAt hx'

Premises used: ContMDiffWithinAt.contMDiffAt, mem_of_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
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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffWithinAt I I' n f s x ↔ ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'

Tactic:
⟨?_, fun h ↦ mem_of_mem_nhdsWithin (mem_insert x s) h⟩

Premises used: mem_of_mem_nhdsWithin, Iff.intro, Set.mem_insert
-- 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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
refine : ContMDiffWithinAt I I' n f s x → ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
⊢ ContMDiffWithinAt I I' n f s x ↔ ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'

Tactic:
refine ⟨?_, fun h ↦ mem_of_mem_nhdsWithin (mem_insert x s) 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
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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
rw : (∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u) → ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
⊢ ContMDiffWithinAt I I' n f s x → ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'

Tactic:
rw [contMDiffWithinAt_iff_contMDiffOn_nhds hn]

Premises used: contMDiffWithinAt_iff_contMDiffOn_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
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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
h₁ : ∀ (x' : M) (h'x' : x' ∈ u) (hx' : u ∈ 𝓝[insert x s] x'), ContMDiffWithinAt I I' n f s x'
⊢ ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'

Tactic:
filter_upwards [hu, eventually_mem_nhdsWithin_iff.mpr hu] with x' h'x' hx'

Premises used: Iff.mpr, eventually_mem_nhdsWithin_iff
-- 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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
x' : M
h'x' : x' ∈ u
hx' : u ∈ 𝓝[insert x s] x'
h₁ : u ∈ 𝓝[s] x'
⊢ ContMDiffWithinAt I I' n f s x'

Tactic:
apply (h x' h'x').mono_of_mem_nhdsWithin

Premises used: ContMDiffWithinAt.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
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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
x' : M
h'x' : x' ∈ u
hx' : u ∈ 𝓝[insert x s] x'
⊢ u ∈ 𝓝[s] x'

Tactic:
nhdsWithin_mono _ (subset_insert x s) hx'

Premises used: Set.subset_insert, nhdsWithin_mono
-- 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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
x' : M
h'x' : x' ∈ u
hx' : u ∈ 𝓝[insert x s] x'
⊢ u ∈ 𝓝[s] x'

Tactic:
exact nhdsWithin_mono _ (subset_insert x s) hx'

Premises used: Set.subset_insert, nhdsWithin_mono
-- 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'
f f₁ : M → M'
s : Set M
x : M
n : ℕ∞ω
h : ContMDiffWithinAt I I' n f s x
h₁ : ∀ y ∈ s, f₁ y = f y
hx : f₁ x = f x
⊢ ContMDiffWithinAt I I' n f₁ s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr h h₁ hx

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_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
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'
f f₁ : M → M'
s t : Set M
x : M
n : ℕ∞ω
h : ContMDiffWithinAt I I' n f s x
h₁ : ∀ y ∈ t, f₁ y = f y
hst : s ⊆ t
hxt : x ∈ t
⊢ ContMDiffWithinAt I I' n f₁ s x

Tactic:
h.congr (fun _y hy ↦ h₁ _ (hst hy)) (h₁ x hxt)

Premises used: ContMDiffWithinAt.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
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'
f f₁ : M → M'
s : Set M
x : M
n : ℕ∞ω
h₁ : ∀ y ∈ s, f₁ y = f y
hx : f₁ x = f x
⊢ ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff h₁ hx

Premises used: ContMDiffWithinAt, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff, contDiffWithinAt_localInvariantProp
-- 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'
f f₁ : M → M'
s : Set M
x : M
n : ℕ∞ω
h : ContMDiffWithinAt I I' n f s x
h₁ : ∀ y ∈ s, f₁ y = f y
hx : x ∈ s
⊢ ContMDiffWithinAt I I' n f₁ s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_mem h h₁ hx

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_mem
-- 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'
f f₁ : M → M'
s : Set M
x : M
n : ℕ∞ω
h₁ : ∀ y ∈ s, f₁ y = f y
hx : x ∈ s
⊢ ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff_of_mem h₁ hx

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_mem
-- 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'
f f₁ : M → M'
s : Set M
x : M
n : ℕ∞ω
h : ContMDiffWithinAt I I' n f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ContMDiffWithinAt I I' n f₁ s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_eventuallyEq h h₁ hx

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq
-- 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'
f f₁ : M → M'
s : Set M
x : M
n : ℕ∞ω
h : ContMDiffWithinAt I I' n f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ ContMDiffWithinAt I I' n f₁ s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_eventuallyEq_of_mem h h₁ hx

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq_of_mem
-- 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'
f f₁ : M → M'
s : Set M
x : M
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff_of_eventuallyEq h₁ hx

Premises used: ContMDiffWithinAt, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq, contDiffWithinAt_localInvariantProp
-- 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'
f f₁ : M → M'
x : M
n : ℕ∞ω
h : ContMDiffAt I I' n f x
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ ContMDiffAt I I' n f₁ x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropAt_congr_of_eventuallyEq h h₁

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropAt_congr_of_eventuallyEq, ContMDiffAt, ChartedSpace.LiftPropAt
-- 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'
f f₁ : M → M'
x : M
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ ContMDiffAt I I' n f₁ x ↔ ContMDiffAt I I' n f x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropAt_congr_iff_of_eventuallyEq h₁

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq, ContMDiffAt, ChartedSpace.LiftPropAt
-- 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'
f f₁ : M → M'
s : Set M
n : ℕ∞ω
h : ContMDiffOn I I' n f s
h₁ : ∀ y ∈ s, f₁ y = f y
⊢ ContMDiffOn I I' n f₁ s

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropOn_congr h h₁

Premises used: ContMDiffWithinAt, ChartedSpace.LiftPropOn, StructureGroupoid.LocalInvariantProp.liftPropOn_congr, contDiffWithinAt_localInvariantProp, ContMDiffOn
-- 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'
f f₁ : M → M'
s : Set M
n : ℕ∞ω
h₁ : ∀ y ∈ s, f₁ y = f y
⊢ ContMDiffOn I I' n f₁ s ↔ ContMDiffOn I I' n f s

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropOn_congr_iff h₁

Premises used: ContMDiffWithinAt, ChartedSpace.LiftPropOn, contDiffWithinAt_localInvariantProp, ContMDiffOn, StructureGroupoid.LocalInvariantProp.liftPropOn_congr_iff
-- 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'
f f₁ : M → M'
s s₁ : Set M
n : ℕ∞ω
hf : ContMDiffOn I I' n f s
h₁ : ∀ y ∈ s₁, f₁ y = f y
hs : s₁ ⊆ s
⊢ ContMDiffOn I I' n f₁ s₁

Tactic:
(hf.mono hs).congr h₁

Premises used: ContMDiffOn.mono, ContMDiffOn.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
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'
f f₁ : M → M'
n : ℕ∞ω
h : ContMDiff I I' n f
h₁ : ∀ (y : M), f₁ y = f y
rw : ∀ (h : ContMDiffOn I I' n f univ) (h₁ : ∀ (y : M), f₁ y = f y), ContMDiffOn I I' n f₁ univ
⊢ ContMDiff I I' n f₁

Tactic:
rw [← contMDiffOn_univ] at h ⊢

Premises used: contMDiffOn_univ
-- 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'
f f₁ : M → M'
n : ℕ∞ω
h : ContMDiffOn I I' n f univ
h₁ : ∀ (y : M), f₁ y = f y
⊢ ContMDiffOn I I' n f₁ univ

Tactic:
(contMDiffOn_congr fun y _ ↦ h₁ y).mpr h

Premises used: Iff.mpr, contMDiffOn_congr