awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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_8
inst_9 : TopologicalSpace M''
inst_10 : ChartedSpace H' M''
s : Set M
inst_11 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ (extChartAt I' y).source ∈ nhds (f z)

Tactic:
exact (isOpen_extChartAt_source y).mem_nhds hz.2

Premises used: isOpen_extChartAt_source, And.right, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
this :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
w : F := ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2
fst :
  ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).1 =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w).1
snd :
  ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2 =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w).2
⊢ (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
this :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
w : F := ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2
⊢ ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).1 =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w).1

Tactic:
simp [FiberBundle.chartedSpace_chartAt]

Premises used: FiberBundle.chartedSpace_chartAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
this :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
w : F := ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2
⊢ ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2 =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w).2

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
this :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
w : F := ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2
⊢ (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)

Tactic:
have A : extChartAt (I.prod 𝓘(𝕜, F)) p p = (extChartAt I p.1 p.1, w) := by
      ext
      · simp [FiberBundle.chartedSpace_chartAt]
      · rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
this :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
w : F := ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2
A :
  (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)
simp :
  UniqueDiffWithinAt 𝕜
    ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F))
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj (E := Z) ⁻¹' s) p

Tactic:
simp only [UniqueMDiffWithinAt, A] at hs ⊢

Premises used: UniqueMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs :
  UniqueDiffWithinAt 𝕜 ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
this :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
w : F := ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2
A :
  (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)
⊢ UniqueDiffWithinAt 𝕜
    ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F))
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)

Tactic:
(hs.prod (uniqueDiffWithinAt_univ (x := w))).mono this

Premises used: setOf, UniqueDiffWithinAt.mono, uniqueDiffWithinAt_univ, UniqueDiffWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs :
  UniqueDiffWithinAt 𝕜 ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
this :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
w : F := ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p).2
A :
  (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)
⊢ UniqueDiffWithinAt 𝕜
    ((↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F))
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)

Tactic:
exact (hs.prod (uniqueDiffWithinAt_univ (x := w))).mono this

Premises used: UniqueDiffWithinAt.mono, uniqueDiffWithinAt_univ, UniqueDiffWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
suffices :
  SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj (E := Z) ⁻¹' s) p

Tactic:
suffices ((extChartAt I p.proj).symm ⁻¹' s ∩ range I) ×ˢ univ ⊆
      (extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' (TotalSpace.proj ⁻¹' s) ∩ range (I.prod 𝓘(𝕜, F)) by
    let w := (extChartAt (I.prod 𝓘(𝕜, F)) p p).2
    have A : extChartAt (I.prod 𝓘(𝕜, F)) p p = (extChartAt I p.1 p.1, w) := by
      ext
      · simp [FiberBundle.chartedSpace_chartAt]
      · rfl
    simp only [UniqueMDiffWithinAt, A] at hs ⊢
    exact (hs.prod (uniqueDiffWithinAt_univ (x := w))).mono this
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))
rcases :
  ∀ (x : M) (v : Z x) (hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
    (h's :
      s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))),
    SProd.sprod (β := Set F)
        ((↑(extChartAt I (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)).symm : E → M) ⁻¹' s ∩
          range (↑I : H → E))
        univ ⊆
      preimage (β := TotalSpace F Z)
          (↑(PartialEquiv.symm (extChartAt (I.prod 𝓘(𝕜, F)) ⟨x, v⟩)) : E × F → TotalSpace F Z)
          (TotalSpace.proj (E := Z) ⁻¹' s) ∩
        range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)
⊢ SProd.sprod (β := Set F) ((↑(extChartAt I (p.proj (E := Z))).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm : E × F → TotalSpace F Z) ⁻¹' TotalSpace.proj (E := Z) ⁻¹' s ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)

