awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
⊢ (↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x ∈
    (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))

Tactic:
exact ⟨(extChartAt _ x).map_source (mem_extChartAt_source x), trivial, by
      simp only [e.symm_apply_apply, Equiv.refl_symm, Equiv.coe_refl, mfld_simps]⟩
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M' → M
x : M'
s : Set M'
⊢ ContMDiffWithinAt I' (I.transContinuousLinearEquiv e) n f s x ↔ ContMDiffWithinAt I' I n f s x

Tactic:
(toTransContinuousLinearEquiv I M e).contMDiffWithinAt_diffeomorph_comp_iff le_rfl

Premises used: le_rfl, ContinuousLinearEquiv.toTransContinuousLinearEquiv, Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M' → M
x : M'
⊢ ContMDiffAt I' (I.transContinuousLinearEquiv e) n f x ↔ ContMDiffAt I' I n f x

Tactic:
(toTransContinuousLinearEquiv I M e).contMDiffAt_diffeomorph_comp_iff le_rfl

Premises used: le_rfl, Diffeomorph.contMDiffAt_diffeomorph_comp_iff, ContinuousLinearEquiv.toTransContinuousLinearEquiv
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M' → M
s : Set M'
⊢ ContMDiffOn I' (I.transContinuousLinearEquiv e) n f s ↔ ContMDiffOn I' I n f s

Tactic:
(toTransContinuousLinearEquiv I M e).contMDiffOn_diffeomorph_comp_iff le_rfl

Premises used: le_rfl, Diffeomorph.contMDiffOn_diffeomorph_comp_iff, ContinuousLinearEquiv.toTransContinuousLinearEquiv
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M' → M
⊢ ContMDiff I' (I.transContinuousLinearEquiv e) n f ↔ ContMDiff I' I n f

Tactic:
(toTransContinuousLinearEquiv I M e).contMDiff_diffeomorph_comp_iff le_rfl

Premises used: le_rfl, ContinuousLinearEquiv.toTransContinuousLinearEquiv, Diffeomorph.contMDiff_diffeomorph_comp_iff
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M → M'
x : M
s : Set M
⊢ ContMDiffWithinAt (I.transContinuousLinearEquiv e) I' n f s x ↔ ContMDiffWithinAt I I' n f s x

Tactic:
((toTransContinuousLinearEquiv I M e).contMDiffWithinAt_comp_diffeomorph_iff le_rfl).symm

Premises used: le_rfl, Set.Mem, setOf, Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff, Set.preimage, ContinuousLinearEquiv.toTransContinuousLinearEquiv, Iff.symm
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M → M'
x : M
⊢ ContMDiffAt (I.transContinuousLinearEquiv e) I' n f x ↔ ContMDiffAt I I' n f x

Tactic:
((toTransContinuousLinearEquiv I M e).contMDiffAt_comp_diffeomorph_iff le_rfl).symm

Premises used: le_rfl, Diffeomorph.contMDiffAt_comp_diffeomorph_iff, ContinuousLinearEquiv.toTransContinuousLinearEquiv, Iff.symm
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M → M'
s : Set M
⊢ ContMDiffOn (I.transContinuousLinearEquiv e) I' n f s ↔ ContMDiffOn I I' n f s

Tactic:
((toTransContinuousLinearEquiv I M e).contMDiffOn_comp_diffeomorph_iff le_rfl).symm

Premises used: Diffeomorph.contMDiffOn_comp_diffeomorph_iff, le_rfl, Set.Mem, setOf, Set.preimage, ContinuousLinearEquiv.toTransContinuousLinearEquiv, Iff.symm
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H M
M' : Type u_10
inst_11 : TopologicalSpace M'
inst_12 : ChartedSpace H' M'
n : ℕ∞ω
e : E ≃L[𝕜] F
f : M → M'
⊢ ContMDiff (I.transContinuousLinearEquiv e) I' n f ↔ ContMDiff I I' n f

Tactic:
((toTransContinuousLinearEquiv I M e).contMDiff_comp_diffeomorph_iff le_rfl).symm

