-- 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.mk.intro.right.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
w : F
u : H
hz : ↑(chartAt H x).symm (↑I.symm (↑I u)) ∈ s ∧ ∃ y, ↑I y = ↑I u
⊢ ∃ y, Prod.map (↑I) id y = (↑I u, w)

Tactic:
exact ⟨(u, w), rfl⟩

Result:
no goals

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
A : ↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p = (↑(extChartAt I p.proj) p.proj, w)
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj ⁻¹' s) p

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

Result:
𝕜 : 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)

Proof state:
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 : ↑(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 ∧
    ∃ y, Prod.map (↑I) id y = (z, w)

Tactic:
constructor

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
        (↑((chartAt H x).prod (PartialHomeomorph.refl F)).symm (↑(I.prod (PartialEquiv.refl F)).symm (z, w)))).proj ∈
    s

case mk.mk.intro.right
𝕜 : 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
⊢ ∃ y, Prod.map (↑I) id y = (z, w)

Proof state:
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 : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (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)

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

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 : ↑(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 ∧
    ∃ y, Prod.map (↑I) id y = (z, w)