[GOAL]
B : Type u_1
F : Type u_2
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
⊢ topologicalSpace B F = induced (↑(TotalSpace.toProd B F)) instTopologicalSpaceProd
[PROOFSTEP]
simp only [instTopologicalSpaceProd, induced_inf, induced_compose]
[GOAL]
B : Type u_1
F : Type u_2
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
⊢ topologicalSpace B F =
    induced (Prod.fst ∘ ↑(TotalSpace.toProd B F)) inst✝¹ ⊓ induced (Prod.snd ∘ ↑(TotalSpace.toProd B F)) inst✝
[PROOFSTEP]
rfl
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
let f₁ : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p ↦
  ((⟨p.1, p.2.1⟩ : TotalSpace F₁ E₁), (⟨p.1, p.2.2⟩ : TotalSpace F₂ E₂))
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
let f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ ⟨e₁ p.1, e₂ p.2⟩
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
let f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ ⟨p.1.1, p.1.2, p.2.2⟩
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
have hf₁ : Continuous f₁ := (Prod.inducing_diag F₁ E₁ F₂ E₂).continuous
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
have hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source) :=
  e₁.toLocalHomeomorph.continuousOn.prod_map e₂.toLocalHomeomorph.continuousOn
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
have hf₃ : Continuous f₃ := (continuous_fst.comp continuous_fst).prod_mk (continuous_snd.prod_map continuous_snd)
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
refine' ((hf₃.comp_continuousOn hf₂).comp hf₁.continuousOn _).congr _
[GOAL]
case refine'_1
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ MapsTo f₁ (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) (e₁.source ×ˢ e₂.source)
[PROOFSTEP]
rw [e₁.source_eq, e₂.source_eq]
[GOAL]
case refine'_1
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ MapsTo f₁ (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    ((TotalSpace.proj ⁻¹' e₁.baseSet) ×ˢ (TotalSpace.proj ⁻¹' e₂.baseSet))
[PROOFSTEP]
exact mapsTo_preimage _ _
[GOAL]
case refine'_2
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ EqOn (toFun' e₁ e₂) ((f₃ ∘ f₂) ∘ f₁) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
rintro ⟨b, v₁, v₂⟩ ⟨hb₁, _⟩
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ toFun' e₁ e₂ { proj := b, snd := (v₁, v₂) } = ((f₃ ∘ f₂) ∘ f₁) { proj := b, snd := (v₁, v₂) }
[PROOFSTEP]
simp only [Prod.toFun', Prod.mk.inj_iff, Function.comp_apply, and_true_iff]
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ b = (↑e₁ { proj := b, snd := v₁ }).fst
[PROOFSTEP]
rw [e₁.coe_fst]
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ } ∈ e₁.source
[PROOFSTEP]
rw [e₁.source_eq, mem_preimage]
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ }.proj ∈ e₁.baseSet
[PROOFSTEP]
exact hb₁
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x
h : x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)
⊢ invFun' e₁ e₂ (toFun' e₁ e₂ x) = x
[PROOFSTEP]
obtain ⟨x, v₁, v₂⟩ := x
[GOAL]
case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
v₁ : E₁ x
v₂ : E₂ x
h : { proj := x, snd := (v₁, v₂) } ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)
⊢ invFun' e₁ e₂ (toFun' e₁ e₂ { proj := x, snd := (v₁, v₂) }) = { proj := x, snd := (v₁, v₂) }
[PROOFSTEP]
obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h
[GOAL]
case mk.mk.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
v₁ : E₁ x
v₂ : E₂ x
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ invFun' e₁ e₂ (toFun' e₁ e₂ { proj := x, snd := (v₁, v₂) }) = { proj := x, snd := (v₁, v₂) }
[PROOFSTEP]
simp only [Prod.toFun', Prod.invFun', symm_apply_apply_mk, h₁, h₂]
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B × F₁ × F₂
h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ x) = x
[PROOFSTEP]
obtain ⟨x, w₁, w₂⟩ := x
[GOAL]
case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h : (x, w₁, w₂) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
[PROOFSTEP]
obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h
[GOAL]
case mk.mk.intro.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
[PROOFSTEP]
simp only [Prod.toFun', Prod.invFun', apply_mk_symm, h₁, h₂]
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ ContinuousOn (invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
[PROOFSTEP]
rw [(Prod.inducing_diag F₁ E₁ F₂ E₂).continuousOn_iff]
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
[PROOFSTEP]
have H₁ : Continuous fun p : B × F₁ × F₂ ↦ ((p.1, p.2.1), (p.1, p.2.2)) :=
  (continuous_id.prod_map continuous_fst).prod_mk (continuous_id.prod_map continuous_snd)
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
[PROOFSTEP]
refine' (e₁.continuousOn_symm.prod_map e₂.continuousOn_symm).comp H₁.continuousOn _
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ MapsTo (fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
    ((e₁.baseSet ×ˢ univ) ×ˢ e₂.baseSet ×ˢ univ)
[PROOFSTEP]
exact fun x h ↦ ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ IsOpen
    { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂, source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
        target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧ (Prod.toFun' e₁ e₂ x).snd ∈ univ),
        map_target' :=
          (_ : ∀ (x : B × F₁ × F₂), x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) → Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
        right_inv' :=
          (_ :
            ∀ (x : B × F₁ × F₂),
              x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source
[PROOFSTEP]
convert (e₁.open_source.prod e₂.open_source).preimage (FiberBundle.Prod.inducing_diag F₁ E₁ F₂ E₂).continuous
[GOAL]
case h.e'_3
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂, source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
        target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧ (Prod.toFun' e₁ e₂ x).snd ∈ univ),
        map_target' :=
          (_ : ∀ (x : B × F₁ × F₂), x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) → Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
        right_inv' :=
          (_ :
            ∀ (x : B × F₁ × F₂),
              x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source =
    (fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ⁻¹' e₁.source ×ˢ e₂.source
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x
⊢ x ∈
      { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
          source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet), target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
          map_source' :=
            (_ :
              ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                  (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧ (Prod.toFun' e₁ e₂ x).snd ∈ univ),
          map_target' :=
            (_ : ∀ (x : B × F₁ × F₂), x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
          left_inv' :=
            (_ :
              ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) → Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
          right_inv' :=
            (_ :
              ∀ (x : B × F₁ × F₂),
                x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source ↔
    x ∈
      (fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ⁻¹' e₁.source ×ˢ e₂.source
[PROOFSTEP]
simp only [Trivialization.source_eq, mfld_simps]
[GOAL]
B : Type u_1
inst✝¹⁰ : TopologicalSpace B
F₁ : Type u_2
inst✝⁹ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁸ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝⁷ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁵ : (x : B) → Zero (E₁ x)
inst✝⁴ : (x : B) → Zero (E₂ x)
inst✝³ : (x : B) → TopologicalSpace (E₁ x)
inst✝² : (x : B) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₁ E₁
inst✝ : FiberBundle F₂ E₂
b : B
⊢ Inducing (TotalSpace.mk b)
[PROOFSTEP]
rw [(Prod.inducing_diag F₁ E₁ F₂ E₂).inducing_iff]
[GOAL]
B : Type u_1
inst✝¹⁰ : TopologicalSpace B
F₁ : Type u_2
inst✝⁹ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁸ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝⁷ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁵ : (x : B) → Zero (E₁ x)
inst✝⁴ : (x : B) → Zero (E₂ x)
inst✝³ : (x : B) → TopologicalSpace (E₁ x)
inst✝² : (x : B) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₁ E₁
inst✝ : FiberBundle F₂ E₂
b : B
⊢ Inducing ((fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ∘ TotalSpace.mk b)
[PROOFSTEP]
exact (totalSpaceMk_inducing F₁ E₁ b).prod_map (totalSpaceMk_inducing F₂ E₂ b)
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f : B' → B
inst✝ : (x : B) → TopologicalSpace (E x)
⊢ (x : B') → TopologicalSpace ((f *ᵖ E) x)
[PROOFSTEP]
intro x
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f : B' → B
inst✝ : (x : B) → TopologicalSpace (E x)
x : B'
⊢ TopologicalSpace ((f *ᵖ E) x)
[PROOFSTEP]
rw [Bundle.Pullback]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f : B' → B
inst✝ : (x : B) → TopologicalSpace (E x)
x : B'
⊢ TopologicalSpace (E (f x))
[PROOFSTEP]
infer_instance
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous TotalSpace.proj
[PROOFSTEP]
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced TotalSpace.proj inst✝¹
[PROOFSTEP]
exact inf_le_left
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous (Pullback.lift f)
[PROOFSTEP]
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced (Pullback.lift f) inst✝
[PROOFSTEP]
exact inf_le_right
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Inducing (pullbackTotalSpaceEmbedding f)
[PROOFSTEP]
constructor
[GOAL]
case induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding f) instTopologicalSpaceProd
[PROOFSTEP]
simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose, Pullback.TotalSpace.topologicalSpace,
  pullbackTopology_def]
[GOAL]
case induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ =
    induced (Prod.fst ∘ pullbackTotalSpaceEmbedding f) inst✝¹ ⊓ induced (Prod.snd ∘ pullbackTotalSpaceEmbedding f) inst✝
[PROOFSTEP]
rfl
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ Continuous (TotalSpace.mk x)
[PROOFSTEP]
simp only [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, induced_compose, induced_inf, Function.comp,
  induced_const, top_inf_eq, pullbackTopology_def]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ instForAllTopologicalSpacePullback E f x ≤ induced (fun x_1 => Pullback.lift f { proj := x, snd := x_1 }) inst✝⁴
[PROOFSTEP]
exact le_of_eq (FiberBundle.totalSpaceMk_inducing F E (f x)).induced
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : x ∈ Pullback.lift ↑f ⁻¹' e.source
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
[PROOFSTEP]
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj] at h 
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : ↑f x.proj ∈ e.baseSet
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
[PROOFSTEP]
simp_rw [prod_mk_mem_set_prod_eq, mem_univ, and_true_iff, mem_preimage, h]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈ Pullback.lift ↑f ⁻¹' e.source
[PROOFSTEP]
rw [mem_prod, mem_preimage] at h 
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : ↑f y.fst ∈ e.baseSet ∧ y.snd ∈ univ
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈ Pullback.lift ↑f ⁻¹' e.source
[PROOFSTEP]
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : x ∈ Pullback.lift ↑f ⁻¹' e.source
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
      ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
    x
[PROOFSTEP]
simp_rw [mem_preimage, e.mem_source, Pullback.lift_proj] at h 
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : ↑f x.proj ∈ e.baseSet
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
      ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
    x
[PROOFSTEP]
simp_rw [Pullback.lift, e.symm_apply_apply_mk h]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
      ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
    x
[PROOFSTEP]
simp_rw [mem_prod, mem_preimage, mem_univ, and_true_iff] at h 
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : ↑f x.fst ∈ e.baseSet
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
      ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
    x
[PROOFSTEP]
simp_rw [Pullback.lift_mk, e.apply_mk_symm h]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ IsOpen
    { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
        invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
        source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (y : B' × F),
              y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                  Pullback.lift ↑f ⁻¹' e.source),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                    ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ (x : B' × F),
              x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                    ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                  x) }.source
[PROOFSTEP]
simp_rw [e.source_eq, ← preimage_comp]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ IsOpen (TotalSpace.proj ∘ Pullback.lift ↑f ⁻¹' e.baseSet)
[PROOFSTEP]
exact e.open_baseSet.preimage ((map_continuous f).comp <| Pullback.continuous_proj F E f)
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ ContinuousOn
    { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
        invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
        source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (y : B' × F),
              y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                  Pullback.lift ↑f ⁻¹' e.source),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                    ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ (x : B' × F),
              x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                    ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                  x) }.invFun
    { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
        invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
        source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (y : B' × F),
              y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                  Pullback.lift ↑f ⁻¹' e.source),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                    ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ (x : B' × F),
              x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                    ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                  x) }.target
[PROOFSTEP]
dsimp only
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ ContinuousOn (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) ((↑f ⁻¹' e.baseSet) ×ˢ univ)
[PROOFSTEP]
simp_rw [(inducing_pullbackTotalSpaceEmbedding F E f).continuousOn_iff, Function.comp, pullbackTotalSpaceEmbedding]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ ContinuousOn (fun x => (x.fst, { proj := ↑f x.fst, snd := Trivialization.symm e (↑f x.fst) x.snd }))
    ((↑f ⁻¹' e.baseSet) ×ˢ univ)
[PROOFSTEP]
refine'
  continuousOn_fst.prod (e.continuousOn_symm.comp ((map_continuous f).prod_map continuous_id).continuousOn Subset.rfl)
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ {
          toLocalEquiv :=
            { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
              invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
              source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
              map_source' :=
                (_ :
                  ∀ (x : TotalSpace F (↑f *ᵖ E)),
                    x ∈ Pullback.lift ↑f ⁻¹' e.source →
                      (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
              map_target' :=
                (_ :
                  ∀ (y : B' × F),
                    y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                      (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                        Pullback.lift ↑f ⁻¹' e.source),
              left_inv' :=
                (_ :
                  ∀ (x : TotalSpace F (↑f *ᵖ E)),
                    x ∈ Pullback.lift ↑f ⁻¹' e.source →
                      (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                          ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                        x),
              right_inv' :=
                (_ :
                  ∀ (x : B' × F),
                    x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                      (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                          ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                        x) },
          open_source :=
            (_ :
              IsOpen
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.source),
          open_target := (_ : IsOpen ((↑f ⁻¹' e.baseSet) ×ˢ univ)),
          continuous_toFun :=
            (_ :
              ContinuousOn (fun x => (x.proj, (↑e (Pullback.lift (↑f) x)).snd))
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.source),
          continuous_invFun :=
            (_ :
              ContinuousOn
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.invFun
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.target) }.toLocalEquiv.source =
    TotalSpace.proj ⁻¹' (↑f ⁻¹' e.baseSet)
[PROOFSTEP]
dsimp only
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ Pullback.lift ↑f ⁻¹' e.source = TotalSpace.proj ⁻¹' (↑f ⁻¹' e.baseSet)
[PROOFSTEP]
rw [e.source_eq]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ Pullback.lift ↑f ⁻¹' (TotalSpace.proj ⁻¹' e.baseSet) = TotalSpace.proj ⁻¹' (↑f ⁻¹' e.baseSet)
[PROOFSTEP]
rfl
