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 ℕ∞
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
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)
⊢ 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:
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'
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)
⊢ 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:
simp only [mfld_simps, sum_chartAt_inr]

Premises used: ChartedSpace.sum_chartAt_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 ℕ∞
x : M'
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
⊢ (↑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:
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 ℕ∞
x : M'
⊢ 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:
apply Sum.inr_injective.extend_apply (chartAt _ x)

Premises used: Sum.inr_injective, chartAt, 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) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).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) ⁻¹' (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)
-- 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) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M' → E) x
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
⊢ 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:
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) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M' → E) x
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:
simp [extChartAt, sum_chartAt_inr, ← hC, Sum.inr_injective.extend_apply C, C.right_inv hy.1,
    I.right_inv hy.2]

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, Sum.inr_injective, 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'
x y : M
⊢ (↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl y) = (↑(extChartAt I x) : M → E) y

Tactic:
simp
-- 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'
x y : M'
⊢ (↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr y) = (↑(extChartAt I x) : M' → E) y

Tactic:
simp
-- 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'
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)
⊢ ContMDiffAt I J n (Sum.elim f g) p

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 ℕ∞
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)

Tactic:
⟨(Continuous.sumElim hf.continuous hg.continuous).continuousAt, ?_⟩

Premises used: ContMDiff.continuous, Continuous.continuousAt, And.intro, Continuous.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
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'
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)
⊢ 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:
refine ⟨(Continuous.sumElim hf.continuous hg.continuous).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 ℕ∞
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 := ⋯
⊢ 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'

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
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)
⊢ 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:
simpa using hf'.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 (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
-- 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 :
  (↑(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)
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))
⊢ 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))

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 (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') =ᶠ[𝓝[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)
⊢ (↑(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:
simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_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))
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) ⋯) 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
⊢ (↑(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)

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 (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))
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) ⋯) 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:
congr