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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
Hfh : ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s ((h.symm : (a : N) → M) ((h : (a : M) → N) x : N))
⊢ ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x)

Tactic:
simpa only [Function.comp_def, h.apply_symm_apply] using
      Hfh.comp (h x) (h.symm.contMDiffWithinAt.of_le hm) (mapsTo_preimage _ _)

Premises used: Diffeomorph.contMDiffWithinAt, Diffeomorph.symm, Diffeomorph.apply_symm_apply, Set.mapsTo_preimage, Function.comp_def, ContMDiffWithinAt.of_le, DFunLike.coe, ContMDiffWithinAt.comp
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
mpr :
  ContMDiffWithinAt J I' m f ((⇑h : (a : M) → N) '' s) ((h : (a : M) → N) x) →
    ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x
⊢ ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x) →
    ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x

Tactic:
rw [← h.image_eq_preimage_symm]

Premises used: Diffeomorph.image_eq_preimage_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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt J I' m f ((⇑h : (a : M) → N) '' s) ((h : (a : M) → N) x) →
    ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x

Tactic:
fun hf => hf.comp x (h.contMDiffWithinAt.of_le hm) (mapsTo_image _ _)

Premises used: Diffeomorph.contMDiffWithinAt, Set.mapsTo_image, ContMDiffWithinAt.of_le, DFunLike.coe, ContMDiffWithinAt.comp
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt J I' m f ((⇑h : (a : M) → N) '' s) ((h : (a : M) → N) x) →
    ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x

Tactic:
exact fun hf => hf.comp x (h.contMDiffWithinAt.of_le hm) (mapsTo_image _ _)
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
hm : m ≤ n
x : M
⊢ x ∈ s → ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x ↔
    Membership.mem.{u_11, u_11} (α := N) (γ := Set N) ((⇑h.symm : (a : N) → M) ⁻¹' s)
        ((h.toEquiv : (a : M) → N) x : N) →
      ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h.toEquiv : (a : M) → N) x)

Tactic:
simp only [hm, coe_toEquiv, h.symm_apply_apply, contMDiffWithinAt_comp_diffeomorph_iff,
      mem_preimage]

Premises used: Diffeomorph.symm_apply_apply, Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff, Diffeomorph.coe_toEquiv, Set.mem_preimage
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
x : M
hm : m ≤ n
⊢ ContMDiffAt I I' m (f ∘ (⇑h : (a : M) → N)) x ↔ ContMDiffAt J I' m f ((h : (a : M) → N) x)

Tactic:
h.contMDiffWithinAt_comp_diffeomorph_iff hm

Premises used: Set.Mem, Set.univ, setOf, Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff, Set.preimage, ContMDiffAt
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
hm : m ≤ n
⊢ ContMDiff.{u_1, u_2, u_5, u_9, u_3, u_6, u_10} I (M := M) I' m (f ∘ (⇑h : (a : M) → N)) ↔ ContMDiff J I' m f

Tactic:
h.toEquiv.forall_congr fun _ ↦ h.contMDiffAt_comp_diffeomorph_iff hm

Premises used: ContMDiff, Diffeomorph.toEquiv, Diffeomorph.contMDiffAt_comp_diffeomorph_iff, Equiv.forall_congr
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : M' → M
hm : m ≤ n
s : Set M'
x : M'
Hhf : ContMDiffWithinAt.{u_1, u_3, u_6, u_10, u_4, u_7, u_11} I' J (M' := N) m ((⇑h : (a : M) → N) ∘ f) s x
⊢ ContMDiffWithinAt I' I m f s x

Tactic:
simpa only [Function.comp_def, h.symm_apply_apply] using
      (h.symm.contMDiffAt.of_le hm).comp_contMDiffWithinAt _ Hhf

Premises used: Diffeomorph.symm, Diffeomorph.symm_apply_apply, ContMDiffAt.of_le, Function.comp_def, Diffeomorph.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : M' → M
hm : m ≤ n
x : M'
⊢ ContMDiffAt.{u_1, u_3, u_6, u_10, u_4, u_7, u_11} I' J (M' := N) m ((⇑h : (a : M) → N) ∘ f) x ↔ ContMDiffAt I' I m f x

Tactic:
h.contMDiffWithinAt_diffeomorph_comp_iff hm

Premises used: ContMDiffAt, 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'
G : Type u_7
inst_9 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : M' → M
hm : m ≤ n
s : Set M'
⊢ ContMDiffOn.{u_1, u_3, u_6, u_10, u_4, u_7, u_11} I' J (M' := N) m ((⇑h : (a : M) → N) ∘ f) s ↔ ContMDiffOn I' I m f s

Tactic:
forall₂_congr fun _ _ => h.contMDiffWithinAt_diffeomorph_comp_iff hm

Premises used: forall₂_congr, Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff, ContMDiffOn
-- 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
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : M' → M
hm : m ≤ n
⊢ ContMDiff.{u_1, u_3, u_6, u_10, u_4, u_7, u_11} I' J (M' := N) m ((⇑h : (a : M) → N) ∘ f) ↔ ContMDiff I' I m f

Tactic:
forall_congr' fun _ => h.contMDiffWithinAt_diffeomorph_comp_iff hm

Premises used: ContMDiff, forall_congr', 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
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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
⊢ OpenPartialHomeomorph.MDifferentiable I J h.toHomeomorph.toOpenPartialHomeomorph

Tactic:
⟨h.mdifferentiableOn _ hn, h.symm.mdifferentiableOn _ hn⟩

