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

Tactic:
rw [range_comp]

Premises used: Set.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
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 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
eR : E →L[ℝ] E' := ContinuousLinearMap.restrictScalars ℝ (↑e : E →L[𝕜] E')
pos : Convex.{0, u_3} ℝ (E := E') ((⇑eR : (a : E) → E') '' range (↑I : H → E))
⊢ Convex.{0, u_3} ℝ (E := E') ((⇑e : (a : E) → E') '' range (↑I : H → E))

Tactic:
change Convex ℝ (⇑eR '' range ↑I)

Premises used: Real, ModelWithCorners.toFun', Convex, Set.image, Set.range, DFunLike.coe
-- 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 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
eR : E →L[ℝ] E' := ContinuousLinearMap.restrictScalars ℝ (↑e : E →L[𝕜] E')
⊢ Convex.{0, u_3} ℝ (E := E') ((⇑eR : (a : E) → E') '' range (↑I : H → E))

Tactic:
apply I.convex_range.linear_image

Premises used: Convex.linear_image, ModelWithCorners.convex_range
-- 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 𝕜
⊢ range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E') = univ

Tactic:
simp [range_eq_univ_of_not_isRCLikeNormedField I h, range_comp]

Premises used: Set.range_comp, ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField
-- 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'
simp : Set.Nonempty.{u_3} (α := E') (interior ((⇑e.symm : (a : E') → E) ⁻¹' range (↑I : H → E)))
⊢ (interior (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))).Nonempty

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

Premises used: LinearEquiv.coe_toEquiv, Set.range_comp, Equiv.toPartialEquiv_apply, ModelWithCorners.toPartialEquiv_coe, ContinuousLinearEquiv.coe_toLinearEquiv, ContinuousLinearEquiv.image_eq_preimage_symm, PartialEquiv.coe_trans
-- 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'
apply : Set.Nonempty.{u_3} (α := E') ((⇑e.symm : (a : E') → E) ⁻¹' interior (range (↑I : H → E)))
⊢ Set.Nonempty.{u_3} (α := E') (interior ((⇑e.symm : (a : E') → E) ⁻¹' range (↑I : H → E)))

Tactic:
apply Nonempty.mono (preimage_interior_subset_interior_preimage e.symm.continuous)

Premises used: ContinuousLinearEquiv.symm, preimage_interior_subset_interior_preimage, Set.Nonempty.mono, ContinuousLinearEquiv.continuous
-- 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'
rw : Set.Nonempty.{u_3} (α := E') ((⇑e : (a : E) → E') '' interior (range (↑I : H → E)))
⊢ Set.Nonempty.{u_3} (α := E') ((⇑e.symm : (a : E') → E) ⁻¹' interior (range (↑I : H → E)))

Tactic:
rw [← ContinuousLinearEquiv.image_eq_preimage_symm]

Premises used: ContinuousLinearEquiv.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
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'
⊢ Set.Nonempty.{u_3} (α := E') ((⇑e : (a : E) → E') '' interior (range (↑I : H → E)))

Tactic:
simpa using I.nonempty_interior

Premises used: ModelWithCorners.nonempty_interior
-- 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
e : E ≃L[𝕜] E'
⊢ (↑(I.transContinuousLinearEquiv e) : H → E') = (⇑e : (a : E) → E') ∘ (↑I : H → E)

Tactic:
rfl

