awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 1 ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
h₁ :
  (↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)
convert! :
  MapsTo ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
convert! (this.differentiableWithinAt one_ne_zero).comp _ h _

Premises used: DifferentiableWithinAt.comp, one_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 1 ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
h₁ :
  ∀ (y : E),
    ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H)) y =
      (((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y
⊢ (↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)

Tactic:
ext y
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 1 ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
y : E
⊢ ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H)) y =
    (((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y

Tactic:
simp only [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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 1 ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)

Tactic:
simp only [mfld_simps] at hy
-- 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'
hs : s ⊆ f ⁻¹' e'.source
hx : f 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)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 1 ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
y : E
hy : (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)
⊢ ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y ∈ (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')

Tactic:
simpa only [hy, mfld_simps] using hs hy.1

Premises used: And.left
-- 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
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'
f : M → M'
s : Set M
x : M
rw :
  ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I'
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ MDifferentiableWithinAt I I' f s x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [MDifferentiableWithinAt, liftPropWithinAt_iff']

Premises used: MDifferentiableWithinAt, ChartedSpace.liftPropWithinAt_iff'
-- 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
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'
f : M → M'
s : Set M
x : M
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I'
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
rfl
-- 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
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'
f : M → M'
s : Set M
x : M
hf : MDifferentiableWithinAt I I' f s x
⊢ ContinuousWithinAt f s x

Tactic:
mdifferentiableWithinAt_iff' .. |>.1 hf |>.1

Premises used: mdifferentiableWithinAt_iff', And.left, Iff.mp
-- 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
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'
f : M → M'
s : Set M
x : M
hf : MDifferentiableWithinAt I I' f s x
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
mdifferentiableWithinAt_iff' .. |>.1 hf |>.2

Premises used: mdifferentiableWithinAt_iff', And.right, Iff.mp
-- 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
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'
f : M → M'
x : M
rw :
  ContinuousAt f x ∧
      DifferentiableWithinAtProp I I'
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ MDifferentiableAt I I' f x ↔
    ContinuousAt f x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [MDifferentiableAt, liftPropAt_iff]

Premises used: MDifferentiableAt, ChartedSpace.liftPropAt_iff
-- 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
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'
f : M → M'
x : M
a :
  DifferentiableWithinAtProp I I'
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
      ((↑(chartAt H x) : M → H) x) ↔
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousAt f x ∧
      DifferentiableWithinAtProp I I'
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
congrm _ ∧ ?_
-- 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
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'
f : M → M'
x : M
⊢ DifferentiableWithinAtProp I I'
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
      ((↑(chartAt H x) : M → H) x) ↔
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
simp [DifferentiableWithinAtProp, Set.univ_inter, Function.comp_assoc]

Premises used: Set.univ_inter, DifferentiableWithinAtProp, Function.comp_assoc
-- 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
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'
f : M → M'
x : M
hf : MDifferentiableAt I I' f x
⊢ ContinuousAt f x

Tactic:
mdifferentiableAt_iff .. |>.1 hf |>.1

Premises used: mdifferentiableAt_iff, And.left, Iff.mp
-- 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
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'
f : M → M'
x : M
hf : MDifferentiableAt I I' f x
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
mdifferentiableAt_iff .. |>.1 hf |>.2

Premises used: mdifferentiableAt_iff, And.right, Iff.mp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) s x ↔ UniqueDiffWithinAt 𝕜 s x

Tactic:
simp only [UniqueMDiffWithinAt, mfld_simps]

Premises used: UniqueMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ UniqueMDiffOn 𝓘(𝕜, E) s ↔ UniqueDiffOn 𝕜 s

Tactic:
simp [UniqueMDiffOn, UniqueDiffOn, uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]

Premises used: UniqueDiffOn, UniqueMDiffOn, uniqueMDiffWithinAt_iff_uniqueDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ UniqueMDiffOn 𝓘(𝕜, E) (Set.range (↑I : H → E))

Tactic:
I.uniqueDiffOn.uniqueMDiffOn

Premises used: UniqueDiffOn.uniqueMDiffOn, ModelWithCorners.uniqueDiffOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
x : E
⊢ writtenInExtChartAt 𝓘(𝕜, E) 𝓘(𝕜, E') x f = f

Tactic:
rfl

Premises used: writtenInExtChartAt, rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
s : Set E
x : E
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))
⊢ HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f' ↔ HasFDerivWithinAt f f' s x

Tactic:
simpa only [HasMFDerivWithinAt, and_iff_right_iff_imp, mfld_simps] using
    HasFDerivWithinAt.continuousWithinAt

Premises used: and_iff_right_iff_imp, HasFDerivWithinAt.continuousWithinAt, HasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
x : E
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))
rw : HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x f' ↔ HasFDerivAt f f' x
rw₁ : HasFDerivWithinAt f f' Set.univ x ↔ HasFDerivAt f f' x
rw₂ rw₃ : HasFDerivAt f f' x ↔ HasFDerivAt f f' x
⊢ HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x

Tactic:
rw [← hasMFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_univ]

Premises used: hasMFDerivWithinAt_univ, hasFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
s : Set E
x : E
simp : ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f s x
⊢ MDiffAt[s] f x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [mdifferentiableWithinAt_iff', mfld_simps]

Premises used: mdifferentiableWithinAt_iff'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
s : Set E
x : E
⊢ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨fun H => H.2, fun H => ⟨H.continuousWithinAt, H⟩⟩

Premises used: DifferentiableWithinAt.continuousWithinAt, And.right, And.intro, Iff.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
s : Set E
x : E
⊢ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact ⟨fun H => H.2, fun H => ⟨H.continuousWithinAt, H⟩⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
x : E
simp : ContinuousAt f x ∧ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x
⊢ MDiffAt f x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [mdifferentiableAt_iff, differentiableWithinAt_univ, mfld_simps]

Premises used: mdifferentiableAt_iff, differentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
x : E
⊢ ContinuousAt f x ∧ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x

Tactic:
⟨fun H => H.2, fun H => ⟨H.continuousAt, H⟩⟩

Premises used: DifferentiableAt.continuousAt, And.right, And.intro, Iff.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
x : E
⊢ ContinuousAt f x ∧ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x

Tactic:
exact ⟨fun H => H.2, fun H => ⟨H.continuousAt, H⟩⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
s : Set E
⊢ MDiff[s] f ↔ DifferentiableOn 𝕜 f s

Tactic:
simp only [MDifferentiableOn, DifferentiableOn,
    mdifferentiableWithinAt_iff_differentiableWithinAt]

Premises used: mdifferentiableWithinAt_iff_differentiableWithinAt, MDifferentiableOn, DifferentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
⊢ MDiff f ↔ Differentiable 𝕜 f

Tactic:
simp only [MDifferentiable, Differentiable, mdifferentiableAt_iff_differentiableAt]

Premises used: Differentiable, mdifferentiableAt_iff_differentiableAt, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
s : Set E
x : E
pos :
  ∀ (h : MDiffAt[s] f x),
    Eq (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
      (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
neg :
  ∀ (h : ¬MDiffAt[s] f x),
    Eq (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
      (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)

Tactic:
by_cases h : MDiffAt[s] f x

Premises used: modelWithCornersSelf, MDifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
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 : E → E'
s : Set E
x : E
h : MDiffAt[s] f x
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)

Tactic:
simp only [mfderivWithin, h, if_pos, mfld_simps]

Premises used: mfderivWithin, if_pos