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 : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
x : M
hx : x ∈ s ∪ t
inl : ∀ (hx : x ∈ s), ContMDiffWithinAt I I' n f (s ∪ t) x
inr : ∀ (hx : x ∈ t), ContMDiffWithinAt I I' n f (s ∪ t) x
⊢ ContMDiffWithinAt I I' n f (s ∪ t) x

Tactic:
obtain (hx | hx) := 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'
f : M → M'
n : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
x : M
hx : x ∈ s
⊢ ContMDiffWithinAt I I' n f (s ∪ t) x

Tactic:
(hf x hx).contMDiffAt (hs.mem_nhds hx) |>.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, ContMDiffWithinAt.contMDiffAt, 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'
f : M → M'
n : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
x : M
hx : x ∈ s
⊢ ContMDiffWithinAt I I' n f (s ∪ t) x

Tactic:
exact (hf x hx).contMDiffAt (hs.mem_nhds hx) |>.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, ContMDiffWithinAt.contMDiffAt, 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'
f : M → M'
n : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
x : M
hx : x ∈ t
⊢ ContMDiffWithinAt I I' n f (s ∪ t) x

Tactic:
(hf' x hx).contMDiffAt (ht.mem_nhds hx) |>.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, ContMDiffWithinAt.contMDiffAt, 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'
f : M → M'
n : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
x : M
hx : x ∈ t
⊢ ContMDiffWithinAt I I' n f (s ∪ t) x

Tactic:
exact (hf' x hx).contMDiffAt (ht.mem_nhds hx) |>.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, ContMDiffWithinAt.contMDiffAt, 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'
f : M → M'
n : ℕ∞ω
s t : Set M
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
⊢ ContMDiffOn I I' n f (s ∪ t) ↔ ContMDiffOn I I' n f s ∧ ContMDiffOn I I' n f t

Tactic:
⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right⟩,
   fun ⟨hfs, hft⟩ ↦ ContMDiffOn.union_of_isOpen hfs hft hs ht⟩

Premises used: Set.subset_union_right, _private.0.contMDiffOn_union_iff_of_isOpen.match_1, Set.subset_union_left, ContMDiffOn.mono, And.intro, Iff.intro, Union.union, ContMDiffOn.union_of_isOpen, ContMDiffOn
-- 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 : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hst : s ∪ t = univ
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
rw : ContMDiffOn I I' n f (s ∪ t)
⊢ ContMDiff I I' n f

Tactic:
rw [← contMDiffOn_univ, ← hst]

Premises used: contMDiffOn_univ
-- 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 : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hst : s ∪ t = univ
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
⊢ ContMDiffOn I I' n f (s ∪ t)

Tactic:
hf.union_of_isOpen hf' hs ht

Premises used: ContMDiffOn.union_of_isOpen
-- 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 : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hst : s ∪ t = univ
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
⊢ ContMDiffOn I I' n f (s ∪ t)

Tactic:
exact hf.union_of_isOpen hf' hs ht

Premises used: ContMDiffOn.union_of_isOpen
-- 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 : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
x : M
i : ι
hxsi : Membership.mem (γ := Set M) ((fun (i : ι) ↦ s i) i) x
⊢ ContMDiffWithinAt I I' n f (⋃ (i : ι), s i) x

Tactic:
(hf i).contMDiffAt ((hs i).mem_nhds hxsi) |>.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, ContMDiffOn.contMDiffAt, 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'
f : M → M'
n : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
x : M
i : ι
hxsi : Membership.mem (γ := Set M) ((fun (i : ι) ↦ s i) i) x
⊢ ContMDiffWithinAt I I' n f (⋃ (i : ι), s i) x

Tactic:
exact (hf i).contMDiffAt ((hs i).mem_nhds hxsi) |>.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, ContMDiffOn.contMDiffAt, 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'
f : M → M'
n : ℕ∞ω
ι : Type u_11
s : ι → Set M
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
⊢ ContMDiffOn I I' n f (⋃ (i : ι), s i) ↔ ∀ (i : ι), ContMDiffOn I I' n f (s i)

Tactic:
⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a,
   fun h ↦ ContMDiffOn.iUnion_of_isOpen h hs⟩

Premises used: Set.subset_iUnion_of_subset, ContMDiffOn.mono, Iff.intro, ContMDiffOn.iUnion_of_isOpen
-- 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 : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
hs' : Eq.{u_4 + 1} (α := Set M) (⋃ (i : ι), s i) univ
rw : ContMDiffOn I I' n f (⋃ (i : ι), s i)
⊢ ContMDiff I I' n f

Tactic:
rw [← contMDiffOn_univ, ← hs']

Premises used: contMDiffOn_univ
-- 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 : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
hs' : Eq.{u_4 + 1} (α := Set M) (⋃ (i : ι), s i) univ
⊢ ContMDiffOn I I' n f (⋃ (i : ι), s i)

Tactic:
ContMDiffOn.iUnion_of_isOpen hf hs

Premises used: ContMDiffOn.iUnion_of_isOpen
-- 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 : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
hs' : Eq.{u_4 + 1} (α := Set M) (⋃ (i : ι), s i) univ
⊢ ContMDiffOn I I' n f (⋃ (i : ι), s i)

Tactic:
exact ContMDiffOn.iUnion_of_isOpen hf hs

Premises used: ContMDiffOn.iUnion_of_isOpen
-- 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 : ℕ∞ω
U : Opens M
f : M → M'
x : ↥U
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') n (fun (x : ↥U) ↦ f (↑x : M)) x ↔
    ContMDiffAt I I' n f (↑x : M)

Tactic:
((contDiffWithinAt_localInvariantProp n).liftPropAt_iff_comp_subtype_val _ _).symm

Premises used: ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, ContMDiffAt, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val, ChartedSpace.LiftPropAt, Iff.symm
-- 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
inst_5 : ChartedSpace H M
n : ℕ∞ω
U : Opens M
⊢ ContMDiff.{u_1, u_2, u_3, u_4, u_2, u_3, u_4} I (M := ↥U) I n (Subtype.val (p := fun (x : M) ↦ x ∈ U))

Tactic:
fun _ ↦ contMDiffAt_subtype_iff.mpr contMDiffAt_id

Premises used: Iff.mpr, ContMDiff, contMDiffAt_id, contMDiffAt_subtype_iff
-- 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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x : M
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) x

Tactic:
contMDiff_of_mulTSupport (fun x h ↦ ?_) _

Premises used: contMDiff_of_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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x : M
refine :
  ∀ (x : M) (h : x ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)),
    ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) x
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) x