Premises used: Diffeomorph.symm, Diffeomorph.mdifferentiableOn, And.intro, OpenPartialHomeomorph.MDifferentiable
-- 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
s : Set M
hs : UniqueMDiffOn I s
⊢ UniqueMDiffOn J
    (h.toHomeomorph.toOpenPartialHomeomorph.target ∩ (↑h.toHomeomorph.toOpenPartialHomeomorph.symm : N → M) ⁻¹' s)

Tactic:
hs.uniqueMDiffOn_preimage (h.toOpenPartialHomeomorph_mdifferentiable hn)

Premises used: UniqueMDiffOn.uniqueMDiffOn_preimage, Diffeomorph.toOpenPartialHomeomorph_mdifferentiable
-- 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
s : Set M
hs : UniqueMDiffOn I s
h₁ :
  (⇑h : (a : M) → N) '' s =
    h.toHomeomorph.toOpenPartialHomeomorph.target ∩ (↑h.toHomeomorph.toOpenPartialHomeomorph.symm : N → M) ⁻¹' s
⊢ UniqueMDiffOn.{u_1, u_4, u_7, u_11} J (M := N) ((⇑h : (a : M) → N) '' s)

Tactic:
convert! hs.uniqueMDiffOn_preimage (h.toOpenPartialHomeomorph_mdifferentiable hn)

Premises used: UniqueMDiffOn.uniqueMDiffOn_preimage, Diffeomorph.toOpenPartialHomeomorph_mdifferentiable
-- 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
s : Set M
hs : UniqueMDiffOn I s
⊢ (⇑h : (a : M) → N) '' s =
    h.toHomeomorph.toOpenPartialHomeomorph.target ∩ (↑h.toHomeomorph.toOpenPartialHomeomorph.symm : N → M) ⁻¹' s

Tactic:
simp [h.image_eq_preimage_symm]

Premises used: Diffeomorph.image_eq_preimage_symm
-- 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
s : Set M
⊢ UniqueMDiffOn.{u_1, u_4, u_7, u_11} J (M := N) ((⇑h : (a : M) → N) '' s) ↔ UniqueMDiffOn I s

Tactic:
⟨fun hs => h.symm_image_image s ▸ h.symm.uniqueMDiffOn_image_aux hn hs,
    h.uniqueMDiffOn_image_aux hn⟩

Premises used: Diffeomorph.symm, Eq.rec, Diffeomorph.symm_image_image, Diffeomorph.uniqueMDiffOn_image_aux, Iff.intro
-- 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
s : Set N
⊢ UniqueMDiffOn.{u_1, u_2, u_5, u_9} I (M := M) ((⇑h : (a : M) → N) ⁻¹' s) ↔ UniqueMDiffOn J s

Tactic:
h.symm_image_eq_preimage s ▸ h.symm.uniqueMDiffOn_image hn

Premises used: Diffeomorph.symm, Eq.rec, Diffeomorph.uniqueMDiffOn_image, Diffeomorph.symm_image_eq_preimage
-- 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
n : ℕ∞ω
h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
hn : n ≠ 0
s : Set E
⊢ UniqueDiffOn.{u_1, u_4} 𝕜 (E := F) ((⇑h : (a : E) → F) '' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
simp only [← uniqueMDiffOn_iff_uniqueDiffOn, uniqueMDiffOn_image _ hn]

Premises used: Diffeomorph.uniqueMDiffOn_image, uniqueMDiffOn_iff_uniqueDiffOn
-- 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
n : ℕ∞ω
h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
hn : n ≠ 0
s : Set F
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) ((⇑h : (a : E) → F) ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
h.symm_image_eq_preimage s ▸ h.symm.uniqueDiffOn_image hn

Premises used: Diffeomorph.symm, Eq.rec, Diffeomorph.uniqueDiffOn_image, Diffeomorph.symm_image_eq_preimage
-- 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'
e : E ≃L[𝕜] E'
⊢ Eq (α := (a : E) → E') (⇑e.toDiffeomorph : (a : E) → E') (⇑e : (a : E) → E')

Tactic:
rfl

Premises used: 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'
e : E ≃L[𝕜] E'
⊢ e.symm.toDiffeomorph = e.toDiffeomorph.symm

Tactic:
rfl

Premises used: Diffeomorph.symm, ContinuousLinearEquiv.toDiffeomorph, 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
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
e : E ≃L[𝕜] E'
⊢ Eq (α := (a : E') → E) (⇑e.toDiffeomorph.symm : (a : E') → E) (⇑e.symm : (a : E') → E)

Tactic:
rfl

Premises used: 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 : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ (I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv).source = univ

Tactic:
simp
-- 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 : E ≃L[𝕜] E'
pos :
  ∀ (h : IsRCLikeNormedField 𝕜),
    Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))
neg :
  ∀ (h : ¬IsRCLikeNormedField 𝕜), range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E') = univ
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))
  else range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E') = univ

Tactic:
split_ifs with h
-- 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 : E ≃L[𝕜] E'
h : IsRCLikeNormedField 𝕜
pos : Convex.{0, u_3} ℝ (E := E') (range ((⇑e : (a : E) → E') ∘ (↑I : H → E)))
⊢ Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))

Tactic:
simp only [PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply, LinearEquiv.coe_toEquiv,
      ContinuousLinearEquiv.coe_toLinearEquiv, toPartialEquiv_coe]

Premises used: LinearEquiv.coe_toEquiv, Equiv.toPartialEquiv_apply, ModelWithCorners.toPartialEquiv_coe, ContinuousLinearEquiv.coe_toLinearEquiv, PartialEquiv.coe_trans