Tactic:
rcases p with ⟨x, v⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
dsimp :
  SProd.sprod (β := Set F)
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) univ ⊆
    preimage (β := TotalSpace F Z)
        ((↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H F) ⟨x, v⟩)) : ModelProd H F → TotalSpace F Z) ∘
          (↑(I.prod (PartialEquiv.refl F)).symm : E × F → ModelProd H F))
        (TotalSpace.proj (E := Z) ⁻¹' s) ∩
      range (Prod.map (↑I : H → E) id)
⊢ SProd.sprod (β := Set F)
      ((↑(extChartAt I (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)).symm : E → M) ⁻¹' s ∩
        range (↑I : H → E))
      univ ⊆
    preimage (β := TotalSpace F Z) (↑(PartialEquiv.symm (extChartAt (I.prod 𝓘(𝕜, F)) ⟨x, v⟩)) : E × F → TotalSpace F Z)
        (TotalSpace.proj (E := Z) ⁻¹' s) ∩
      range (↑(I.prod 𝓘(𝕜, F)) : ModelProd H F → E × F)

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (z, w).1 ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z

Tactic:
simp only [mem_inter_iff, mem_preimage, Function.comp_apply,
    mem_range] at hz

Premises used: Set.mem_range, Set.mem_inter_iff, Function.comp_apply, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
simp :
  ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
              M × F → TotalSpace F Z)
            ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.prod (chartAt H x) (OpenPartialHomeomorph.refl F))) :
                ModelProd H F → M × F)
              ((↑(I.prod (PartialEquiv.refl F)).symm : E × F → ModelProd H F) (z, w)))).proj
        (E := Z) ∈
      s ∧
    ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = (z, w)
⊢ (z, w) ∈
    preimage (β := TotalSpace F Z)
        ((↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H F) ⟨x, v⟩)) : ModelProd H F → TotalSpace F Z) ∘
          (↑(I.prod (PartialEquiv.refl F)).symm : E × F → ModelProd H F))
        (TotalSpace.proj (E := Z) ⁻¹' s) ∩
      range (Prod.map (↑I : H → E) id)

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, OpenPartialHomeomorph.coe_trans_symm, mem_inter_iff,
    mem_preimage, Function.comp_apply, mem_range]

Premises used: Set.mem_range, Set.mem_inter_iff, FiberBundle.chartedSpace_chartAt, Function.comp_apply, OpenPartialHomeomorph.coe_trans_symm, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
left :
  ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
            M × F → TotalSpace F Z)
          ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.prod (chartAt H x) (OpenPartialHomeomorph.refl F))) :
              ModelProd H F → M × F)
            ((↑(I.prod (PartialEquiv.refl F)).symm : E × F → ModelProd H F) (z, w)))).proj
      (E := Z) ∈
    s
right : ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = (z, w)
⊢ ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
              M × F → TotalSpace F Z)
            ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.prod (chartAt H x) (OpenPartialHomeomorph.refl F))) :
                ModelProd H F → M × F)
              ((↑(I.prod (PartialEquiv.refl F)).symm : E × F → ModelProd H F) (z, w)))).proj
        (E := Z) ∈
      s ∧
    ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = (z, w)

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
left :
  ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
            M × F → TotalSpace F Z)
          ((fun (p : H × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) p.1, id p.2))
            ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)))).proj
      (E := Z) ∈
    s
⊢ ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
            M × F → TotalSpace F Z)
          ((↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.prod (chartAt H x) (OpenPartialHomeomorph.refl F))) :
              ModelProd H F → M × F)
            ((↑(I.prod (PartialEquiv.refl F)).symm : E × F → ModelProd H F) (z, w)))).proj
      (E := Z) ∈
    s

Tactic:
rw [PartialEquiv.prod_symm, PartialEquiv.refl_symm, PartialEquiv.prod_coe,
      ModelWithCorners.toPartialEquiv_coe_symm, PartialEquiv.refl_coe,
      OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.refl_symm,
      OpenPartialHomeomorph.prod_apply, OpenPartialHomeomorph.refl_apply]

Premises used: OpenPartialHomeomorph.refl_apply, OpenPartialHomeomorph.refl_symm, OpenPartialHomeomorph.prod_apply, OpenPartialHomeomorph.prod_symm, PartialEquiv.refl_symm, PartialEquiv.prod_coe, PartialEquiv.prod_symm, PartialEquiv.refl_coe, ModelWithCorners.toPartialEquiv_coe_symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s

Tactic:
hz.1

Premises used: And.left