awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
n : ℕ∞ω
inst_11 : Subsingleton M'
x : M
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') n (fun (x_1 : M) ↦ f x) x

Tactic:
exact contMDiffAt_const

Premises used: contMDiffAt_const
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
n : ℕ∞ω
inst_11 : Subsingleton M'
⊢ ContMDiffAt I I' n f x

Tactic:
contMDiff_of_subsingleton.contMDiffAt

Premises used: ContMDiff.contMDiffAt, contMDiff_of_subsingleton
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : Subsingleton M'
⊢ ContMDiffWithinAt I I' n f s x

Tactic:
contMDiffAt_of_subsingleton.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, contMDiffAt_of_subsingleton
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : Subsingleton M'
⊢ ContMDiffOn I I' n f s

Tactic:
contMDiff_of_subsingleton.contMDiffOn

Premises used: ContMDiff.contMDiffOn, contMDiff_of_subsingleton
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
n : ℕ∞ω
inst_11 : DiscreteTopology M
x : M
apply : f =ᶠ[𝓝 x] fun (x_1 : M) ↦ f x
⊢ ContMDiffAt I I' n f x

Tactic:
apply contMDiff_const (c := f x).contMDiffAt.congr_of_eventuallyEq

Premises used: contMDiff_const, ContMDiffAt.congr_of_eventuallyEq, ContMDiff.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
n : ℕ∞ω
inst_11 : DiscreteTopology M
x : M
⊢ f =ᶠ[𝓝 x] fun (x_1 : M) ↦ f x

Tactic:
simp [EventuallyEq]

Premises used: Filter.EventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
inst_11 : One M'
f : M → M'
hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x
x : M
pos : ∀ (hx : x ∈ mulTSupport f), ContMDiffAt I I' n f x
neg : ∀ (hx : x ∉ mulTSupport f), ContMDiffAt I I' n f x
⊢ ContMDiffAt I I' n f x

Tactic:
by_cases hx : x ∈ mulTSupport f

Premises used: mulTSupport
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
inst_11 : One M'
f : M → M'
hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x
x : M
hx : x ∈ mulTSupport f
⊢ ContMDiffAt I I' n f x

Tactic:
hf x hx
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
inst_11 : One M'
f : M → M'
hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x
x : M
hx : x ∈ mulTSupport f
⊢ ContMDiffAt I I' n f x

Tactic:
exact hf x hx
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
inst_11 : One M'
f : M → M'
hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x
x : M
hx : x ∉ mulTSupport f
⊢ ContMDiffAt I I' n f x

Tactic:
ContMDiffAt.congr_of_eventuallyEq contMDiffAt_const
      (notMem_mulTSupport_iff_eventuallyEq.1 hx)

Premises used: contMDiffAt_const, ContMDiffAt.congr_of_eventuallyEq, Iff.mp, notMem_mulTSupport_iff_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
inst_11 : One M'
f : M → M'
hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x
x : M
hx : x ∉ mulTSupport f
⊢ ContMDiffAt I I' n f x

Tactic:
exact ContMDiffAt.congr_of_eventuallyEq contMDiffAt_const
      (notMem_mulTSupport_iff_eventuallyEq.1 hx)

Premises used: contMDiffAt_const, ContMDiffAt.congr_of_eventuallyEq, Iff.mp, notMem_mulTSupport_iff_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
inst_11 : One M'
x : M
hx : x ∉ mulTSupport f
n : ℕ∞ω
s : Set M
⊢ ContMDiffWithinAt I I' n f s x

Tactic:
apply contMDiffWithinAt_const.congr_of_eventuallyEq
    (eventually_nhdsWithin_of_eventually_nhds <| notMem_mulTSupport_iff_eventuallyEq.mp hx)
    (image_eq_one_of_notMem_mulTSupport hx)

Premises used: contMDiffWithinAt_const, eventually_nhdsWithin_of_eventually_nhds, image_eq_one_of_notMem_mulTSupport, Iff.mp, ContMDiffWithinAt.congr_of_eventuallyEq, notMem_mulTSupport_iff_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
inst_11 : One M'
x : M
hx : x ∉ mulTSupport f
n : ℕ∞ω
⊢ ContMDiffAt I I' n f x