Tactic:
refine contMDiff_of_mulTSupport (fun x h ↦ ?_) _

Premises used: contMDiff_of_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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 x : M
h : x ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
⊢ x ∈ U

Tactic:
Subtype.coe_image_subset _ _
    (supp.mulTSupport_extend_one_subset continuous_subtype_val h)

Premises used: HasCompactMulSupport.mulTSupport_extend_one_subset, continuous_subtype_val, Subtype.coe_image_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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 x : M
h : x ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
lift :
  ∀ (x : ↥U) (h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)),
    ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) (↑x : M)
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) x

Tactic:
lift x to U using Subtype.coe_image_subset _ _
    (supp.mulTSupport_extend_one_subset continuous_subtype_val h)

Premises used: HasCompactMulSupport.mulTSupport_extend_one_subset, continuous_subtype_val, Subtype.coe_image_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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
rw :
  ContMDiffAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') n
    (fun (x : ↥U) ↦ extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 (↑x : M)) x
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1) (↑x : M)

Tactic:
rw [← contMDiffAt_subtype_iff]

Premises used: contMDiffAt_subtype_iff
-- 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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
simp_rw :
  ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') n
    (fun (x : ↥U) ↦ extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 (↑x : M)) x

Tactic:
simp_rw [← comp_def]

Premises used: Function.comp_def
-- 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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
rw : ContMDiffAt I I' n f x
⊢ ContMDiffAt I I' n (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1 ∘ Subtype.val (p := fun (x : M) ↦ x ∈ U)) x

Tactic:
rw [extend_comp Subtype.val_injective]

Premises used: Subtype.val_injective, Function.extend_comp
-- 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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
⊢ ContMDiffAt I I' n f x

Tactic:
diff.contMDiffAt

Premises used: 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'
inst_11 : T2Space M
inst_12 : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x_1 : M
x : ↥U
h : (↑x : M) ∈ mulTSupport (extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) f 1)
⊢ ContMDiffAt I I' n f x

Tactic:
exact diff.contMDiffAt

Premises used: 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
inst_5 : ChartedSpace H M
n : ℕ∞ω
U V : Opens M
h : U ≤ V
⊢ ContMDiff I I n (Opens.inclusion h)

Tactic:
fun _ ↦
  (contDiffWithinAt_localInvariantProp n).liftProp_inclusion (contDiffWithinAtProp_id ·) _ _

Premises used: ContMDiffWithinAt, ContMDiff, contDiffWithinAtProp_id, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftProp_inclusion, ContMDiffAt, ChartedSpace.LiftPropAt