awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
⊢ UniqueMDiffOn 𝓘(𝕜, E) ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)
have rw : UniqueMDiffOn 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) '' (s ∩ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source))
Tactic: rw [← PartialEquiv.image_source_inter_eq', inter_comm, extChartAt_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : E
hy : y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) y
have apply : (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s ⊆
  range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s
Tactic: apply (hs.uniqueDiffOn_target_inter x y hy).mono
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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
⊢ UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' y).source) z
have apply : f ⁻¹' (extChartAt I' y).source ∈ nhdsWithin z s
Tactic: apply (hs z hz.1).inter'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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
⊢ f ⁻¹' (extChartAt I' y).source ∈ nhdsWithin z s
have apply : (extChartAt I' y).source ∈ nhds (f z)
Tactic: apply (hf z hz.1).preimage_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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
⊢ (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) : TotalSpace F Z → E × F) p =
    ((↑(extChartAt I (p.proj (E := Z))) : M → E) (p.proj (E := Z)), w)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (hypothesis)
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
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj (E := Z) ⁻¹' s) p
have 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)
Tactic: have A : extChartAt (I.prod 𝓘(𝕜, F)) p p = (extChartAt I p.1 p.1, w) := by
      ext
      · simp [FiberBundle.chartedSpace_chartAt]
      · rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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)
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj (E := Z) ⁻¹' s) p
have 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)
Tactic: simp only [UniqueMDiffWithinAt, A] at hs ⊢
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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)))
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj (E := Z) ⁻¹' s) p
have 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)
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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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)))
⊢ 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)
have 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)
Tactic: rcases p with ⟨x, v⟩
Cleared hypotheses: p, hs, h's
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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⟩))
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (hypothesis)
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)
⊢ (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)
have hz₁ : (↑(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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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
⊢ (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)
have 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)
Tactic: simp only [FiberBundle.chartedSpace_chartAt, OpenPartialHomeomorph.coe_trans_symm, mem_inter_iff,
    mem_preimage, Function.comp_apply, mem_range]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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 (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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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
⊢ ((↑(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)
have right : ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = (z, w)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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 (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
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
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 (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
have h : ((↑(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) =
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)
Tactic: convert! hz.1