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

Tactic:
simp [aux]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
⊢ aux ∘ Sum.inl ∘ f = f

Tactic:
have : aux ∘ (@Sum.inl N N') ∘ f = f := by ext; simp [aux]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
rw : ContMDiff I J n (aux ∘ Sum.inl ∘ f)
⊢ ContMDiff I J n f

Tactic:
rw [← this]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
rw :
  ∀ (h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ),
    Nontrivial N →
      ∀ (inhabited_h : Inhabited N),
        let aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default;
        ∀ (this : aux ∘ Sum.inl ∘ f = f), ContMDiffOn I J n (aux ∘ Sum.inl ∘ f) univ
⊢ ContMDiff I J n (aux ∘ Sum.inl ∘ f)

Tactic:
rw [← contMDiffOn_univ] at h ⊢

Premises used: contMDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
apply : univ ⊆ preimage (β := N ⊕ N') (Sum.inl ∘ f) (Sum.inl '' univ)
⊢ ContMDiffOn I J n (aux ∘ Sum.inl ∘ f) univ

Tactic:
apply (contMDiff_id.sumElim contMDiff_const).contMDiffOn (s := @Sum.inl N N' '' univ).comp h

Premises used: contMDiff_const, ContMDiff.contMDiffOn, ContMDiff.sumElim, contMDiff_id, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
x : M
_hx : Membership.mem (γ := Set M) univ x
w : N
left : Membership.mem (γ := Set N) univ (f x)
right : Eq (α := N ⊕ N') (Sum.inl (f x)) (Sum.inl (f x))
⊢ Membership.mem (γ := Set (N ⊕ N')) (Sum.inl '' univ) (Sum.inl (f x))

Tactic:
use f x, trivial

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

Tactic:
nontriviality N'
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabit : ∀ (inhabited_h : Inhabited N'), ContMDiff I J n g
⊢ ContMDiff I J n g

Tactic:
inhabit N'
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
h₁ : ∀ (x : M'), (aux ∘ Sum.inr ∘ g) x = g x
⊢ aux ∘ Sum.inr ∘ g = g

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

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

Tactic:
have : aux ∘ (@Sum.inr N N') ∘ g = g := by ext; simp [aux]
-- 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_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
rw : ContMDiff I J n (aux ∘ Sum.inr ∘ g)
⊢ ContMDiff I J n g

Tactic:
rw [← this]
-- 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_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
rw :
  ∀ (h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inr ∘ g) univ),
    Nontrivial N' →
      ∀ (inhabited_h : Inhabited N'),
        let aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id;
        ∀ (this : aux ∘ Sum.inr ∘ g = g), ContMDiffOn I J n (aux ∘ Sum.inr ∘ g) univ
⊢ ContMDiff I J n (aux ∘ Sum.inr ∘ g)

Tactic:
rw [← contMDiffOn_univ] at h ⊢

Premises used: contMDiffOn_univ
-- 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_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inr ∘ g) univ
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
apply : univ ⊆ preimage (β := N ⊕ N') (Sum.inr ∘ g) (Sum.inr '' univ)
⊢ ContMDiffOn I J n (aux ∘ Sum.inr ∘ g) univ

Tactic:
apply ((contMDiff_const.sumElim contMDiff_id).contMDiffOn (s := Sum.inr '' univ)).comp h

Premises used: contMDiff_const, ContMDiff.contMDiffOn, ContMDiff.sumElim, contMDiff_id, ContMDiffOn.comp
-- 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_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inr ∘ g) univ
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
x : M'
_hx : Membership.mem (γ := Set M') univ x
w : N'
left : Membership.mem (γ := Set N') univ (g x)
right : Eq (α := N ⊕ N') (Sum.inr (g x)) (Sum.inr (g x))
⊢ Membership.mem (γ := Set (N ⊕ N')) (Sum.inr '' univ) (Sum.inr (g x))

Tactic:
use g x, trivial

Premises used: trivial
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_11 : TopologicalSpace N
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H' N
inst_14 : ChartedSpace H' N'
f : M → N
g : M' → N'
⊢ ContMDiff I J n (Sum.map f g) ↔ ContMDiff I J n f ∧ ContMDiff I J n g

Tactic:
⟨fun h ↦ ⟨contMDiff_of_contMDiff_inl (h.comp ContMDiff.inl),
    contMDiff_of_contMDiff_inr (h.comp ContMDiff.inr)⟩,
   fun h ↦ ContMDiff.sumMap h.1 h.2⟩

Premises used: ContMDiff.comp, contMDiff_of_contMDiff_inl, ContMDiff.inr, ContMDiff.sumMap, ContMDiff.inl, contMDiff_of_contMDiff_inr, And.right, And.left, And.intro, Iff.intro
-- 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 ℕ∞
⊢ ContMDiff I (M := M ⊕ M') I n Sum.swap

Tactic:
ContMDiff.sumElim inr inl

Premises used: Sum.swap, ContMDiff.inr, ContMDiff.inl, ContMDiff.sumElim
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
f : E → H'
s : Set E
x : E
simp_rw :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x
simp_rw₁ :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
    ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x
simp_rw₂ :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ univ) (id x) ↔
    ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x
simp_rw₃ :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s) (id x) ↔
    ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x
simp_rw₄ :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f ∘ id) (id ⁻¹' s) (id x) ↔ ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x
simp_rw₅ : ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) (id ⁻¹' s) (id x) ↔ ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x
simp_rw₆ : ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) (id s) (id x) ↔ ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x
⊢ ContDiffWithinAtProp 𝓘(𝕜, E) I' n f s x ↔ ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ f) s x

Tactic:
simp_rw [ContDiffWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]

Premises used: modelWithCornersSelf_coe_symm, Set.inter_univ, CompTriple.comp_eq, Set.preimage_id_eq, Set.range_id, modelWithCornersSelf_coe, ContDiffWithinAtProp, id_eq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : ℕ∞ω
f : E → E'
s : Set E
x : E
⊢ ContDiffWithinAtProp 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
contDiffWithinAtProp_self_source

Premises used: contDiffWithinAtProp_self_source, ModelWithCorners.toFun'
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
n : ℕ∞ω
f : H → E'
s : Set H
x : H
⊢ ContDiffWithinAtProp I 𝓘(𝕜, E') n f s x ↔
    ContDiffWithinAt 𝕜 n (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
Iff.rfl

Premises used: Iff.rfl, ModelWithCorners.toFun', ContDiffWithinAtProp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
⊢ (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u

Tactic:
simp only [inter_right_comm, preimage_inter]

Premises used: Set.preimage_inter, Set.inter_right_comm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
⊢ (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u

Tactic:
have : I.symm ⁻¹' (s ∩ u) ∩ range I = I.symm ⁻¹' s ∩ range I ∩ I.symm ⁻¹' u := by
      simp only [inter_right_comm, preimage_inter]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
rw :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x) ↔
    ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x)
⊢ ContDiffWithinAtProp I I' m f s x ↔ ContDiffWithinAtProp I I' m f (s ∩ u) x

Tactic:
rw [ContDiffWithinAtProp, ContDiffWithinAtProp, this]

Premises used: ContDiffWithinAtProp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
symm :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x) ↔
    ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x) ↔
    ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x)

Tactic:
symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
h : (↑I.symm : E → H) ⁻¹' u ∈ 𝓝 ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x) ↔
    ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x)

Tactic:
apply contDiffWithinAt_inter

Premises used: contDiffWithinAt_inter