awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
g : M' → M''
p : TangentBundle I M
hg : MDifferentiableAt I' I'' g (f (p.proj (E := TangentSpace I)))
hf : MDifferentiableAt I I' f (p.proj (E := TangentSpace I))
simp :
  Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderiv I I'' (g ∘ f) (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I'' ((g ∘ f) (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I'' (g (f p.proj)))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderiv I' I'' g (f (p.proj (E := TangentSpace I))) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f (p.proj (E := TangentSpace I))))
              (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
          (a : TangentSpace I' (f p.proj)) → TangentSpace I'' (g (f p.proj)))
        (((mfderiv I I' f (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
          (p.snd (E := TangentSpace I))) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
⊢ Eq (α := TangentBundle I'' M'') (tangentMap I I'' (g ∘ f) p) (tangentMap I' I'' g (tangentMap I I' f p))

Tactic:
simp only [tangentMap, mfld_simps]

Premises used: tangentMap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
g : M' → M''
p : TangentBundle I M
hg : MDifferentiableAt I' I'' g (f (p.proj (E := TangentSpace I)))
hf : MDifferentiableAt I I' f (p.proj (E := TangentSpace I))
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I' (f (p.proj (E := TangentSpace I))))
              (mfderiv I' I'' g (f (p.proj (E := TangentSpace I)))) (mfderiv I I' f (p.proj (E := TangentSpace I))) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
          (a : TangentSpace I p.proj) → TangentSpace I'' (g (f p.proj)))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderiv I' I'' g (f (p.proj (E := TangentSpace I))) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f (p.proj (E := TangentSpace I))))
              (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
          (a : TangentSpace I' (f p.proj)) → TangentSpace I'' (g (f p.proj)))
        (((mfderiv I I' f (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
          (p.snd (E := TangentSpace I))) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiable I I' f
h :
  ∀ (p : TangentBundle I M),
    Eq (α := TangentBundle I'' M'') (tangentMap I I'' (g ∘ f) p)
      (Function.comp (β := TangentBundle I' M') (tangentMap I' I'' g) (tangentMap I I' f) p)
⊢ Eq (α := TangentBundle I M → TangentBundle I'' M'') (tangentMap I I'' (g ∘ f))
    (Function.comp (β := TangentBundle I' M') (tangentMap I' I'' g) (tangentMap I I' f))

Tactic:
ext p : 1
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiable I I' f
p : TangentBundle I M
⊢ Eq (α := TangentBundle I'' M'') (tangentMap I I'' (g ∘ f) p)
    (Function.comp (β := TangentBundle I' M') (tangentMap I' I'' g) (tangentMap I I' f) p)

Tactic:
tangentMap_comp_at _ (hg _) (hf _)

Premises used: tangentMap_comp_at, tangentMap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiable I I' f
p : TangentBundle I M
⊢ Eq (α := TangentBundle I'' M'') (tangentMap I I'' (g ∘ f) p)
    (Function.comp (β := TangentBundle I' M') (tangentMap I' I'' g) (tangentMap I I' f) p)

Tactic:
exact tangentMap_comp_at _ (hg _) (hf _)

Premises used: tangentMap_comp_at
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
simp_rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₁ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₂ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ univ) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₃ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₄ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ id) (id ⁻¹' s) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₅ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) (id ⁻¹' s) (id x) ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₆ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) (id s) (id x) ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x

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

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

Tactic:
differentiableWithinAtProp_self_source

Premises used: ModelWithCorners.toFun', differentiableWithinAtProp_self_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
f : H → E'
s : Set H
x : H
⊢ DifferentiableWithinAtProp I 𝓘(𝕜, E') f s x ↔
    DifferentiableWithinAt 𝕜 (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
Iff.rfl

Premises used: Iff.rfl, ModelWithCorners.toFun', DifferentiableWithinAtProp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
⊢ (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u

Tactic:
simp only [Set.inter_right_comm, Set.preimage_inter]

Premises used: Set.preimage_inter, Set.inter_right_comm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
⊢ (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u

Tactic:
have : I.symm ⁻¹' (s ∩ u) ∩ Set.range I = I.symm ⁻¹' s ∩ Set.range I ∩ I.symm ⁻¹' u := by
        simp only [Set.inter_right_comm, Set.preimage_inter]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x)
⊢ DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x

Tactic:
rw [DifferentiableWithinAtProp, DifferentiableWithinAtProp, this]

Premises used: DifferentiableWithinAtProp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
symm :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x)
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x)

Tactic:
symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
ht : (↑I.symm : E → H) ⁻¹' u ∈ 𝓝 ((↑I : H → E) x)
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x)

Tactic:
apply differentiableWithinAt_inter

Premises used: differentiableWithinAt_inter
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
rw : u ∈ 𝓝 x
⊢ u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))

Tactic:
rw [ModelWithCorners.left_inv]

Premises used: ModelWithCorners.left_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ u ∈ 𝓝 x

Tactic:
u_open.mem_nhds xu

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ u ∈ 𝓝 x

Tactic:
exact u_open.mem_nhds xu

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))

Tactic:
have : u ∈ 𝓝 (I.symm (I x)) := by
        rw [ModelWithCorners.left_inv]
        exact u_open.mem_nhds xu
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this_1 :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
this : u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))
⊢ (↑I.symm : E → H) ⁻¹' u ∈ 𝓝 ((↑I : H → E) x)

Tactic:
apply I.continuous_symm.continuousAt this

Premises used: Continuous.continuousAt, ModelWithCorners.continuous_symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAtProp I I' f s x
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)

Tactic:
rw [DifferentiableWithinAtProp] at h ⊢

Premises used: DifferentiableWithinAtProp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
⊢ (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
⊢ (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
have : I x = (I ∘ e.symm ∘ I.symm) (I (e x)) := by simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))

Tactic:
rw [this] at h
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
h₁ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
⊢ (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))

Tactic:
rw [this] at h