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
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (f x)) : N → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl x))
inl :
  ((↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
        Sum.elim f g ∘
          (↑(PartialEquiv.symm
                (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
            E → M ⊕ M'))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inl x)) =
    ((↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inl x))
⊢ ((↑(extChartAt J (Sum.elim f g (Sum.inl x))) : N → E') ∘
        Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inl x))) : E → M ⊕ M'))
      ((↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl x)) =
    ((↑(extChartAt J (f x)) : N → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl x))

Tactic:
simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]

Premises used: extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (f x)) : N → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl x))
⊢ ((↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
        Sum.elim f g ∘
          (↑(PartialEquiv.symm
                (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
            E → M ⊕ M'))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inl x)) =
    ((↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inl x))

Tactic:
congr
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
hg' : ContMDiffAt I J n g x := ⋯
⊢ ContinuousAt g x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
      ((↑(extChartAt I x) : M' → E) x)

Tactic:
rw [contMDiffAt_iff] at hg'

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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
hg' :
  ContinuousAt g x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
      ((↑(extChartAt I x) : M' → E) x)
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))

Tactic:
simpa using hg'.2

Premises used: And.right
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))

Tactic:
have : ContDiffWithinAt 𝕜 n ((extChartAt J (g x)) ∘ g ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) := by
      let hg' := hg x
      rw [contMDiffAt_iff] at hg'
      simpa using hg'.2
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
inr :
  (↑(extChartAt J (Sum.elim f g (Sum.inr x))) : N → E') ∘
      Sum.elim f g ∘
        (↑(PartialEquiv.symm (extChartAt I (Sum.inr x))) :
          E → M ⊕ M') =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x)]
    (↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')
inr₁ :
  ((↑(extChartAt J (Sum.elim f g (Sum.inr x))) : N → E') ∘
        Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inr x))) : E → M ⊕ M'))
      ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x)) =
    ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M'))
      ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
⊢ ContDiffWithinAt 𝕜 n
    ((↑(extChartAt J (Sum.elim f g (Sum.inr x))) : N → E') ∘
      Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inr x))) : E → M ⊕ M'))
    (range (↑I : H → E)) ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))

Tactic:
apply this.congr_of_eventuallyEq

Premises used: ContDiffWithinAt.congr_of_eventuallyEq
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
inr :
  (↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
      Sum.elim f g ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
          E →
            M ⊕
              M') =ᶠ[𝓝[range (↑I : H → E)]
      (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inr x)]
    (↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
      g ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M')
⊢ (↑(extChartAt J (Sum.elim f g (Sum.inr x))) : N → E') ∘
      Sum.elim f g ∘
        (↑(PartialEquiv.symm (extChartAt I (Sum.inr x))) :
          E → M ⊕ M') =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x)]
    (↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')

Tactic:
simp only [extChartAt, Sum.elim_inr, ChartedSpace.sum_chartAt_inr]

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, Sum.elim_inr
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
inr :
  ∀ (a : E),
    ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
          Sum.elim f g ∘
            (↑(PartialEquiv.symm
                  (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
              E → M ⊕ M'))
        a =
      ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
          g ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M'))
        a
⊢ (↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
      Sum.elim f g ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
          E →
            M ⊕
              M') =ᶠ[𝓝[range (↑I : H → E)]
      (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inr x)]
    (↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
      g ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M')

Tactic:
filter_upwards with a
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
a : E
⊢ ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
        Sum.elim f g ∘
          (↑(PartialEquiv.symm
                (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
            E → M ⊕ M'))
      a =
    ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
        g ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M'))
      a

Tactic:
congr
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
inr :
  ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
        Sum.elim f g ∘
          (↑(PartialEquiv.symm
                (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
            E → M ⊕ M'))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inr x)) =
    ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
        g ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M'))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inr x))
⊢ ((↑(extChartAt J (Sum.elim f g (Sum.inr x))) : N → E') ∘
        Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inr x))) : E → M ⊕ M'))
      ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x)) =
    ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M'))
      ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))

Tactic:
simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, Sum.elim_inr
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (g x)) : N → E') ∘ g ∘ (↑(extChartAt I x).symm : E → M')) (range (↑I : H → E))
    ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
⊢ ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
        Sum.elim f g ∘
          (↑(PartialEquiv.symm
                (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I)) :
            E → M ⊕ M'))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inr x)) =
    ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
        g ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M'))
      ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
        (Sum.inr x))

Tactic:
congr
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
p : M ⊕ M'
inl :
  ∀ (x : M),
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt J (Sum.elim f g (Sum.inl x))) : N → E') ∘
        Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inl x))) : E → M ⊕ M'))
      (range (↑I : H → E)) ((↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl x))
inr :
  ∀ (x : M'),
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt J (Sum.elim f g (Sum.inr x))) : N → E') ∘
        Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inr x))) : E → M ⊕ M'))
      (range (↑I : H → E)) ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
⊢ ContDiffWithinAt 𝕜 n
    ((↑(extChartAt J (Sum.elim f g p)) : N → E') ∘ Sum.elim f g ∘ (↑(extChartAt I p).symm : E → M ⊕ M'))
    (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)

Tactic:
cases p with
  | inl x =>
    -- In charts around x : M, the map f ⊔ g looks like f.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) := by
      let hf' := hf x
      rw [contMDiffAt_iff] at hf'
      simpa using hf'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_inl]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]
      congr
  | inr x =>
    -- In charts around x : M, the map f ⊔ g looks like g.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (g x)) ∘ g ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) := by
      let hg' := hg x
      rw [contMDiffAt_iff] at hg'
      simpa using hg'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inr, ChartedSpace.sum_chartAt_inr]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]
      congr

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, ContMDiff.inr, ContMDiff.inl, ChartedSpace.sum_chartAt_inl, Sum.elim_inr, Sum.elim_inl
-- 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 ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_11 : TopologicalSpace N
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H' N
inst_14 : ChartedSpace H' N'
f : M → N
g : M' → N'
hf : ContMDiff I J n f
hg : ContMDiff I J n g
⊢ ContMDiff I J n (Sum.map f g)

Tactic:
ContMDiff.sumElim (ContMDiff.inl.comp hf) (ContMDiff.inr.comp hg)

Premises used: ContMDiff.comp, Sum.map, ContMDiff.inr, ContMDiff.inl, ContMDiff.sumElim
-- 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 ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
⊢ Nontrivial N

Tactic:
nontriviality N
-- 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 ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabit : ∀ (inhabited_h : Inhabited N), ContMDiff I J n f
⊢ ContMDiff I J n f

Tactic:
inhabit N
-- 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 ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
h₁ : ∀ (x : M), (aux ∘ Sum.inl ∘ f) x = f x
⊢ aux ∘ Sum.inl ∘ f = f

Tactic:
ext