awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
x : M
n : WithTop ℕ∞
g : N → N'
y : N
hf : ContMDiffAt I I' n f x
hg : ContMDiffAt J J' n g y
simp :
  ∀ (hf : ContMDiffWithinAt I I' n f univ x) (hg : ContMDiffWithinAt J J' n g univ y),
    ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (SProd.sprod (α := Set M) (β := Set N) univ univ) (x, y)
⊢ ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)

Tactic:
simp only [← contMDiffWithinAt_univ, ← univ_prod_univ] at *

Premises used: Set.univ_prod_univ, contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
x : M
n : WithTop ℕ∞
g : N → N'
y : N
hf : ContMDiffWithinAt I I' n f univ x
hg : ContMDiffWithinAt J J' n g univ y
⊢ ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (SProd.sprod (α := Set M) (β := Set N) univ univ) (x, y)

Tactic:
hf.prodMap hg

Premises used: ContMDiffWithinAt.prodMap
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
x : M
n : WithTop ℕ∞
g : N → N'
y : N
hf : ContMDiffWithinAt I I' n f univ x
hg : ContMDiffWithinAt J J' n g univ y
⊢ ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (SProd.sprod (α := Set M) (β := Set N) univ univ) (x, y)

Tactic:
exact hf.prodMap hg

Premises used: ContMDiffWithinAt.prodMap
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
s : Set M
n : WithTop ℕ∞
g : N → N'
r : Set N
hf : ContMDiffOn I I' n f s
hg : ContMDiffOn J J' n g r
⊢ ContMDiffOn (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r)

Tactic:
(hf.comp contMDiffOn_fst mapsTo_fst_prod).prodMk <| hg.comp contMDiffOn_snd mapsTo_snd_prod

Premises used: ContMDiffOn.prodMk, Set.Mem, Prod.map, contMDiffOn_fst, Set.mapsTo_fst_prod, Set.mapsTo_snd_prod, contMDiffOn_snd, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
n : WithTop ℕ∞
g : N → N'
hf : ContMDiff I I' n f
hg : ContMDiff J J' n g
p : M × N
⊢ ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) p

Tactic:
(hf p.1).prodMap' (hg p.2)

Premises used: Prod.fst, ContMDiffAt.prodMap', Prod.snd
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
n : WithTop ℕ∞
g : N → N'
hf : ContMDiff I I' n f
hg : ContMDiff J J' n g
p : M × N
⊢ ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) p

Tactic:
exact (hf p.1).prodMap' (hg p.2)

Premises used: Prod.fst, ContMDiffAt.prodMap', Prod.snd
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
x : M
n : WithTop ℕ∞
ι : Type u_16
inst_6 : Fintype ι
Fi : ι → Type u_17
inst_7 : (i : ι) → NormedAddCommGroup (Fi i)
inst_8 : (i : ι) → NormedSpace.{u_1, u_17} 𝕜 (Fi i)
φ : M → (i : ι) → Fi i
⊢ ContMDiffWithinAt I (E' := (i : ι) → Fi i) 𝓘(𝕜, (i : ι) → Fi i) n φ s x ↔
    ∀ (i : ι),
      ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_17, u_17, u_17} I (E' := Fi i) 𝓘(𝕜, Fi i) (M' := Fi i) n
        (fun (x : M) ↦ φ x i) s x

Tactic:
simp only [contMDiffWithinAt_iff, continuousWithinAt_pi, contDiffWithinAt_pi, forall_and,
    extChartAt_model_space_eq_id, Function.comp_def, PartialEquiv.refl_coe, id]

