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
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'
s : Set M
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
t : Set (M' × N')
ha : ContMDiffWithinAt (I'.prod J') J n h t y
fa : ContMDiffWithinAt I I' n f s x
ga : ContMDiffWithinAt I J' n g s x
e : (f x, g x) = y
st : MapsTo (fun (x : M) ↦ (f x, g x)) s t
⊢ ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ h (f x, g x)) s x
have ha₁ : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x)
Tactic: rw [← e] at ha
Cleared hypotheses: ha, fa, ga, e, st
-- 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
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'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
ha : ContMDiffAt (I'.prod J') J n h y
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
e : (f x, g x) = y
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ h (f x, g x)) x
have ha₁ : ContMDiffAt (I'.prod J') J n h (f x, g x)
Tactic: rw [← e] at ha
Cleared hypotheses: ha, fa, ga, e
-- 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
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
⊢ ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)
have 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)
Tactic: simp only [← contMDiffWithinAt_univ, ← univ_prod_univ] at *
Cleared hypotheses: hf, hg
-- 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 ℕ∞
x : M
⊢ ContMDiffAt I I (M' := M ⊕ M') n Sum.inl x
have 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)
Tactic: rw [contMDiffAt_iff]
-- 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 ℕ∞
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)
have 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)
Tactic: refine ⟨continuous_inl.continuousAt, ?_⟩
-- 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 ℕ∞
x : M
⊢ 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)
have 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
Tactic: apply contDiffWithinAt_id.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 ℕ∞
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
⊢ 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)
have 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)
Tactic: apply contDiffWithinAt_id.congr_of_eventuallyEq
-- 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 ℕ∞
x : M
⊢ 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
have hC : let C : OpenPartialHomeomorph M H := chartAt H x;
C = chartAt H x
Tactic: set C := chartAt H x with hC
-- 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 ℕ∞
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
have rw : (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
  𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
Tactic: rw [← I.image_eq (chartAt H x).target]
-- 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 ℕ∞
x : M
C : OpenPartialHomeomorph M H := chartAt H x
hC : C = chartAt H x
⊢ 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
have this : (↑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)
-- 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 ℕ∞
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
⊢ 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
have 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
Tactic: filter_upwards [this] with y hy
-- 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 ℕ∞
x : M'
⊢ ContMDiffAt I I (M' := M ⊕ M') n Sum.inr x
have 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)
Tactic: rw [contMDiffAt_iff]
-- 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 ℕ∞
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)
have 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)
Tactic: refine ⟨continuous_inr.continuousAt, ?_⟩
-- 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 ℕ∞
x : M'
⊢ 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)
have h₁ : 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]
  id
Tactic: apply contDiffWithinAt_id.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 ℕ∞
x : M'
h₁ :
  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]
    id
⊢ 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)
have hx : Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr ∘ (↑(extChartAt I x).symm : E → M'))
    ((↑(extChartAt I x) : M' → E) x) =
  id ((↑(extChartAt I x) : M' → E) x)
Tactic: apply contDiffWithinAt_id.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 ℕ∞
x : M'
⊢ Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr ∘ (↑(extChartAt I x).symm : E → M'))
      ((↑(extChartAt I x) : M' → E) x) =
    id ((↑(extChartAt I x) : M' → E) x)
have hx : (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) =
  (↑I : H → E) ((↑(chartAt H x) : M' → H) x)
Tactic: simp only [mfld_simps, 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 ℕ∞
x : M'
⊢ (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) =
    (↑I : H → E) ((↑(chartAt H x) : M' → H) x)
have hx : extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x) =
  (↑(chartAt H x) : M' → H) x
Tactic: congr
-- 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 ℕ∞
x : M'
⊢ 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]
    id
have hC : let C : OpenPartialHomeomorph M' H := chartAt H x;
C = chartAt H x
Tactic: set C := chartAt H x with hC
-- 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 ℕ∞
x : M'
C : OpenPartialHomeomorph M' H := chartAt H x
hC : C = chartAt H x
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M' → E) x
have rw : (↑I : H → E) '' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
  𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M' → E) x
Tactic: rw [← I.image_eq (chartAt H x).target]
-- 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 ℕ∞
x : M'
C : OpenPartialHomeomorph M' H := chartAt H x
hC : C = chartAt H x
⊢ 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]
    id
have this : (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) ∈
  𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M' → E) x
Tactic: have : I.symm ⁻¹' (chartAt H x).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)
-- 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 ℕ∞
x : M'
C : OpenPartialHomeomorph M' H := chartAt H x
hC : C = chartAt H x
this :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M' → E) x
⊢ 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]
    id
have h : ∀ (y : E)
  (hy : y ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)),
  Function.comp (β := M ⊕ M') (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr ∘ (↑(extChartAt I x).symm : E → M'))
      y =
    id y
Tactic: filter_upwards [this] with y hy
-- 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
p : M ⊕ M'
⊢ ContMDiffAt I J n (Sum.elim f g) p
have rw : ContinuousAt (Sum.elim f g) p ∧
  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: rw [contMDiffAt_iff]
-- 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
p : M ⊕ M'
⊢ ContinuousAt (Sum.elim f g) p ∧
    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)
have refine : 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: refine ⟨(Continuous.sumElim hf.continuous hg.continuous).continuousAt, ?_⟩
-- 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
hf' : ContMDiffAt I J n f x := ⋯
⊢ 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))
have hf'₁ : ContinuousAt f x ∧
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J (f x)) : N → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
Tactic: rw [contMDiffAt_iff] at hf'
Cleared hypotheses: hf'