Premises used: le_rfl, Diffeomorph.contMDiff_comp_diffeomorph_iff, ContinuousLinearEquiv.toTransContinuousLinearEquiv, Iff.symm
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
h₁ : M ≃ₘ^n⟮I, I'⟯ M'
h₂ : N ≃ₘ^n⟮J, J'⟯ N'
⊢ (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm

Tactic:
rfl

Premises used: Diffeomorph.symm, Prod.map, Equiv.symm, Equiv.prodCongr, Diffeomorph.prodCongr, rfl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
h₁ : M ≃ₘ^n⟮I, I'⟯ M'
h₂ : N ≃ₘ^n⟮J, J'⟯ N'
⊢ Eq (α := (a : M × N) → M' × N') (⇑(h₁.prodCongr h₂) : (a : M × N) → M' × N')
    (Prod.map (⇑h₁ : (a : M) → M') (⇑h₂ : (a : N) → N'))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_11
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
⊢ Eq (α := (N × M) ≃ₘ^n⟮J.prod I, I.prod J⟯ M × N) (Diffeomorph.symm (prodComm I J M N n)) (prodComm J I N M n)

Tactic:
rfl

Premises used: Diffeomorph.symm, Equiv.prodComm, Diffeomorph.prodComm, Prod.swap, Equiv.symm, rfl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_11
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
⊢ Eq (α := (a : M × N) → N × M) (⇑(prodComm I J M N n) : (a : M × N) → N × M) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M'
N : Type u_15
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H N'
φ : M ≃ₘ^n⟮I, J⟯ N
ψ : M' ≃ₘ^n⟮I, J⟯ N'
⊢ φ.symm.sumCongr ψ.symm = (φ.sumCongr ψ).symm

Tactic:
rfl

Premises used: Diffeomorph.symm, Sum.map, Diffeomorph.sumCongr, Equiv.sumCongr, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M'
N : Type u_15
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H N'
φ : M ≃ₘ^n⟮I, J⟯ N
ψ : M' ≃ₘ^n⟮I, J⟯ N'
⊢ Eq (α := (a : M ⊕ M') → N ⊕ N') (⇑(φ.sumCongr ψ) : (a : M ⊕ M') → N ⊕ N')
    (Sum.map (⇑φ : (a : M) → N) (⇑ψ : (a : M') → N'))

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M'
N : Type u_15
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H N'
φ : M ≃ₘ^n⟮I, J⟯ N
ψ : M' ≃ₘ^n⟮I, J⟯ N'
⊢ Eq (α := M → N ⊕ N') (comp (β := M ⊕ M') (⇑(φ.sumCongr ψ) : (a : M ⊕ M') → N ⊕ N') Sum.inl)
    (Sum.inl ∘ (⇑φ : (a : M) → N))

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_8 : TopologicalSpace M'
inst_9 : ChartedSpace H M'
N : Type u_15
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H N'
φ : M ≃ₘ^n⟮I, J⟯ N
ψ : M' ≃ₘ^n⟮I, J⟯ N'
⊢ Eq (α := M' → N ⊕ N') (comp (β := M ⊕ M') (⇑(φ.sumCongr ψ) : (a : M ⊕ M') → N ⊕ N') Sum.inr)
    (Sum.inr ∘ (⇑ψ : (a : M') → N'))

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
⊢ Eq (α := (a : M ⊕ M') → M' ⊕ M) (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.swap

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
⊢ Eq (α := (M' ⊕ M) ≃ₘ^n⟮I, I⟯ M ⊕ M') (Diffeomorph.symm (sumComm I M n M')) (sumComm I M' n M)

Tactic:
rfl

Premises used: Sum.swap, Diffeomorph.symm, Equiv.sumComm, Diffeomorph.sumComm, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
h : ∀ (x : M), Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inl x) (Sum.inr x)
⊢ Eq (α := M → M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inl) Sum.inr

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
⊢ Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inl x) (Sum.inr x)

Tactic:
Sum.swap_inl

Premises used: Sum.swap, Sum.elim, Sum.swap_inl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
⊢ Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inl x) (Sum.inr x)

Tactic:
exact Sum.swap_inl

Premises used: Sum.swap_inl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
h :
  ∀ (x : M'), Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inr x) (Sum.inl x)
⊢ Eq (α := M' → M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inr) Sum.inl

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
⊢ Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inr x) (Sum.inl x)

Tactic:
Sum.swap_inr

Premises used: Sum.swap, Sum.swap_inr, Sum.elim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
⊢ Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inr x) (Sum.inl x)

Tactic:
exact Sum.swap_inr

Premises used: Sum.swap_inr
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
hf : ContMDiff I (M := M ⊕ M') I (M' := M ⊕ M' ⊕ M'') n (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl))
hg : ContMDiff I (M := M'') I (M' := M ⊕ M' ⊕ M'') n (Sum.inr ∘ Sum.inr)
⊢ ContMDiff I (M := (M ⊕ M') ⊕ M'') I (M' := M ⊕ M' ⊕ M'') n
    (⇑(Equiv.sumAssoc M M' M'') : (a : (M ⊕ M') ⊕ M'') → M ⊕ M' ⊕ M'')

Tactic:
apply ContMDiff.sumElim

Premises used: ContMDiff.sumElim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M ⊕ M') I (M' := M ⊕ M' ⊕ M'') n (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl))

Tactic:
contMDiff_id.sumMap ContMDiff.inl

Premises used: Sum.map, ContMDiff.sumMap, ContMDiff.inl, contMDiff_id