Premises used: id, contMDiffWithinAt_iff, Function.comp_def, extChartAt_model_space_eq_id, contDiffWithinAt_pi, continuousWithinAt_pi, PartialEquiv.refl_coe, forall_and
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : WithTop ℕ∞
ι : Type u_16
inst_6 : Fintype ι
Fi : ι → Type u_17
inst_7 : (i : ι) → NormedAddCommGroup (Fi i)
inst_8 : (i : ι) → NormedSpace.{u_1, u_17} 𝕜 (Fi i)
φ : M → (i : ι) → Fi i
⊢ ContMDiffOn I (E' := (i : ι) → Fi i) 𝓘(𝕜, (i : ι) → Fi i) n φ s ↔
    ∀ (i : ι),
      ContMDiffOn.{u_1, u_2, u_3, u_4, u_17, u_17, u_17} I (E' := Fi i) 𝓘(𝕜, Fi i) (M' := Fi i) n (fun (x : M) ↦ φ x i)
        s

Tactic:
⟨fun h i x hx => contMDiffWithinAt_pi_space.1 (h x hx) i, fun h x hx =>
    contMDiffWithinAt_pi_space.2 fun i => h i x hx⟩

Premises used: Iff.mpr, contMDiffWithinAt_pi_space, Iff.intro, Iff.mp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
x : M
n : WithTop ℕ∞
ι : Type u_16
inst_6 : Fintype ι
Fi : ι → Type u_17
inst_7 : (i : ι) → NormedAddCommGroup (Fi i)
inst_8 : (i : ι) → NormedSpace.{u_1, u_17} 𝕜 (Fi i)
φ : M → (i : ι) → Fi i
⊢ ContMDiffAt I (E' := (i : ι) → Fi i) 𝓘(𝕜, (i : ι) → Fi i) n φ x ↔
    ∀ (i : ι),
      ContMDiffAt.{u_1, u_2, u_3, u_4, u_17, u_17, u_17} I (E' := Fi i) 𝓘(𝕜, Fi i) (M' := Fi i) n (fun (x : M) ↦ φ x i)
        x

Tactic:
contMDiffWithinAt_pi_space

Premises used: contMDiffWithinAt_pi_space, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : WithTop ℕ∞
ι : Type u_16
inst_6 : Fintype ι
Fi : ι → Type u_17
inst_7 : (i : ι) → NormedAddCommGroup (Fi i)
inst_8 : (i : ι) → NormedSpace.{u_1, u_17} 𝕜 (Fi i)
φ : M → (i : ι) → Fi i
⊢ ContMDiff I (E' := (i : ι) → Fi i) 𝓘(𝕜, (i : ι) → Fi i) n φ ↔
    ∀ (i : ι),
      ContMDiff.{u_1, u_2, u_3, u_4, u_17, u_17, u_17} I (E' := Fi i) 𝓘(𝕜, Fi i) (M' := Fi i) n fun (x : M) ↦ φ x i

Tactic:
⟨fun h i x => contMDiffAt_pi_space.1 (h x) i, fun h x => contMDiffAt_pi_space.2 fun i => h i x⟩

Premises used: Iff.mpr, Iff.intro, Iff.mp, contMDiffAt_pi_space
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
rw :
  ContinuousAt (Y := M ⊕ M') Sum.inl x ∧
    ContDiffWithinAt 𝕜 n
      (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E)
        (Sum.inl ∘ (↑(extChartAt I x).symm : E → M)))
      (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContMDiffAt I I (M' := M ⊕ M') n Sum.inl x

Tactic:
rw [contMDiffAt_iff]

Premises used: contMDiffAt_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
⊢ ContinuousAt (Y := M ⊕ M') Sum.inl x ∧
    ContDiffWithinAt 𝕜 n
      (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E)
        (Sum.inl ∘ (↑(extChartAt I x).symm : E → M)))
      (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
⟨continuous_inl.continuousAt, ?_⟩

Premises used: continuous_inl, Continuous.continuousAt, And.intro
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
refine :
  ContDiffWithinAt 𝕜 n
    (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E)
      (Sum.inl ∘ (↑(extChartAt I x).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousAt (Y := M ⊕ M') Sum.inl x ∧
    ContDiffWithinAt 𝕜 n
      (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E)
        (Sum.inl ∘ (↑(extChartAt I x).symm : E → M)))
      (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
refine ⟨continuous_inl.continuousAt, ?_⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
h₁ :
  Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E)
      (Sum.inl ∘ (↑(extChartAt I x).symm : E → M)) =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    id
hx :
  Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) x) =
    id ((↑(extChartAt I x) : M → E) x)
⊢ ContDiffWithinAt 𝕜 n
    (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E)
      (Sum.inl ∘ (↑(extChartAt I x).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
apply contDiffWithinAt_id.congr_of_eventuallyEq

Premises used: ContDiffWithinAt.congr_of_eventuallyEq, contDiffWithinAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
⊢ Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) x) =
    id ((↑(extChartAt I x) : M → E) x)

Tactic:
simp [ChartedSpace.sum_chartAt_inl, Sum.inl_injective.extend_apply (chartAt _ x)]

Premises used: chartAt, Sum.inl_injective, ChartedSpace.sum_chartAt_inl, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
⊢ let C : OpenPartialHomeomorph M H := chartAt H x;
  C = chartAt H x

Tactic:
set C := chartAt H x with hC

Premises used: chartAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
C : OpenPartialHomeomorph M H := chartAt H x
hC : C = chartAt H x
rw :
  (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
⊢ (↑I.symm : E → H) ⁻¹' C.target ∩ range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
rw [← I.image_eq (chartAt H x).target]

Premises used: ModelWithCorners.image_eq, chartAt, PartialEquiv.target, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
C : OpenPartialHomeomorph M H := chartAt H x
hC : C = chartAt H x
⊢ (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
(chartAt H x).extend_image_target_mem_nhds (mem_chart_source _ x)

Premises used: mem_chart_source, chartAt, Set.Mem, setOf, OpenPartialHomeomorph.extend_image_target_mem_nhds
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
C : OpenPartialHomeomorph M H := chartAt H x
hC : C = chartAt H x
⊢ (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
exact (chartAt H x).extend_image_target_mem_nhds (mem_chart_source _ x)

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.extend_image_target_mem_nhds
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
C : OpenPartialHomeomorph M H := chartAt H x
hC : C = chartAt H x
⊢ (↑I.symm : E → H) ⁻¹' C.target ∩ range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
have : I.symm ⁻¹' C.target ∩ range I ∈ 𝓝[range I] (extChartAt I x) x := by
    rw [← I.image_eq (chartAt H x).target]
    exact (chartAt H x).extend_image_target_mem_nhds (mem_chart_source _ x)
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
C : OpenPartialHomeomorph M H := chartAt H x
hC : C = chartAt H x
this : (↑I.symm : E → H) ⁻¹' C.target ∩ range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
h :
  ∀ (y : E) (hy : y ∈ (↑I.symm : E → H) ⁻¹' C.target ∩ range (↑I : H → E)),
    Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl ∘ (↑(extChartAt I x).symm : E → M))
        y =
      id y
⊢ Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E)
      (Sum.inl ∘ (↑(extChartAt I x).symm : E → M)) =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    id

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M
C : OpenPartialHomeomorph M H := chartAt H x
hC : C = chartAt H x
this : (↑I.symm : E → H) ⁻¹' C.target ∩ range (↑I : H → E) ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' C.target ∩ range (↑I : H → E)
⊢ Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl ∘ (↑(extChartAt I x).symm : E → M))
      y =
    id y

Tactic:
simp [extChartAt, sum_chartAt_inl, ← hC, Sum.inl_injective.extend_apply C, C.right_inv hy.1,
    I.right_inv hy.2]

Premises used: extChartAt, Sum.inl_injective, ChartedSpace.sum_chartAt_inl, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply, ModelWithCorners.right_inv, And.right, And.left, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M'
rw :
  ContinuousAt (Y := M ⊕ M') Sum.inr x ∧
    ContDiffWithinAt 𝕜 n
      (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E)
        (Sum.inr ∘ (↑(extChartAt I x).symm : E → M')))
      (range (↑I : H → E)) ((↑(extChartAt I x) : M' → E) x)
⊢ ContMDiffAt I I (M' := M ⊕ M') n Sum.inr x

Tactic:
rw [contMDiffAt_iff]

Premises used: contMDiffAt_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M'
⊢ ContinuousAt (Y := M ⊕ M') Sum.inr x ∧
    ContDiffWithinAt 𝕜 n
      (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E)
        (Sum.inr ∘ (↑(extChartAt I x).symm : E → M')))
      (range (↑I : H → E)) ((↑(extChartAt I x) : M' → E) x)

Tactic:
⟨continuous_inr.continuousAt, ?_⟩

Premises used: continuous_inr, Continuous.continuousAt, And.intro
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
x : M'
refine :
  ContDiffWithinAt 𝕜 n
    (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E)
      (Sum.inr ∘ (↑(extChartAt I x).symm : E → M')))
    (range (↑I : H → E)) ((↑(extChartAt I x) : M' → E) x)
⊢ ContinuousAt (Y := M ⊕ M') Sum.inr x ∧
    ContDiffWithinAt 𝕜 n
      (Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E)
        (Sum.inr ∘ (↑(extChartAt I x).symm : E → M')))
      (range (↑I : H → E)) ((↑(extChartAt I x) : M' → E) x)

Tactic:
refine ⟨continuous_inr.continuousAt, ?_⟩