awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
s : Set M
n : ℕ∞ω
f : M → M
hf : ContMDiffOn I I n f s
hmaps : MapsTo f s s
k : ℕ
zero : ContMDiffOn I I n f^[0] s
⊢ ContMDiffOn I I n f^[k] s
have succ : ∀ (k : ℕ) (h : ContMDiffOn I I n f^[k] s), ContMDiffOn I I n f^[k + 1] s
Tactic: induction k with
  | zero => simpa using contMDiffOn_id
  | succ k h => simpa using h.comp hf hmaps
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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 : ℕ∞ω
c : 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 : M) ↦ c) x
have refine : ContDiffWithinAtProp I I' n
  ((↑(chartAt H' c) : M' → H') ∘ (fun (x : M) ↦ c) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' univ) ((↑(chartAt H x) : M → H) x)
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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 : ℕ∞ω
c : M'
x : M
⊢ ContDiffWithinAtProp I I' n
    ((↑(chartAt H' c) : M' → H') ∘ (fun (x : M) ↦ c) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' univ) ((↑(chartAt H x) : M → H) x)
have simp : ContDiffWithinAt.{u_1, u_2, u_5} 𝕜 (F := E') n (fun (x : E) ↦ (↑I' : H' → E') ((↑(chartAt H' c) : M' → H') c))
  ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' univ ∩ range (↑I : H → E))
  ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: simp only [ContDiffWithinAtProp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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 I I' n f x
have rw : 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: rw [Subsingleton.elim f fun _ => (f x)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n f x
have apply : f =ᶠ[𝓝 x] fun (x_1 : M) ↦ f x
Tactic: apply contMDiff_const (c := f x).contMDiffAt.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n f x
have pos : ∀ (hx : x ∈ mulTSupport f), ContMDiffAt I I' n f x
Tactic: by_cases hx : x ∈ mulTSupport f
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n f x
have neg : ∀ (hx : x ∉ mulTSupport f), ContMDiffAt I I' n f x
Tactic: by_cases hx : x ∈ mulTSupport f
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have pos : ∀ (hx : x ∈ interior s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
Tactic: by_cases hx : x ∈ interior s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have neg : ∀ (hx : x ∉ interior s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
Tactic: by_cases hx : x ∈ interior s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have pos : s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f
Tactic: apply (hf x).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f
have h : ∀ (y : M) (hy : y ∈ interior s), s.piecewise (β := fun (a : M) ↦ M') f g y = f y
Tactic: filter_upwards [isOpen_interior.mem_nhds hx] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ s.piecewise (β := fun (a : M) ↦ M') f g y = f y
have h : y ∈ s
Tactic: rw [piecewise_eq_of_mem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have pos : ∀ (h'x : x ∈ closure[inst_4] s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
Tactic: by_cases h'x : x ∈ closure s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have neg : ∀ (h'x : x ∉ closure[inst_4] s), ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
Tactic: by_cases h'x : x ∈ closure s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have this : x ∈ frontier s
Tactic: have : x ∈ frontier s := ⟨h'x, hx⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have pos : s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f
Tactic: apply (hf x).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] f
have h : ∀ (y : M) (hy : f y = g y), s.piecewise (β := fun (a : M) ↦ M') f g y = f y
Tactic: filter_upwards [hfg x this] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffAt I I' n (s.piecewise (β := fun (a : M) ↦ M') f g) x
have neg : s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] g
Tactic: apply (hg x).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ s.piecewise (β := fun (a : M) ↦ M') f g =ᶠ[𝓝 x] g
have h : ∀ (y : M) (hy : y ∈ (closure[inst_4] s)ᶜ), s.piecewise (β := fun (a : M) ↦ M') f g y = g y
Tactic: filter_upwards [isClosed_closure.isOpen_compl.mem_nhds h'x] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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)ᶜ
⊢ s.piecewise (β := fun (a : M) ↦ M') f g y = g y
have h : y ∉ s
Tactic: rw [piecewise_eq_of_notMem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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)ᶜ
⊢ y ∉ s
have h : ∀ (hy : y ∈ s), y ∉ (closure[inst_4] s)ᶜ
Tactic: contrapose hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffWithinAt I I' n f (s ∪ t) x
have inl : ∀ (hx : x ∈ s), ContMDiffWithinAt I I' n f (s ∪ t) x
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffWithinAt I I' n f (s ∪ t) x
have inr : ∀ (hx : x ∈ t), ContMDiffWithinAt I I' n f (s ∪ t) x
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiff I I' n f
have rw : ContMDiffOn I I' n f (s ∪ t)
Tactic: rw [← contMDiffOn_univ, ← hst]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiff I I' n f
have rw : ContMDiffOn I I' n f (⋃ (i : ι), s i)
Tactic: rw [← contMDiffOn_univ, ← hs']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
have 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
Tactic: refine contMDiff_of_mulTSupport (fun x h ↦ ?_) _