awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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 (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))
have 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))
Tactic: 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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))
⊢ 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))
have inl : (↑(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)]
  (↑(extChartAt J (f x)) : N → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)
Tactic: apply this.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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 :
  (↑(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)]
    (↑(extChartAt J (f x)) : N → E') ∘ f ∘ (↑(extChartAt I x).symm : E → 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))
have inl₁ : ((↑(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: apply this.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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))
⊢ (↑(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)]
    (↑(extChartAt J (f x)) : N → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)
have inl : (↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
    Sum.elim f g ∘
      (↑(PartialEquiv.symm
            (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I)) :
        E →
          M ⊕
            M') =ᶠ[𝓝[range (↑I : H → E)]
    (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) 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)
Tactic: simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_inl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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') =ᶠ[𝓝[range (↑I : H → E)]
      (↑(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)
have inl : ∀ (a : E),
  ((↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
        Sum.elim f g ∘
          (↑(PartialEquiv.symm
                (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I)) :
            E → M ⊕ M'))
      a =
    ((↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.extend (chartAt H x) I).symm : E → M))
      a
Tactic: filter_upwards with a
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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))
⊢ ((↑(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))
have inl : ((↑(OpenPartialHomeomorph.extend (chartAt H' (f x)) J) : N → E') ∘
      Sum.elim f g ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I)) :
          E → M ⊕ M'))
    ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) 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) sorry) I) : M ⊕ M' → E)
      (Sum.inl x))
Tactic: simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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 := ⋯
⊢ 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))
have 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)
Tactic: rw [contMDiffAt_iff] at hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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 (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))
have 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))
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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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))
⊢ 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))
have 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')
Tactic: apply this.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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')
⊢ 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))
have 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))
Tactic: apply this.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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))
⊢ (↑(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')
have inr : (↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
    Sum.elim f g ∘
      (↑(PartialEquiv.symm
            (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I)) :
        E →
          M ⊕
            M') =ᶠ[𝓝[range (↑I : H → E)]
    (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) 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: simp only [extChartAt, Sum.elim_inr, ChartedSpace.sum_chartAt_inr]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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') =ᶠ[𝓝[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')
have 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) sorry) 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: filter_upwards with a
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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
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))
⊢ ((↑(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))
have inr : ((↑(OpenPartialHomeomorph.extend (chartAt H' (g x)) J) : N → E') ∘
      Sum.elim f g ∘
        (↑(PartialEquiv.symm
              (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I)) :
          E → M ⊕ M'))
    ((↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) 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) sorry) I) : M ⊕ M' → E)
      (Sum.inr x))
Tactic: simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]