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

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

Premises used: Iff.mpr, continuousWithinAt_id, contMDiffWithinAt_iff', And.intro
-- 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
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
      ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M))
    ((extChartAt I x).target ∩
      (↑(extChartAt I x).symm : E → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_4} (β := F)
                (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
              Set M)))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
e.contDiff.contDiffWithinAt.congr_of_mem (fun y hy ↦ ?_) ?_

Premises used: ContDiff.contDiffWithinAt, ContDiffWithinAt.congr_of_mem, 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_1 e : E ≃L[𝕜] F
x : M
refine_1 :
  ∀ (y : E)
    (hy :
      y ∈
        (extChartAt I x).target ∩
          (↑(extChartAt I x).symm : E → M) ⁻¹'
            (univ ∩
              preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
                (PartialEquiv.source.{u_9, u_4} (β := F)
                    (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
                  Set M))),
    comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
        ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M) y =
      (e : (a : E) → F) y
refine_2 :
  (↑(extChartAt I x) : M → E) x ∈
    (extChartAt I x).target ∩
      (↑(extChartAt I x).symm : E → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_4} (β := F)
                (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
              Set M))
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
      ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M))
    ((extChartAt I x).target ∩
      (↑(extChartAt I x).symm : E → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_4} (β := F)
                (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
              Set M)))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
refine e.contDiff.contDiffWithinAt.congr_of_mem (fun y hy ↦ ?_) ?_

Premises used: ContDiff.contDiffWithinAt, ContDiffWithinAt.congr_of_mem, 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_1 e : E ≃L[𝕜] F
x : M
y : E
hy :
  y ∈
    (extChartAt I x).target ∩
      (↑(extChartAt I x).symm : E → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_4} (β := F)
                (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
              Set M))
⊢ comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
      ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M) y =
    (e : (a : E) → F) y

Tactic:
simp only [Equiv.coe_refl, id, (· ∘ ·), I.coe_extChartAt_transContinuousLinearEquiv,
        (extChartAt I x).right_inv hy.1]

Premises used: extChartAt, Function.comp, id, PartialEquiv.right_inv, And.left, Equiv.coe_refl, ModelWithCorners.coe_extChartAt_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_1 e : E ≃L[𝕜] F
x : M
⊢ Membership.mem (γ := Set M)
    (preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
      (PartialEquiv.source.{u_9, u_4} (β := F)
          (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
        Set M))
    ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))

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

Tactic:
exact
      ⟨(extChartAt I x).map_source (mem_extChartAt_source x), trivial, by simp only [mfld_simps]⟩
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
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.transContinuousLinearEquiv e) I (M' := M) n (⇑(Equiv.refl M).symm : (a : M) → M) x

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

Premises used: Iff.mpr, continuousWithinAt_id, contMDiffWithinAt_iff', And.intro, 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
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
refine :
  ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M))
    ((extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M)))
    ((↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x)
⊢ ContMDiffAt (I.transContinuousLinearEquiv e) I (M' := M) n (⇑(Equiv.refl M).symm : (a : M) → M) x

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

Premises used: Iff.mpr, continuousWithinAt_id, contMDiffWithinAt_iff', And.intro
-- 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
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M))
    ((extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M)))
    ((↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x)

Tactic:
e.symm.contDiff.contDiffWithinAt.congr_of_mem (fun y hy => ?_) ?_

Premises used: ContinuousLinearEquiv.symm, ContDiff.contDiffWithinAt, ContDiffWithinAt.congr_of_mem, 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_1 e : E ≃L[𝕜] F
x : M
refine_1 :
  ∀ (y : F)
    (hy :
      y ∈
        (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
          (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
            (univ ∩
              preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
                (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) :
                  Set M))),
    comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
        ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M)
        y =
      (e.symm : (a : F) → E) y
refine_2 :
  (↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x ∈
    (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M))
    ((extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M)))
    ((↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x)

Tactic:
refine e.symm.contDiff.contDiffWithinAt.congr_of_mem (fun y hy => ?_) ?_

Premises used: ContinuousLinearEquiv.symm, ContDiff.contDiffWithinAt, ContDiffWithinAt.congr_of_mem, 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_1 e : E ≃L[𝕜] F
x : M
y : F
hy :
  y ∈
    (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))
⊢ Membership.mem (γ := Set F) ((⇑e.symm : (a : F) → E) ⁻¹' (extChartAt I x).target) y ∧
    y ∈
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))

Tactic:
simp only [mem_inter_iff, I.extChartAt_transContinuousLinearEquiv_target] at hy

Premises used: Set.mem_inter_iff, ModelWithCorners.extChartAt_transContinuousLinearEquiv_target
-- 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
y : F
hy :
  Membership.mem (γ := Set F) ((⇑e.symm : (a : F) → E) ⁻¹' (extChartAt I x).target) y ∧
    y ∈
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))
⊢ comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M)
      y =
    (e.symm : (a : F) → E) y

Tactic:
simp only [Equiv.coe_refl, Equiv.refl_symm, id, (· ∘ ·),
        I.coe_extChartAt_transContinuousLinearEquiv_symm, (extChartAt I x).right_inv hy.1]

Premises used: extChartAt, Function.comp, id, Equiv.refl_symm, PartialEquiv.right_inv, ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv_symm, And.left, Equiv.coe_refl
-- 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
⊢ Membership.mem (γ := Set M)
    (preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
      (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))
    ((↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M)
      ((↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x))

Tactic:
simp only [e.symm_apply_apply, Equiv.refl_symm, Equiv.coe_refl, mfld_simps]

Premises used: Equiv.refl_symm, Equiv.coe_refl, ContinuousLinearEquiv.symm_apply_apply