Premises used: ModelWithCorners.toFun', 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
e : E ≃L[𝕜] E'
⊢ (↑(I.transContinuousLinearEquiv e).symm : E' → H) = (↑I.symm : E → H) ∘ (⇑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'
H : Type u_5
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
e : E ≃L[𝕜] E'
⊢ range (↑(I.transContinuousLinearEquiv e) : H → E') = (⇑e : (a : E) → E') '' range (↑I : H → E)

Tactic:
range_comp e I

Premises used: Set.range_comp, ModelWithCorners.toFun', DFunLike.coe
-- 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
e : E ≃L[𝕜] E'
x : M
⊢ (↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → E') = (⇑e : (a : E) → E') ∘ (↑(extChartAt I x) : M → 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'
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
e : E ≃L[𝕜] E'
x : M
⊢ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : E' → M) =
    (↑(extChartAt I x).symm : E → M) ∘ (⇑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'
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
e : E ≃L[𝕜] E'
x : M
⊢ (extChartAt (I.transContinuousLinearEquiv e) x).target = (⇑e.symm : (a : E') → E) ⁻¹' (extChartAt I x).target

Tactic:
simp only [range_comp, preimage_preimage, ContinuousLinearEquiv.image_eq_preimage_symm,
    mfld_simps, ← comp_def]

Premises used: Set.range_comp, Set.preimage_preimage, Function.comp_def, ContinuousLinearEquiv.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
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[𝕜] F
inst_19 : IsManifold I n M
⊢ IsManifold (I.transContinuousLinearEquiv e) n M

Tactic:
isManifold_of_contDiffOn (I.transContinuousLinearEquiv e) n M fun e₁ e₂ h₁ h₂ => ?_

Premises used: isManifold_of_contDiffOn, ModelWithCorners.transContinuousLinearEquiv
-- 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[𝕜] F
inst_19 : IsManifold I n M
refine :
  ∀ (e₁ e₂ : OpenPartialHomeomorph M H) (h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₁)
    (h₂ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₂),
    ContDiffOn 𝕜 n
      ((↑(I.transContinuousLinearEquiv e) : H → F) ∘
        (↑(e₁.symm ≫ₕ e₂) : H → H) ∘ (↑(I.transContinuousLinearEquiv e).symm : F → H))
      ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
        range (↑(I.transContinuousLinearEquiv e) : H → F))
⊢ IsManifold (I.transContinuousLinearEquiv e) n M

Tactic:
refine isManifold_of_contDiffOn (I.transContinuousLinearEquiv e) n M fun e₁ e₂ h₁ h₂ => ?_

Premises used: isManifold_of_contDiffOn, ModelWithCorners.transContinuousLinearEquiv
-- 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[𝕜] F
inst_19 : IsManifold I n M
e₁ e₂ : OpenPartialHomeomorph M H
h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₁
h₂ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₂
⊢ ContDiffOn 𝕜 n
    ((↑(I.transContinuousLinearEquiv e) : H → F) ∘
      (↑(e₁.symm ≫ₕ e₂) : H → H) ∘ (↑(I.transContinuousLinearEquiv e).symm : F → H))
    ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
      range (↑(I.transContinuousLinearEquiv e) : H → F))

Tactic:
e.contDiff.comp_contDiffOn
      (((contDiffGroupoid n I).compatible h₁ h₂).1.comp e.symm.contDiff.contDiffOn ?_)

Premises used: ContDiff.comp_contDiffOn, ContinuousLinearEquiv.symm, ContDiff.contDiffOn, ContDiffOn.comp, contDiffGroupoid, ModelWithCorners.toFun', StructureGroupoid.compatible, And.left, ContinuousLinearEquiv.contDiff
-- 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[𝕜] F
inst_19 : IsManifold I n M
e₁ e₂ : OpenPartialHomeomorph M H
h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₁
h₂ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₂
refine :
  MapsTo (↑((↑e : E ≃ₗ[𝕜] F).toEquiv.toPartialEquiv.restr I.target).symm : F → E)
    ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
      range (↑(I.transContinuousLinearEquiv e) : H → F))
    ((↑I.symm : E → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩ range (↑I : H → E))
⊢ ContDiffOn 𝕜 n
    ((↑(I.transContinuousLinearEquiv e) : H → F) ∘
      (↑(e₁.symm ≫ₕ e₂) : H → H) ∘ (↑(I.transContinuousLinearEquiv e).symm : F → H))
    ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
      range (↑(I.transContinuousLinearEquiv e) : H → F))

Tactic:
refine e.contDiff.comp_contDiffOn
      (((contDiffGroupoid n I).compatible h₁ h₂).1.comp e.symm.contDiff.contDiffOn ?_)

Premises used: ContDiff.comp_contDiffOn, ContinuousLinearEquiv.symm, ContDiff.contDiffOn, ContDiffOn.comp, contDiffGroupoid, StructureGroupoid.compatible, And.left, ContinuousLinearEquiv.contDiff
-- 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[𝕜] F
inst_19 : IsManifold I n M
e₁ e₂ : OpenPartialHomeomorph M H
h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₁
h₂ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₂
⊢ MapsTo (↑((↑e : E ≃ₗ[𝕜] F).toEquiv.toPartialEquiv.restr I.target).symm : F → E)
    ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
      range (↑(I.transContinuousLinearEquiv e) : H → F))
    ((↑I.symm : E → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩ range (↑I : H → E))

Tactic:
simp [preimage_comp, range_comp, mapsTo_iff_subset_preimage,
    ContinuousLinearEquiv.image_eq_preimage_symm]

Premises used: Set.mapsTo_iff_subset_preimage, Set.range_comp, Set.preimage_comp, ContinuousLinearEquiv.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
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
⊢ ContMDiffAt I (I.transContinuousLinearEquiv e) (M' := M) n (⇑(Equiv.refl M) : (a : M) → M) x

Tactic:
contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, ?_⟩

Premises used: Iff.mpr, continuousWithinAt_id, contMDiffWithinAt_iff', And.intro, ContMDiffAt