Tactic:
contMDiffWithinAt_of_notMem_mulTSupport hx n univ

Premises used: Set.univ, ContMDiffAt, contMDiffWithinAt_of_notMem_mulTSupport
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
pos : ∀ (hx : x ∈ interior s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
neg : ∀ (hx : x ∉ interior s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x

Tactic:
by_cases hx : x ∈ interior s

Premises used: interior
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
pos : s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x

Tactic:
apply (hf x).congr_of_eventuallyEq

Premises used: ContMDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
h : ∀ (y : M) (hy : y ∈ interior s), s.piecewise (β := fun (a : M) ↦ M') f g y = f y
⊢ s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f

Tactic:
filter_upwards [isOpen_interior.mem_nhds hx] with y hy

Premises used: isOpen_interior, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
y : M
hy : y ∈ interior s
h : y ∈ s
⊢ s.piecewise (β := fun (a : M) ↦ M') f g y = f y

Tactic:
rw [piecewise_eq_of_mem]

Premises used: Set.piecewise_eq_of_mem
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
y : M
hy : y ∈ interior s
⊢ y ∈ s

Tactic:
apply interior_subset hy

Premises used: interior_subset
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
pos : ∀ (h'x : x ∈ closure[inst_4] s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
neg : ∀ (h'x : x ∉ closure[inst_4] s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x

Tactic:
by_cases h'x : x ∈ closure s

Premises used: closure
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∈ closure[inst_4] s
⊢ x ∈ frontier s

Tactic:
have : x ∈ frontier s := ⟨h'x, hx⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∈ closure[inst_4] s
this : x ∈ frontier s
pos : s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x

Tactic:
apply (hf x).congr_of_eventuallyEq

Premises used: ContMDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∈ closure[inst_4] s
this : x ∈ frontier s
h : ∀ (y : M) (hy : f y = g y), s.piecewise (β := fun (a : M) ↦ M') f g y = f y
⊢ s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f

Tactic:
filter_upwards [hfg x this] with y hy
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∈ closure[inst_4] s
this : x ∈ frontier s
y : M
hy : f y = g y
⊢ s.piecewise (β := fun (a : M) ↦ M') f g y = f y

Tactic:
simp [Set.piecewise, hy]

Premises used: Set.piecewise
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst_4] s
neg : s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] g
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x

Tactic:
apply (hg x).congr_of_eventuallyEq

Premises used: ContMDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst_4] s
h : ∀ (y : M) (hy : y ∈ (closure[inst_4] s)ᶜ), s.piecewise (β := fun (a : M) ↦ M') f g y = g y
⊢ s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] g

Tactic:
filter_upwards [isClosed_closure.isOpen_compl.mem_nhds h'x] with y hy

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst_4] s
y : M
hy : y ∈ (closure[inst_4] s)ᶜ
h : y ∉ s
⊢ s.piecewise (β := fun (a : M) ↦ M') f g y = g y

Tactic:
rw [piecewise_eq_of_notMem]

Premises used: Set.piecewise_eq_of_notMem
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst_4] s
y : M
hy : y ∈ (closure[inst_4] s)ᶜ
h : ∀ (hy : y ∈ s), y ∉ (closure[inst_4] s)ᶜ
⊢ y ∉ s

Tactic:
contrapose hy
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst_11 : DecidablePred fun (x : M) ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst_4] s
y : M
hy : y ∈ s
⊢ y ∉ (closure[inst_4] s)ᶜ

Tactic:
simpa using subset_closure hy

Premises used: subset_closure
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
n : ℕ∞ω
E : Type u_11
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_12
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_13
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
f g : ℝ → M
s : ℝ
hf : ContMDiff 𝓘(ℝ, ℝ) I n f
hg : ContMDiff 𝓘(ℝ, ℝ) I n g
hfg : f =ᶠ[𝓝 s] g
⊢ ∀ x ∈ frontier (Iic s), f =ᶠ[𝓝 x] g

Tactic:
simpa using hfg