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'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
s : Set M
x : M
⊢ ContMDiffWithinAt.{u_1, u_2, u_5, u_9, u_3, u_6, u_10} I I' (M' := M') n (⇑h : (a : M) → M') s x

Tactic:
h.contMDiffAt.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, Diffeomorph.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'
n : ℕ∞ω
h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (E := E) (F := E') n (⇑h : (a : E) → E')

Tactic:
h.contMDiff.contDiff

Premises used: ContMDiff.contDiff, Diffeomorph.contMDiff
-- 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
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
hn : n ≠ 0
⊢ MDiff (⇑h : (a : M) → M')

Tactic:
h.contMDiff.mdifferentiable hn

Premises used: ContMDiff.mdifferentiable, Diffeomorph.contMDiff
-- 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
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
s : Set M
hn : n ≠ 0
⊢ MDiff[s] (⇑h : (a : M) → M')

Tactic:
(h.mdifferentiable hn).mdifferentiableOn

Premises used: Diffeomorph.mdifferentiable, MDifferentiable.mdifferentiableOn
-- 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
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
⊢ Eq (α := (a : M) → M') (⇑h.toEquiv : (a : M) → M') (⇑h : (a : M) → M')

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'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
⊢ Eq (α := (a : M) → M') (⇑(↑h : C^n⟮I, M; I', M'⟯) : (a : M) → M') (⇑h : (a : M) → M')

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'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h h' : M ≃ₘ^n⟮I, I'⟯ M'
⊢ h.toEquiv = h'.toEquiv ↔ h = h'

Tactic:
toEquiv_injective.eq_iff

Premises used: Diffeomorph.toEquiv_injective, Function.Injective.eq_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'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
⊢ Injective (α := M ≃ₘ^n⟮I, I'⟯ M') (β := (a : M) → M') (DFunLike.coe (β := fun (x : M) ↦ M'))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- 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
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h h' : M ≃ₘ^n⟮I, I'⟯ M'
Heq : ∀ (x : M), Eq.{u_10 + 1} (α := M') ((h : (a : M) → M') x : M') ((h' : (a : M) → M') x : M')
⊢ h = h'

Tactic:
coeFn_injective <| funext Heq

Premises used: Diffeomorph.coeFn_injective, funext
-- 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 : ℕ∞ω
⊢ toEquiv (Diffeomorph.refl I M n) = Equiv.refl M

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- 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 : ℕ∞ω
⊢ Eq (α := (a : M) → M) (⇑(Diffeomorph.refl I M n) : (a : M) → M) id

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'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
⊢ h.trans (Diffeomorph.refl I' M' n) = h

Tactic:
ext fun _ => rfl

Premises used: Diffeomorph.ext, 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
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_10
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
n : ℕ∞ω
h : M ≃ₘ^n⟮I, I'⟯ M'
⊢ Diffeomorph.trans (Diffeomorph.refl I M n) h = h

Tactic:
ext fun _ => rfl

Premises used: Diffeomorph.ext, 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
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 : ℕ∞ω
h₁ : M ≃ₘ^n⟮I, I'⟯ M'
h₂ : M' ≃ₘ^n⟮I', J⟯ N
⊢ Eq (α := (a : M) → N) (⇑(h₁.trans h₂) : (a : M) → N)
    (comp.{u_9 + 1, u_10 + 1, u_11 + 1} (β := M') (⇑h₂ : (a : M') → N) (⇑h₁ : (a : M) → M'))

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
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
x : N
⊢ (h : (a : M) → N) ((h.symm : (a : N) → M) x : M) = x

Tactic:
h.toEquiv.apply_symm_apply x

Premises used: Equiv.apply_symm_apply, Diffeomorph.toEquiv
-- 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
x : M
⊢ (h.symm : (a : N) → M) ((h : (a : M) → N) x : N) = x

Tactic:
h.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, Diffeomorph.toEquiv
-- 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 : ℕ∞ω
⊢ Eq (α := M ≃ₘ^n⟮I, I⟯ M) (Diffeomorph.symm (Diffeomorph.refl I M n)) (Diffeomorph.refl I M n)

Tactic:
ext fun _ => rfl

Premises used: Diffeomorph.ext, 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
⊢ h.trans h.symm = Diffeomorph.refl I M n

Tactic:
ext h.symm_apply_apply

Premises used: Diffeomorph.symm_apply_apply, Diffeomorph.ext
-- 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
⊢ h.symm.trans h = Diffeomorph.refl J N n

Tactic:
ext h.apply_symm_apply

Premises used: Diffeomorph.apply_symm_apply, Diffeomorph.ext
-- 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 : ℕ∞ω
h₁ : M ≃ₘ^n⟮I, I'⟯ M'
h₂ : M' ≃ₘ^n⟮I', J⟯ N
⊢ (h₁.trans h₂).symm = h₂.symm.trans h₁.symm

Tactic:
rfl

Premises used: Equiv.trans, Diffeomorph.trans, 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
⊢ h.symm.toEquiv = h.symm

Tactic:
rfl

Premises used: 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
⊢ Eq (α := (a : N) → M) (⇑h.symm : (a : N) → M) (⇑h.symm : (a : N) → M)

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
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
s : Set M
⊢ Eq.{u_11 + 1} (α := Set N) ((⇑h : (a : M) → N) '' s) ((⇑h.symm : (a : N) → M) ⁻¹' s)

Tactic:
h.toEquiv.image_eq_preimage_symm s

Premises used: Diffeomorph.toEquiv, Equiv.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
s : Set N
⊢ Eq.{u_9 + 1} (α := Set M) ((⇑h.symm : (a : N) → M) '' s) ((⇑h : (a : M) → N) ⁻¹' s)

Tactic:
h.symm.image_eq_preimage_symm s

Premises used: Diffeomorph.symm, 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 : ℕ∞ω
α : Sort u_13
h : M ≃ₘ^n⟮I, J⟯ N
f : α → M
rw : Eq.{u_11 + 1} (α := Set N) ((⇑h : (a : M) → N) '' range f) ((⇑h.symm : (a : N) → M) ⁻¹' range f)
rw₁ rw₂ : Eq.{u_11 + 1} (α := Set N) ((⇑h.symm : (a : N) → M) ⁻¹' range f) ((⇑h.symm : (a : N) → M) ⁻¹' range f)
⊢ Eq.{u_11 + 1} (α := Set N) (range ((⇑h : (a : M) → N) ∘ f)) ((⇑h.symm : (a : N) → M) ⁻¹' range f)

Tactic:
rw [range_comp, image_eq_preimage_symm]

Premises used: Diffeomorph.image_eq_preimage_symm, Diffeomorph.range_comp
-- 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
s : Set N
⊢ image.{u_9, u_11} (α := M) (⇑h : (a : M) → N) ((⇑h.symm : (a : N) → M) '' s) = s

Tactic:
h.toEquiv.image_symm_image s

Premises used: Diffeomorph.toEquiv, Equiv.image_symm_image
-- 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
s : Set M
⊢ image.{u_11, u_9} (α := N) (⇑h.symm : (a : N) → M) ((⇑h : (a : M) → N) '' s) = s

Tactic:
h.toEquiv.symm_image_image s

Premises used: Diffeomorph.toEquiv, Equiv.symm_image_image
-- 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
⊢ h.toHomeomorph.toEquiv = h.toEquiv

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
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
⊢ h.symm.toHomeomorph = h.toHomeomorph.symm

Tactic:
rfl

Premises used: Diffeomorph.toHomeomorph, Homeomorph.symm, 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 : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
⊢ Eq (α := (a : M) → N) (⇑h.toHomeomorph : (a : M) → N) (⇑h : (a : M) → N)

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
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
⊢ Eq (α := (a : N) → M) (⇑h.toHomeomorph.symm : (a : N) → M) (⇑h.symm : (a : N) → M)

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
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
mp :
  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)
mpr :
  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
⊢ 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)

Tactic:
constructor
-- 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 x
⊢ ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s ((h.symm : (a : N) → M) ((h : (a : M) → N) x : N))

Tactic:
rw [← h.symm_apply_apply x] at Hfh

Premises used: Diffeomorph.symm_apply_apply