-- Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
private lemma UniqueMDiffWithinAt.bundle_preimage_aux {p : TotalSpace F Z}
    (hs : UniqueMDiffWithinAt I s p.proj) (h's : s ⊆ (trivializationAt F Z p.proj).baseSet) :
    UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (π F Z ⁻¹' s) p

Proof state:
case mk
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s { proj := x, snd := v }.proj
h's : s ⊆ (trivializationAt F Z { proj := x, snd := v }.proj).baseSet
⊢ (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(chartAt (ModelProd H F) { proj := x, snd := v }).symm ∘ ↑(I.prod (PartialEquiv.refl F)).symm ⁻¹'
        (TotalSpace.proj ⁻¹' s) ∩
      range (Prod.map (↑I) id)

Tactic:
rintro ⟨z, w⟩ ⟨hz, -⟩

Result:
case mk.mk.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s { proj := x, snd := v }.proj
h's : s ⊆ (trivializationAt F Z { proj := x, snd := v }.proj).baseSet
z : E
w : F
hz : (z, w).1 ∈ ↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I
⊢ (z, w) ∈
    ↑(chartAt (ModelProd H F) { proj := x, snd := v }).symm ∘ ↑(I.prod (PartialEquiv.refl F)).symm ⁻¹'
        (TotalSpace.proj ⁻¹' s) ∩
      range (Prod.map (↑I) id)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s p.proj
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
this :
  (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' (TotalSpace.proj ⁻¹' s) ∩ range ↑(I.prod 𝓘(𝕜, F))
w : F := (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).2
⊢ ↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p = (↑(extChartAt I p.proj) p.proj, w)

Tactic:
ext

Result:
case fst
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s p.proj
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
this :
  (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' (TotalSpace.proj ⁻¹' s) ∩ range ↑(I.prod 𝓘(𝕜, F))
w : F := (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).2
⊢ (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).1 = (↑(extChartAt I p.proj) p.proj, w).1

case snd
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s p.proj
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
this :
  (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' (TotalSpace.proj ⁻¹' s) ∩ range ↑(I.prod 𝓘(𝕜, F))
w : F := (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).2
⊢ (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).2 = (↑(extChartAt I p.proj) p.proj, w).2

Proof state:
case mk.mk.intro.left
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s { proj := x, snd := v }.proj
h's : s ⊆ (trivializationAt F Z { proj := x, snd := v }.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        (↑((chartAt H x).prod (PartialHomeomorph.refl F)).symm (↑(I.prod (PartialEquiv.refl F)).symm (z, w)))).proj ∈
    s

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

Result:
case mk.mk.intro.left
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s { proj := x, snd := v }.proj
h's : s ⊆ (trivializationAt F Z { proj := x, snd := v }.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        ((fun p => (↑(chartAt H x).symm p.1, id p.2)) ((fun p => (↑I.symm p.1, id p.2)) (z, w)))).proj ∈
    s

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueDiffWithinAt 𝕜 (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I p.proj) p.proj)
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
this :
  (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' (TotalSpace.proj ⁻¹' s) ∩ range ↑(I.prod 𝓘(𝕜, F))
w : F := (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).2
A : ↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p = (↑(extChartAt I p.proj) p.proj, w)
⊢ UniqueDiffWithinAt 𝕜 (↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' (TotalSpace.proj ⁻¹' s) ∩ range ↑(I.prod 𝓘(𝕜, F)))
    (↑(extChartAt I p.proj) p.proj, w)

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

Result:
no goals