[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (range (TotalSpace.mk x))
[PROOFSTEP]
rw [TotalSpace.range_mk]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (TotalSpace.proj ⁻¹' {x})
[PROOFSTEP]
exact isClosed_singleton.preimage <| continuous_proj F E
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
obtain ⟨ea, hea⟩ : ∃ ea : Trivialization F (π F E), a ∈ ea.baseSet :=
  ⟨trivializationAt F E a, mem_baseSet_trivializationAt F E a⟩
    -- If `a < b`, then `[a, b] = ∅`, and the statement is trivial
[GOAL]
case intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
cases' lt_or_le b a with hab hab
[GOAL]
case intro.inl
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : b < a
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
exact
  ⟨ea, by simp [*]⟩
    /- Let `s` be the set of points `x ∈ [a, b]` such that `E` is trivializable over `[a, x]`.
        We need to show that `b ∈ s`. Let `c = Sup s`. We will show that `c ∈ s` and `c = b`. -/
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : b < a
⊢ Icc a b ⊆ ea.baseSet
[PROOFSTEP]
simp [*]
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
set s : Set B := {x ∈ Icc a b | ∃ e : Trivialization F (π F E), Icc a x ⊆ e.baseSet}
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
have ha : a ∈ s := ⟨left_mem_Icc.2 hab, ea, by simp [hea]⟩
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
⊢ Icc a a ⊆ ea.baseSet
[PROOFSTEP]
simp [hea]
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
have sne : s.Nonempty := ⟨a, ha⟩
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
have hsb : b ∈ upperBounds s := fun x hx => hx.1.2
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
have sbd : BddAbove s := ⟨b, hsb⟩
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
set c := sSup s
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
have hsc : IsLUB s c := isLUB_csSup sne sbd
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
[GOAL]
case intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
obtain ⟨-, ec : Trivialization F (π F E), hec : Icc a c ⊆ ec.baseSet⟩ : c ∈ s :=
  by
  cases' hc.1.eq_or_lt with heq hlt
  · rwa [← heq]
  refine
    ⟨hc, ?_⟩
      /- In order to show that `c ∈ s`, consider a trivialization `ec` of `proj` over a neighborhood
            of `c`. Its base set includes `(c', c]` for some `c' ∈ [a, c)`. -/
  obtain ⟨ec, hc⟩ : ∃ ec : Trivialization F (π F E), c ∈ ec.baseSet :=
    ⟨trivializationAt F E c, mem_baseSet_trivializationAt F E c⟩
  obtain ⟨c', hc', hc'e⟩ : ∃ c' ∈ Ico a c, Ioc c' c ⊆ ec.baseSet :=
    (mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset hlt).1
      (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet hc)
        /- Since `c' < c = Sup s`, there exists `d ∈ s ∩ (c', c]`. Let `ead` be a trivialization of
              `proj` over `[a, d]`. Then we can glue `ead` and `ec` into a trivialization over `[a, c]`. -/
  obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2
  refine' ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 _⟩
  refine'
    ⟨fun x hx => had ⟨hx.1.1, hx.2⟩, fun x hx => hc'e ⟨hd.1.trans (not_le.1 hx.2), hx.1.2⟩⟩
      /- So, `c ∈ s`. Let `ec` be a trivialization of `proj` over `[a, c]`.  If `c = b`, then we are
          done. Otherwise we show that `proj` can be trivialized over a larger interval `[a, d]`,
          `d ∈ (c, b]`, hence `c` is not an upper bound of `s`. -/
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
⊢ c ∈ s
[PROOFSTEP]
cases' hc.1.eq_or_lt with heq hlt
[GOAL]
case inl
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
heq : a = c
⊢ c ∈ s
[PROOFSTEP]
rwa [← heq]
[GOAL]
case inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
hlt : a < c
⊢ c ∈ s
[PROOFSTEP]
refine
  ⟨hc, ?_⟩
    /- In order to show that `c ∈ s`, consider a trivialization `ec` of `proj` over a neighborhood
          of `c`. Its base set includes `(c', c]` for some `c' ∈ [a, c)`. -/
[GOAL]
case inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
hlt : a < c
⊢ ∃ e, Icc a c ⊆ e.baseSet
[PROOFSTEP]
obtain ⟨ec, hc⟩ : ∃ ec : Trivialization F (π F E), c ∈ ec.baseSet :=
  ⟨trivializationAt F E c, mem_baseSet_trivializationAt F E c⟩
[GOAL]
case inr.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc✝ : c ∈ Icc a b
hlt : a < c
ec : Trivialization F TotalSpace.proj
hc : c ∈ ec.baseSet
⊢ ∃ e, Icc a c ⊆ e.baseSet
[PROOFSTEP]
obtain ⟨c', hc', hc'e⟩ : ∃ c' ∈ Ico a c, Ioc c' c ⊆ ec.baseSet :=
  (mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset hlt).1
    (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet hc)
      /- Since `c' < c = Sup s`, there exists `d ∈ s ∩ (c', c]`. Let `ead` be a trivialization of
            `proj` over `[a, d]`. Then we can glue `ead` and `ec` into a trivialization over `[a, c]`. -/
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc✝ : c ∈ Icc a b
hlt : a < c
ec : Trivialization F TotalSpace.proj
hc : c ∈ ec.baseSet
c' : B
hc' : c' ∈ Ico a c
hc'e : Ioc c' c ⊆ ec.baseSet
⊢ ∃ e, Icc a c ⊆ e.baseSet
[PROOFSTEP]
obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2
[GOAL]
case inr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc✝ : c ∈ Icc a b
hlt : a < c
ec : Trivialization F TotalSpace.proj
hc : c ∈ ec.baseSet
c' : B
hc' : c' ∈ Ico a c
hc'e : Ioc c' c ⊆ ec.baseSet
d : B
hd : d ∈ Ioc c' c
hdab : d ∈ Icc a b
ead : Trivialization F TotalSpace.proj
had : Icc a d ⊆ ead.baseSet
⊢ ∃ e, Icc a c ⊆ e.baseSet
[PROOFSTEP]
refine' ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 _⟩
[GOAL]
case inr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc✝ : c ∈ Icc a b
hlt : a < c
ec : Trivialization F TotalSpace.proj
hc : c ∈ ec.baseSet
c' : B
hc' : c' ∈ Ico a c
hc'e : Ioc c' c ⊆ ec.baseSet
d : B
hd : d ∈ Ioc c' c
hdab : d ∈ Icc a b
ead : Trivialization F TotalSpace.proj
had : Icc a d ⊆ ead.baseSet
⊢ Icc a c ∩ Iic d ⊆ ead.baseSet ∧
    Icc a c \ Iic d ⊆
      (Trivialization.transFiberHomeomorph ec
          (Trivialization.coordChangeHomeomorph ec ead (_ : d ∈ ec.baseSet) (_ : d ∈ ead.baseSet))).baseSet
[PROOFSTEP]
refine'
  ⟨fun x hx => had ⟨hx.1.1, hx.2⟩, fun x hx => hc'e ⟨hd.1.trans (not_le.1 hx.2), hx.1.2⟩⟩
    /- So, `c ∈ s`. Let `ec` be a trivialization of `proj` over `[a, c]`.  If `c = b`, then we are
        done. Otherwise we show that `proj` can be trivialized over a larger interval `[a, d]`,
        `d ∈ (c, b]`, hence `c` is not an upper bound of `s`. -/
[GOAL]
case intro.inr.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
cases' hc.2.eq_or_lt with heq hlt
[GOAL]
case intro.inr.intro.intro.inl
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
heq : c = b
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
exact ⟨ec, heq ▸ hec⟩
[GOAL]
case intro.inr.intro.intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
suffices : ∃ d ∈ Ioc c b, ∃ e : Trivialization F (π F E), Icc a d ⊆ e.baseSet
[GOAL]
case intro.inr.intro.intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
this : ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
rcases this with
  ⟨d, hdcb, hd⟩
    -- porting note: todo: use `rsuffices`
[GOAL]
case intro.inr.intro.intro.inr.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : ∃ e, Icc a d ⊆ e.baseSet
⊢ ∃ e, Icc a b ⊆ e.baseSet
[PROOFSTEP]
exact ((hsc.1 ⟨⟨hc.1.trans hdcb.1.le, hdcb.2⟩, hd⟩).not_lt hdcb.1).elim
[GOAL]
case this
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
obtain ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, Ico c d ⊆ ec.baseSet :=
  (mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset hlt).1
    (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet (hec ⟨hc.1, le_rfl⟩))
[GOAL]
case this.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
have had : Ico a d ⊆ ec.baseSet := Ico_subset_Icc_union_Ico.trans (union_subset hec hd)
[GOAL]
case this.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
by_cases he : Disjoint (Iio d) (Ioi c)
[GOAL]
case pos
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
obtain ⟨ed, hed⟩ : ∃ ed : Trivialization F (π F E), d ∈ ed.baseSet :=
  ⟨trivializationAt F E d, mem_baseSet_trivializationAt F E d⟩
[GOAL]
case pos.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
ed : Trivialization F TotalSpace.proj
hed : d ∈ ed.baseSet
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
refine'
  ⟨d, hdcb,
    (ec.restrOpen (Iio d) isOpen_Iio).disjointUnion (ed.restrOpen (Ioi c) isOpen_Ioi)
      (he.mono (inter_subset_right _ _) (inter_subset_right _ _)),
    fun x hx => _⟩
[GOAL]
case pos.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
ed : Trivialization F TotalSpace.proj
hed : d ∈ ed.baseSet
x : B
hx : x ∈ Icc a d
⊢ x ∈
    (Trivialization.disjointUnion (Trivialization.restrOpen ec (Iio d) (_ : IsOpen (Iio d)))
        (Trivialization.restrOpen ed (Ioi c) (_ : IsOpen (Ioi c)))
        (_ :
          Disjoint (Trivialization.restrOpen ec (Iio d) (_ : IsOpen (Iio d))).baseSet
            (Trivialization.restrOpen ed (Ioi c) (_ : IsOpen (Ioi c))).baseSet)).baseSet
[PROOFSTEP]
rcases hx.2.eq_or_lt with (rfl | hxd)
[GOAL]
case pos.intro.inl
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
ed : Trivialization F TotalSpace.proj
x : B
hdcb : x ∈ Ioc c b
hd : Ico c x ⊆ ec.baseSet
had : Ico a x ⊆ ec.baseSet
he : Disjoint (Iio x) (Ioi c)
hed : x ∈ ed.baseSet
hx : x ∈ Icc a x
⊢ x ∈
    (Trivialization.disjointUnion (Trivialization.restrOpen ec (Iio x) (_ : IsOpen (Iio x)))
        (Trivialization.restrOpen ed (Ioi c) (_ : IsOpen (Ioi c)))
        (_ :
          Disjoint (Trivialization.restrOpen ec (Iio x) (_ : IsOpen (Iio x))).baseSet
            (Trivialization.restrOpen ed (Ioi c) (_ : IsOpen (Ioi c))).baseSet)).baseSet
case pos.intro.inr
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
ed : Trivialization F TotalSpace.proj
hed : d ∈ ed.baseSet
x : B
hx : x ∈ Icc a d
hxd : x < d
⊢ x ∈
    (Trivialization.disjointUnion (Trivialization.restrOpen ec (Iio d) (_ : IsOpen (Iio d)))
        (Trivialization.restrOpen ed (Ioi c) (_ : IsOpen (Ioi c)))
        (_ :
          Disjoint (Trivialization.restrOpen ec (Iio d) (_ : IsOpen (Iio d))).baseSet
            (Trivialization.restrOpen ed (Ioi c) (_ : IsOpen (Ioi c))).baseSet)).baseSet
[PROOFSTEP]
exacts [Or.inr ⟨hed, hdcb.1⟩, Or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩]
[GOAL]
case neg
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : ¬Disjoint (Iio d) (Ioi c)
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
rw [disjoint_left] at he 
[GOAL]
case neg
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : ¬∀ ⦃a : B⦄, a ∈ Iio d → ¬a ∈ Ioi c
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
push_neg at he 
[GOAL]
case neg
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Exists fun ⦃a⦄ => a ∈ Iio d ∧ a ∈ Ioi (sSup s)
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
rcases he with ⟨d', hdd' : d' < d, hd'c⟩
[GOAL]
case neg.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : Set.Nonempty s
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
d' : B
hdd' : d' < d
hd'c : d' ∈ Ioi (sSup s)
⊢ ∃ d, d ∈ Ioc c b ∧ ∃ e, Icc a d ⊆ e.baseSet
[PROOFSTEP]
exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
hp : p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ
⊢ (fun p => (p.fst, coordChange Z i j p.fst p.snd)) p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ
[PROOFSTEP]
simpa using hp
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
hp : p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ
⊢ (fun p => (p.fst, coordChange Z j i p.fst p.snd)) p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ
[PROOFSTEP]
simpa using hp
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ∀ ⦃x : B × F⦄,
    x ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
      (fun p => (p.fst, coordChange Z j i p.fst p.snd)) ((fun p => (p.fst, coordChange Z i j p.fst p.snd)) x) = x
[PROOFSTEP]
rintro ⟨x, v⟩ hx
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x, v) ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ
⊢ (fun p => (p.fst, coordChange Z j i p.fst p.snd)) ((fun p => (p.fst, coordChange Z i j p.fst p.snd)) (x, v)) = (x, v)
[PROOFSTEP]
simp only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx 
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ (fun p => (p.fst, coordChange Z j i p.fst p.snd)) ((fun p => (p.fst, coordChange Z i j p.fst p.snd)) (x, v)) = (x, v)
[PROOFSTEP]
dsimp only
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ (x, coordChange Z j i x (coordChange Z i j x v)) = (x, v)
[PROOFSTEP]
rw [coordChange_comp, Z.coordChange_self]
[GOAL]
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ x ∈ baseSet Z i
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ x ∈ baseSet Z i ∩ baseSet Z j ∩ baseSet Z i
[PROOFSTEP]
exacts [hx.1, ⟨⟨hx.1, hx.2⟩, hx.1⟩]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ∀ ⦃x : B × F⦄,
    x ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
      (fun p => (p.fst, coordChange Z i j p.fst p.snd)) ((fun p => (p.fst, coordChange Z j i p.fst p.snd)) x) = x
[PROOFSTEP]
rintro ⟨x, v⟩ hx
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x, v) ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ
⊢ (fun p => (p.fst, coordChange Z i j p.fst p.snd)) ((fun p => (p.fst, coordChange Z j i p.fst p.snd)) (x, v)) = (x, v)
[PROOFSTEP]
simp only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true_iff, mem_univ] at hx 
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ (fun p => (p.fst, coordChange Z i j p.fst p.snd)) ((fun p => (p.fst, coordChange Z j i p.fst p.snd)) (x, v)) = (x, v)
[PROOFSTEP]
dsimp only
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ (x, coordChange Z i j x (coordChange Z j i x v)) = (x, v)
[PROOFSTEP]
rw [Z.coordChange_comp, Z.coordChange_self]
[GOAL]
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ x ∈ baseSet Z j
[PROOFSTEP]
exact hx.2
[GOAL]
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ x ∈ baseSet Z j ∩ baseSet Z i ∩ baseSet Z j
[PROOFSTEP]
simp [hx]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ContinuousOn
    { toFun := fun p => (p.fst, coordChange Z i j p.fst p.snd),
        invFun := fun p => (p.fst, coordChange Z j i p.fst p.snd), source := (baseSet Z i ∩ baseSet Z j) ×ˢ univ,
        target := (baseSet Z i ∩ baseSet Z j) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (p : B × F),
              p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z i j p.fst p.snd)) p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (p : B × F),
              p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z j i p.fst p.snd)) p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ),
        left_inv' :=
          (_ :
            ∀ ⦃x : B × F⦄,
              x ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z j i p.fst p.snd))
                    ((fun p => (p.fst, coordChange Z i j p.fst p.snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : B × F⦄,
              x ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z i j p.fst p.snd))
                    ((fun p => (p.fst, coordChange Z j i p.fst p.snd)) x) =
                  x) }.invFun
    { toFun := fun p => (p.fst, coordChange Z i j p.fst p.snd),
        invFun := fun p => (p.fst, coordChange Z j i p.fst p.snd), source := (baseSet Z i ∩ baseSet Z j) ×ˢ univ,
        target := (baseSet Z i ∩ baseSet Z j) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (p : B × F),
              p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z i j p.fst p.snd)) p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (p : B × F),
              p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z j i p.fst p.snd)) p ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ),
        left_inv' :=
          (_ :
            ∀ ⦃x : B × F⦄,
              x ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z j i p.fst p.snd))
                    ((fun p => (p.fst, coordChange Z i j p.fst p.snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ ⦃x : B × F⦄,
              x ∈ (baseSet Z i ∩ baseSet Z j) ×ˢ univ →
                (fun p => (p.fst, coordChange Z i j p.fst p.snd))
                    ((fun p => (p.fst, coordChange Z j i p.fst p.snd)) x) =
                  x) }.target
[PROOFSTEP]
simpa [inter_comm] using continuous_fst.continuousOn.prod (Z.continuousOn_coordChange j i)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p ∈ (trivChange Z i j).toLocalEquiv.source ↔ p.fst ∈ baseSet Z i ∩ baseSet Z j
[PROOFSTEP]
erw [mem_prod]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.fst ∈ baseSet Z i ∩ baseSet Z j ∧ p.snd ∈ univ ↔ p.fst ∈ baseSet Z i ∩ baseSet Z j
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : TotalSpace Z
hp : p ∈ proj Z ⁻¹' baseSet Z i
⊢ (fun p => (p.proj, coordChange Z (indexAt Z p.proj) i p.proj p.snd)) p ∈ baseSet Z i ×ˢ univ
[PROOFSTEP]
simpa only [Set.mem_preimage, and_true_iff, Set.mem_univ, Set.prod_mk_mem_set_prod_eq] using hp
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
hp : p ∈ baseSet Z i ×ˢ univ
⊢ (fun p => { proj := p.fst, snd := coordChange Z i (indexAt Z p.fst) p.fst p.snd }) p ∈ proj Z ⁻¹' baseSet Z i
[PROOFSTEP]
simpa only [Set.mem_preimage, and_true_iff, Set.mem_univ, Set.mem_prod] using hp
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ ∀ ⦃x : TotalSpace Z⦄,
    x ∈ proj Z ⁻¹' baseSet Z i →
      (fun p => { proj := p.fst, snd := coordChange Z i (indexAt Z p.fst) p.fst p.snd })
          ((fun p => (p.proj, coordChange Z (indexAt Z p.proj) i p.proj p.snd)) x) =
        x
[PROOFSTEP]
rintro ⟨x, v⟩ hx
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Fiber Z x
hx : { proj := x, snd := v } ∈ proj Z ⁻¹' baseSet Z i
⊢ (fun p => { proj := p.fst, snd := coordChange Z i (indexAt Z p.fst) p.fst p.snd })
      ((fun p => (p.proj, coordChange Z (indexAt Z p.proj) i p.proj p.snd)) { proj := x, snd := v }) =
    { proj := x, snd := v }
[PROOFSTEP]
replace hx : x ∈ Z.baseSet i := hx
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Fiber Z x
hx : x ∈ baseSet Z i
⊢ (fun p => { proj := p.fst, snd := coordChange Z i (indexAt Z p.fst) p.fst p.snd })
      ((fun p => (p.proj, coordChange Z (indexAt Z p.proj) i p.proj p.snd)) { proj := x, snd := v }) =
    { proj := x, snd := v }
[PROOFSTEP]
dsimp only
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Fiber Z x
hx : x ∈ baseSet Z i
⊢ { proj := x, snd := coordChange Z i (indexAt Z x) x (coordChange Z (indexAt Z x) i x v) } = { proj := x, snd := v }
[PROOFSTEP]
rw [Z.coordChange_comp, Z.coordChange_self]
[GOAL]
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Fiber Z x
hx : x ∈ baseSet Z i
⊢ x ∈ baseSet Z (indexAt Z x)
[PROOFSTEP]
apply_rules [mem_baseSet_at, mem_inter]
[GOAL]
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Fiber Z x
hx : x ∈ baseSet Z i
⊢ x ∈ baseSet Z (indexAt Z x) ∩ baseSet Z i ∩ baseSet Z (indexAt Z x)
[PROOFSTEP]
apply_rules [mem_baseSet_at, mem_inter]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ ∀ ⦃x : B × F⦄,
    x ∈ baseSet Z i ×ˢ univ →
      (fun p => (p.proj, coordChange Z (indexAt Z p.proj) i p.proj p.snd))
          ((fun p => { proj := p.fst, snd := coordChange Z i (indexAt Z p.fst) p.fst p.snd }) x) =
        x
[PROOFSTEP]
rintro ⟨x, v⟩ hx
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : (x, v) ∈ baseSet Z i ×ˢ univ
⊢ (fun p => (p.proj, coordChange Z (indexAt Z p.proj) i p.proj p.snd))
      ((fun p => { proj := p.fst, snd := coordChange Z i (indexAt Z p.fst) p.fst p.snd }) (x, v)) =
    (x, v)
[PROOFSTEP]
simp only [prod_mk_mem_set_prod_eq, and_true_iff, mem_univ] at hx 
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : x ∈ baseSet Z i
⊢ (fun p => (p.proj, coordChange Z (indexAt Z p.proj) i p.proj p.snd))
      ((fun p => { proj := p.fst, snd := coordChange Z i (indexAt Z p.fst) p.fst p.snd }) (x, v)) =
    (x, v)
[PROOFSTEP]
dsimp only
[GOAL]
case mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : x ∈ baseSet Z i
⊢ (x, coordChange Z (indexAt Z x) i x (coordChange Z i (indexAt Z x) x v)) = (x, v)
[PROOFSTEP]
rw [Z.coordChange_comp, Z.coordChange_self]
[GOAL]
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : x ∈ baseSet Z i
⊢ x ∈ baseSet Z i
case mk.a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : x ∈ baseSet Z i
⊢ x ∈ baseSet Z i ∩ baseSet Z (indexAt Z x) ∩ baseSet Z i
[PROOFSTEP]
exacts [hx, ⟨⟨hx, Z.mem_baseSet_at _⟩, hx⟩]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p ∈ (localTrivAsLocalEquiv Z i).target ↔ p.fst ∈ baseSet Z i
[PROOFSTEP]
erw [mem_prod]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p.fst ∈ baseSet Z i ∧ p.snd ∈ univ ↔ p.fst ∈ baseSet Z i
[PROOFSTEP]
simp only [and_true_iff, mem_univ]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j) ≈
    (trivChange Z i j).toLocalEquiv
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source =
    (trivChange Z i j).toLocalEquiv.source
[PROOFSTEP]
ext x
[GOAL]
case left.h
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B × F
⊢ x ∈ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source ↔
    x ∈ (trivChange Z i j).toLocalEquiv.source
[PROOFSTEP]
simp only [mem_localTrivAsLocalEquiv_target, mfld_simps]
[GOAL]
case left.h
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B × F
⊢ x.fst ∈ baseSet Z i ∧ ↑(LocalEquiv.symm (localTrivAsLocalEquiv Z i)) x ∈ (localTrivAsLocalEquiv Z j).source ↔
    x.fst ∈ baseSet Z i ∧ x.fst ∈ baseSet Z j
[PROOFSTEP]
rfl
[GOAL]
case right
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
⊢ EqOn (↑(LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)))
    (↑(trivChange Z i j).toLocalEquiv)
    (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source
[PROOFSTEP]
rintro ⟨x, v⟩ hx
[GOAL]
case right.mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B
v : F
hx : (x, v) ∈ (LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)).source
⊢ ↑(LocalEquiv.trans (LocalEquiv.symm (localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z j)) (x, v) =
    ↑(trivChange Z i j).toLocalEquiv (x, v)
[PROOFSTEP]
simp only [trivChange, localTrivAsLocalEquiv, LocalEquiv.symm, true_and_iff, Prod.mk.inj_iff, prod_mk_mem_set_prod_eq,
  LocalEquiv.trans_source, mem_inter_iff, and_true_iff, mem_preimage, proj, mem_univ, eq_self_iff_true, (· ∘ ·),
  LocalEquiv.coe_trans, TotalSpace.proj] at hx ⊢
[GOAL]
case right.mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ i j : ι
x : B
v : F
hx : x ∈ baseSet Z i ∧ x ∈ baseSet Z j
⊢ coordChange Z (indexAt Z x) j x (coordChange Z i (indexAt Z x) x v) = coordChange Z i j x v
[PROOFSTEP]
simp only [Z.coordChange_comp, hx, mem_inter_iff, and_self_iff, mem_baseSet_at]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ IsOpen (localTrivAsLocalEquiv Z i).source
[PROOFSTEP]
apply TopologicalSpace.GenerateOpen.basic
[GOAL]
case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ (localTrivAsLocalEquiv Z i).source ∈
    ⋃ (i : ι) (s : Set (B × F)) (_ : IsOpen s),
      {(localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s}
[PROOFSTEP]
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
[GOAL]
case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ∃ i_1 i_2,
    IsOpen i_2 ∧
      (localTrivAsLocalEquiv Z i).source = (localTrivAsLocalEquiv Z i_1).source ∩ ↑(localTrivAsLocalEquiv Z i_1) ⁻¹' i_2
[PROOFSTEP]
refine ⟨i, Z.baseSet i ×ˢ univ, (Z.isOpen_baseSet i).prod isOpen_univ, ?_⟩
[GOAL]
case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ (localTrivAsLocalEquiv Z i).source =
    (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' baseSet Z i ×ˢ univ
[PROOFSTEP]
ext p
[GOAL]
case a.h
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
p : TotalSpace Z
⊢ p ∈ (localTrivAsLocalEquiv Z i).source ↔
    p ∈ (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' baseSet Z i ×ˢ univ
[PROOFSTEP]
simp only [localTrivAsLocalEquiv_apply, prod_mk_mem_set_prod_eq, mem_inter_iff, and_self_iff,
  mem_localTrivAsLocalEquiv_source, and_true, mem_univ, mem_preimage]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ContinuousOn (↑(localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z i).source
[PROOFSTEP]
rw [continuousOn_open_iff (Z.open_source' i)]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ∀ (t : Set (B × F)), IsOpen t → IsOpen ((localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' t)
[PROOFSTEP]
intro s s_open
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen s
⊢ IsOpen ((localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s)
[PROOFSTEP]
apply TopologicalSpace.GenerateOpen.basic
[GOAL]
case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen s
⊢ (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s ∈
    ⋃ (i : ι) (s : Set (B × F)) (_ : IsOpen s),
      {(localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s}
[PROOFSTEP]
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
[GOAL]
case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen s
⊢ ∃ i_1 i_2,
    IsOpen i_2 ∧
      (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s =
        (localTrivAsLocalEquiv Z i_1).source ∩ ↑(localTrivAsLocalEquiv Z i_1) ⁻¹' i_2
[PROOFSTEP]
exact ⟨i, s, s_open, rfl⟩
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ContinuousOn (localTrivAsLocalEquiv Z i).invFun (localTrivAsLocalEquiv Z i).target
[PROOFSTEP]
refine continuousOn_open_of_generateFrom fun t ht ↦ ?_
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
ht :
  t ∈
    ⋃ (i : ι) (s : Set (B × F)) (_ : IsOpen s),
      {(localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s}
⊢ IsOpen ((localTrivAsLocalEquiv Z i).target ∩ (localTrivAsLocalEquiv Z i).invFun ⁻¹' t)
[PROOFSTEP]
simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht 
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
ht : ∃ i i_1, IsOpen i_1 ∧ t = (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' i_1
⊢ IsOpen ((localTrivAsLocalEquiv Z i).target ∩ (localTrivAsLocalEquiv Z i).invFun ⁻¹' t)
[PROOFSTEP]
obtain ⟨j, s, s_open, ts⟩ :
  ∃ j s, IsOpen s ∧ t = (localTrivAsLocalEquiv Z j).source ∩ localTrivAsLocalEquiv Z j ⁻¹' s := ht
[GOAL]
case intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
⊢ IsOpen ((localTrivAsLocalEquiv Z i).target ∩ (localTrivAsLocalEquiv Z i).invFun ⁻¹' t)
[PROOFSTEP]
rw [ts]
[GOAL]
case intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
⊢ IsOpen
    ((localTrivAsLocalEquiv Z i).target ∩
      (localTrivAsLocalEquiv Z i).invFun ⁻¹' ((localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s))
[PROOFSTEP]
simp only [LocalEquiv.right_inv, preimage_inter, LocalEquiv.left_inv]
[GOAL]
case intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
⊢ IsOpen
    ((localTrivAsLocalEquiv Z i).target ∩
      ((localTrivAsLocalEquiv Z i).invFun ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
        (localTrivAsLocalEquiv Z i).invFun ⁻¹' (↑(localTrivAsLocalEquiv Z j) ⁻¹' s)))
[PROOFSTEP]
let e := Z.localTrivAsLocalEquiv i
[GOAL]
case intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
⊢ IsOpen
    ((localTrivAsLocalEquiv Z i).target ∩
      ((localTrivAsLocalEquiv Z i).invFun ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
        (localTrivAsLocalEquiv Z i).invFun ⁻¹' (↑(localTrivAsLocalEquiv Z j) ⁻¹' s)))
[PROOFSTEP]
let e' := Z.localTrivAsLocalEquiv j
[GOAL]
case intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
e' : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z j
⊢ IsOpen
    ((localTrivAsLocalEquiv Z i).target ∩
      ((localTrivAsLocalEquiv Z i).invFun ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
        (localTrivAsLocalEquiv Z i).invFun ⁻¹' (↑(localTrivAsLocalEquiv Z j) ⁻¹' s)))
[PROOFSTEP]
let f := e.symm.trans e'
[GOAL]
case intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
e' : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z j
f : LocalEquiv (B × F) (B × F) := LocalEquiv.trans (LocalEquiv.symm e) e'
⊢ IsOpen
    ((localTrivAsLocalEquiv Z i).target ∩
      ((localTrivAsLocalEquiv Z i).invFun ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
        (localTrivAsLocalEquiv Z i).invFun ⁻¹' (↑(localTrivAsLocalEquiv Z j) ⁻¹' s)))
[PROOFSTEP]
have : IsOpen (f.source ∩ f ⁻¹' s) :=
  by
  rw [LocalEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsLocalEquiv_trans i j)]
  exact (continuousOn_open_iff (Z.trivChange i j).open_source).1 (Z.trivChange i j).continuousOn _ s_open
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
e' : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z j
f : LocalEquiv (B × F) (B × F) := LocalEquiv.trans (LocalEquiv.symm e) e'
⊢ IsOpen (f.source ∩ ↑f ⁻¹' s)
[PROOFSTEP]
rw [LocalEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsLocalEquiv_trans i j)]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
e' : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z j
f : LocalEquiv (B × F) (B × F) := LocalEquiv.trans (LocalEquiv.symm e) e'
⊢ IsOpen ((trivChange Z i j).toLocalEquiv.source ∩ ↑(trivChange Z i j).toLocalEquiv ⁻¹' s)
[PROOFSTEP]
exact (continuousOn_open_iff (Z.trivChange i j).open_source).1 (Z.trivChange i j).continuousOn _ s_open
[GOAL]
case intro.intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
e' : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z j
f : LocalEquiv (B × F) (B × F) := LocalEquiv.trans (LocalEquiv.symm e) e'
this : IsOpen (f.source ∩ ↑f ⁻¹' s)
⊢ IsOpen
    ((localTrivAsLocalEquiv Z i).target ∩
      ((localTrivAsLocalEquiv Z i).invFun ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
        (localTrivAsLocalEquiv Z i).invFun ⁻¹' (↑(localTrivAsLocalEquiv Z j) ⁻¹' s)))
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
e' : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z j
f : LocalEquiv (B × F) (B × F) := LocalEquiv.trans (LocalEquiv.symm e) e'
this : IsOpen (f.source ∩ ↑f ⁻¹' s)
⊢ (localTrivAsLocalEquiv Z i).target ∩
      ((localTrivAsLocalEquiv Z i).invFun ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
        (localTrivAsLocalEquiv Z i).invFun ⁻¹' (↑(localTrivAsLocalEquiv Z j) ⁻¹' s)) =
    f.source ∩ ↑f ⁻¹' s
[PROOFSTEP]
dsimp [LocalEquiv.trans_source]
[GOAL]
case h.e'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set (TotalSpace Z)
j : ι
s : Set (B × F)
s_open : IsOpen s
ts : t = (localTrivAsLocalEquiv Z j).source ∩ ↑(localTrivAsLocalEquiv Z j) ⁻¹' s
e : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z i
e' : LocalEquiv (TotalSpace Z) (B × F) := localTrivAsLocalEquiv Z j
f : LocalEquiv (B × F) (B × F) := LocalEquiv.trans (LocalEquiv.symm e) e'
this : IsOpen (f.source ∩ ↑f ⁻¹' s)
⊢ (localTrivAsLocalEquiv Z i).target ∩
      (↑(LocalEquiv.symm (localTrivAsLocalEquiv Z i)) ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
        ↑(LocalEquiv.symm (localTrivAsLocalEquiv Z i)) ⁻¹' (↑(localTrivAsLocalEquiv Z j) ⁻¹' s)) =
    (localTrivAsLocalEquiv Z i).target ∩
        ↑(LocalEquiv.symm (localTrivAsLocalEquiv Z i)) ⁻¹' (localTrivAsLocalEquiv Z j).source ∩
      ↑(localTrivAsLocalEquiv Z j) ∘ ↑(LocalEquiv.symm (localTrivAsLocalEquiv Z i)) ⁻¹' s
[PROOFSTEP]
rw [← preimage_comp, inter_assoc]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
p : TotalSpace Z
x✝ :
  p ∈
    { toLocalEquiv := localTrivAsLocalEquiv Z i, open_source := (_ : IsOpen (localTrivAsLocalEquiv Z i).source),
          open_target := (_ : IsOpen (baseSet Z i ×ˢ univ)),
          continuous_toFun := (_ : ContinuousOn (↑(localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z i).source),
          continuous_invFun :=
            (_ :
              ContinuousOn (localTrivAsLocalEquiv Z i).invFun (localTrivAsLocalEquiv Z i).target) }.toLocalEquiv.source
⊢ (↑{ toLocalEquiv := localTrivAsLocalEquiv Z i, open_source := (_ : IsOpen (localTrivAsLocalEquiv Z i).source),
            open_target := (_ : IsOpen (baseSet Z i ×ˢ univ)),
            continuous_toFun := (_ : ContinuousOn (↑(localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z i).source),
            continuous_invFun :=
              (_ : ContinuousOn (localTrivAsLocalEquiv Z i).invFun (localTrivAsLocalEquiv Z i).target) }
        p).fst =
    proj Z p
[PROOFSTEP]
simp only [mfld_simps]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
p : TotalSpace Z
x✝ :
  p ∈
    { toLocalEquiv := localTrivAsLocalEquiv Z i, open_source := (_ : IsOpen (localTrivAsLocalEquiv Z i).source),
          open_target := (_ : IsOpen (baseSet Z i ×ˢ univ)),
          continuous_toFun := (_ : ContinuousOn (↑(localTrivAsLocalEquiv Z i)) (localTrivAsLocalEquiv Z i).source),
          continuous_invFun :=
            (_ :
              ContinuousOn (localTrivAsLocalEquiv Z i).invFun (localTrivAsLocalEquiv Z i).target) }.toLocalEquiv.source
⊢ (↑(localTrivAsLocalEquiv Z i) p).fst = p.proj
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
⊢ Continuous
    (let_fun this := fun x => { proj := x, snd := v };
    this)
[PROOFSTEP]
refine continuous_iff_continuousAt.2 fun x => ?_
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
⊢ ContinuousAt
    (let_fun this := fun x => { proj := x, snd := v };
    this)
    x
[PROOFSTEP]
have A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x := IsOpen.mem_nhds (Z.isOpen_baseSet (Z.indexAt x)) (Z.mem_baseSet_at x)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (let_fun this := fun x => { proj := x, snd := v };
    this)
    x
[PROOFSTEP]
refine ((Z.localTrivAt x).toLocalHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_
[GOAL]
case refine_1
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ (let_fun this := fun x => { proj := x, snd := v };
      this) ⁻¹'
      (localTrivAt Z x).toLocalHomeomorph.toLocalEquiv.source ∈
    𝓝 x
[PROOFSTEP]
exact A
[GOAL]
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (↑(localTrivAt Z x).toLocalHomeomorph ∘
      let_fun this := fun x => { proj := x, snd := v };
      this)
    x
[PROOFSTEP]
apply continuousAt_id.prod
[GOAL]
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (fun x_1 =>
      coordChange Z
        (indexAt Z
          ((let_fun this := fun x => { proj := x, snd := v };
              this)
              x_1).proj)
        (indexAt Z x)
        ((let_fun this := fun x => { proj := x, snd := v };
            this)
            x_1).proj
        ((let_fun this := fun x => { proj := x, snd := v };
            this)
            x_1).snd)
    x
[PROOFSTEP]
simp only [(· ∘ ·), mfld_simps, localTrivAt_snd]
[GOAL]
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt (fun x_1 => coordChange Z (indexAt Z x_1) (indexAt Z x) x_1 v) x
[PROOFSTEP]
have : ContinuousOn (fun _ : B => v) (Z.baseSet (Z.indexAt x)) := continuousOn_const
[GOAL]
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (baseSet Z (indexAt Z x))
⊢ ContinuousAt (fun x_1 => coordChange Z (indexAt Z x_1) (indexAt Z x) x_1 v) x
[PROOFSTEP]
refine (this.congr fun y hy ↦ ?_).continuousAt A
[GOAL]
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (baseSet Z (indexAt Z x))
y : B
hy : y ∈ baseSet Z (indexAt Z x)
⊢ coordChange Z (indexAt Z y) (indexAt Z x) y v = v
[PROOFSTEP]
exact h _ _ _ ⟨mem_baseSet_at _ _, hy⟩
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
p : TotalSpace Z
⊢ ↑(localTrivAt Z p.proj) p = (p.proj, p.snd)
[PROOFSTEP]
rw [localTrivAt, localTriv_apply, coordChange_self]
[GOAL]
case a
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
p : TotalSpace Z
⊢ p.proj ∈ baseSet Z (indexAt Z p.proj)
[PROOFSTEP]
exact Z.mem_baseSet_at p.1
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
⊢ b ∈ (localTrivAt Z b).baseSet
[PROOFSTEP]
rw [localTrivAt, ← baseSet_at]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
⊢ b ∈ baseSet Z (indexAt Z b)
[PROOFSTEP]
exact Z.mem_baseSet_at b
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
⊢ { proj := b, snd := a } ∈ (localTrivAt Z b).toLocalHomeomorph.toLocalEquiv.source
[PROOFSTEP]
simp only [mfld_simps]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Fiber Z b
⊢ 𝓝 x = comap (TotalSpace.mk b) (𝓝 { proj := b, snd := x })
[PROOFSTEP]
rw [(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _), comap_inf, comap_principal,
  comap_comap]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Fiber Z b
⊢ 𝓝 x =
    comap (↑(localTrivAt Z b).toLocalHomeomorph ∘ TotalSpace.mk b)
        (𝓝 (↑(localTrivAt Z b).toLocalHomeomorph { proj := b, snd := x })) ⊓
      𝓟 (TotalSpace.mk b ⁻¹' (localTrivAt Z b).toLocalHomeomorph.toLocalEquiv.source)
[PROOFSTEP]
simp only [(· ∘ ·), localTrivAt_apply_mk, Trivialization.coe_coe, ← (embedding_prod_mk b).nhds_eq_comap]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Fiber Z b
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 (TotalSpace.mk b ⁻¹' (localTrivAt Z b).toLocalHomeomorph.toLocalEquiv.source)
[PROOFSTEP]
convert_to 𝓝 x = 𝓝 x ⊓ 𝓟 univ
[GOAL]
case h.e'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Fiber Z b
⊢ 𝓝 x ⊓ 𝓟 (TotalSpace.mk b ⁻¹' (localTrivAt Z b).toLocalHomeomorph.toLocalEquiv.source) = 𝓝 x ⊓ 𝓟 univ
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.e_a.e_s
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Fiber Z b
⊢ TotalSpace.mk b ⁻¹' (localTrivAt Z b).toLocalHomeomorph.toLocalEquiv.source = univ
[PROOFSTEP]
exact eq_univ_of_forall (mk_mem_localTrivAt_source Z _)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Fiber Z b
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 univ
[PROOFSTEP]
rw [principal_univ, inf_top_eq]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
⊢ ContinuousOn (↑(LocalEquiv.symm e.toLocalEquiv)) e.target
[PROOFSTEP]
refine' fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono _) U h)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
z : B × F
H : z ∈ e.target
U : Set (TotalSpace F E)
h : U ∈ 𝓝 (↑(LocalEquiv.symm e.toLocalEquiv) z)
⊢ coinduced (fun x => ↑(LocalEquiv.symm e.toLocalEquiv) ↑x) inferInstance ≤ totalSpaceTopology a
[PROOFSTEP]
exact le_iSup₂ (α := TopologicalSpace (TotalSpace F E)) e he
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e : Pretrivialization F TotalSpace.proj
⊢ IsOpen e.source
[PROOFSTEP]
refine isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ IsOpen e.source
[PROOFSTEP]
refine' isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, _⟩)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ Subtype.val ⁻¹' e.target = Pretrivialization.setSymm e' ⁻¹' e.source
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.mk
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
x : B × F
hx : x ∈ e'.target
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' e.target ↔
    { val := x, property := hx } ∈ Pretrivialization.setSymm e' ⁻¹' e.source
[PROOFSTEP]
simp only [mem_preimage, Pretrivialization.setSymm, restrict, e.mem_target, e.mem_source, e'.proj_symm_apply hx]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
[PROOFSTEP]
letI := a.totalSpaceTopology
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
[PROOFSTEP]
obtain ⟨u, hu1, hu2⟩ :=
  continuousOn_iff'.mp (a.continuous_symm_of_mem_pretrivializationAtlas he') e.source (a.isOpen_source e)
[GOAL]
case intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
[PROOFSTEP]
rw [inter_comm, hu2]
[GOAL]
case intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (u ∩ e'.target)
[PROOFSTEP]
exact hu1.inter e'.open_target
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ ContinuousOn (↑e.toLocalEquiv) e.source
[PROOFSTEP]
refine
  continuousOn_iff'.mpr fun s hs =>
    ⟨e ⁻¹' s ∩ e.source, isOpen_iSup_iff.mpr fun e' => ?_, by rw [inter_assoc, inter_self]; rfl⟩
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
⊢ ↑e.toLocalEquiv ⁻¹' s ∩ e.source = ↑e ⁻¹' s ∩ e.source ∩ e.source
[PROOFSTEP]
rw [inter_assoc, inter_self]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
⊢ ↑e.toLocalEquiv ⁻¹' s ∩ e.source = ↑e ⁻¹' s ∩ e.source
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
⊢ IsOpen (↑e ⁻¹' s ∩ e.source)
[PROOFSTEP]
refine isOpen_iSup_iff.mpr fun he' => ?_
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen (↑e ⁻¹' s ∩ e.source)
[PROOFSTEP]
rw [isOpen_coinduced, isOpen_induced_iff]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = Pretrivialization.setSymm e' ⁻¹' (↑e ⁻¹' s ∩ e.source)
[PROOFSTEP]
obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_trivChange _ he _ he') s hs
[GOAL]
case intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen u
hu2 :
  ↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = Pretrivialization.setSymm e' ⁻¹' (↑e ⁻¹' s ∩ e.source)
[PROOFSTEP]
have hu3 := congr_arg (fun s => (fun x : e'.target => (x : B × F)) ⁻¹' s) hu2
[GOAL]
case intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen u
hu2 :
  ↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
hu3 :
  (fun s => (fun x => ↑x) ⁻¹' s)
      (↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)) =
    (fun s => (fun x => ↑x) ⁻¹' s) (u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source))
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = Pretrivialization.setSymm e' ⁻¹' (↑e ⁻¹' s ∩ e.source)
[PROOFSTEP]
simp only [Subtype.coe_preimage_self, preimage_inter, univ_inter] at hu3 
[GOAL]
case intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen u
hu2 :
  ↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
hu3 :
  (fun x => ↑x) ⁻¹' (↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s) ∩
      (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    (fun x => ↑x) ⁻¹' u ∩ (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = Pretrivialization.setSymm e' ⁻¹' (↑e ⁻¹' s ∩ e.source)
[PROOFSTEP]
refine
  ⟨u ∩ e'.toLocalEquiv.target ∩ e'.toLocalEquiv.symm ⁻¹' e.source, ?_, by
    simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]; rfl⟩
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen u
hu2 :
  ↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
hu3 :
  (fun x => ↑x) ⁻¹' (↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s) ∩
      (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    (fun x => ↑x) ⁻¹' u ∩ (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
⊢ Subtype.val ⁻¹' (u ∩ e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    Pretrivialization.setSymm e' ⁻¹' (↑e ⁻¹' s ∩ e.source)
[PROOFSTEP]
simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen u
hu2 :
  ↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
hu3 :
  (fun x => ↑x) ⁻¹' (↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s) ∩
      (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    (fun x => ↑x) ⁻¹' u ∩ (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
⊢ (fun x => ↑x) ⁻¹' (↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s) ∩
      (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    Pretrivialization.setSymm e' ⁻¹' (↑e ⁻¹' s) ∩ Pretrivialization.setSymm e' ⁻¹' e.source
[PROOFSTEP]
rfl
[GOAL]
case intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen u
hu2 :
  ↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
hu3 :
  (fun x => ↑x) ⁻¹' (↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s) ∩
      (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    (fun x => ↑x) ⁻¹' u ∩ (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
⊢ IsOpen (u ∩ e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
[PROOFSTEP]
rw [inter_assoc]
[GOAL]
case intro.intro
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
s : Set (B × F)
hs : IsOpen s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen u
hu2 :
  ↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
hu3 :
  (fun x => ↑x) ⁻¹' (↑e ∘ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' s) ∩
      (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source) =
    (fun x => ↑x) ⁻¹' u ∩ (fun x => ↑x) ⁻¹' (↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
⊢ IsOpen (u ∩ (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source))
[PROOFSTEP]
exact hu1.inter (a.isOpen_target_of_mem_pretrivializationAtlas_inter e e' he')
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
x : E b
⊢ { proj := b, snd := x } ∈ (pretrivializationAt a b).source
[PROOFSTEP]
simp only [(a.pretrivializationAt b).source_eq, mem_preimage, TotalSpace.proj]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
x : E b
⊢ b ∈ (pretrivializationAt a b).baseSet
[PROOFSTEP]
exact a.mem_base_pretrivializationAt b
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
⊢ Continuous (TotalSpace.mk b)
[PROOFSTEP]
letI := a.totalSpaceTopology
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ Continuous (TotalSpace.mk b)
[PROOFSTEP]
let e := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a b ∈ a.pretrivializationAtlas)
⊢ Continuous (TotalSpace.mk b)
[PROOFSTEP]
rw [e.toLocalHomeomorph.continuous_iff_continuous_comp_left (a.totalSpaceMk_preimage_source b)]
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a b ∈ a.pretrivializationAtlas)
⊢ Continuous (↑e.toLocalHomeomorph ∘ TotalSpace.mk b)
[PROOFSTEP]
exact continuous_iff_le_induced.mpr (le_antisymm_iff.mp (a.totalSpaceMk_inducing b).induced).1
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
h : Inducing (↑(pretrivializationAt a b) ∘ TotalSpace.mk b)
⊢ Inducing (TotalSpace.mk b)
[PROOFSTEP]
letI := a.totalSpaceTopology
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
h : Inducing (↑(pretrivializationAt a b) ∘ TotalSpace.mk b)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ Inducing (TotalSpace.mk b)
[PROOFSTEP]
rw [← restrict_comp_codRestrict (a.mem_pretrivializationAt_source b)] at h 
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => { proj := b, snd := x }) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), { proj := b, snd := x } ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ Inducing (TotalSpace.mk b)
[PROOFSTEP]
apply Inducing.of_codRestrict (a.mem_pretrivializationAt_source b)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => { proj := b, snd := x }) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), { proj := b, snd := x } ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ Inducing
    (codRestrict (fun a => { proj := b, snd := a }) (pretrivializationAt a b).source
      (_ : ∀ (x : E b), { proj := b, snd := x } ∈ (pretrivializationAt a b).source))
[PROOFSTEP]
refine
  inducing_of_inducing_compose ?_
    (continuousOn_iff_continuous_restrict.mp
      (a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)).continuous_toFun)
    h
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => { proj := b, snd := x }) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), { proj := b, snd := x } ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ Continuous
    (codRestrict (fun a => { proj := b, snd := a }) (pretrivializationAt a b).source
      (_ : ∀ (x : E b), { proj := b, snd := x } ∈ (pretrivializationAt a b).source))
[PROOFSTEP]
exact (a.continuous_totalSpaceMk b).codRestrict (a.mem_pretrivializationAt_source b)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
⊢ Continuous TotalSpace.proj
[PROOFSTEP]
letI := a.totalSpaceTopology
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ Continuous TotalSpace.proj
[PROOFSTEP]
letI := a.toFiberBundle
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
this✝ : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
this : FiberBundle F E := toFiberBundle a
⊢ Continuous TotalSpace.proj
[PROOFSTEP]
exact FiberBundle.continuous_proj F E
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
⊢ ContinuousOn f (TotalSpace.proj ⁻¹' s)
[PROOFSTEP]
letI := a.totalSpaceTopology
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
⊢ ContinuousOn f (TotalSpace.proj ⁻¹' s)
[PROOFSTEP]
intro z hz
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
⊢ ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z
[PROOFSTEP]
let e : Trivialization F (π F E) := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas z.proj)
[GOAL]
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z
[PROOFSTEP]
refine' (e.continuousAt_of_comp_right _ ((hf z.proj hz).continuousAt (IsOpen.mem_nhds _ _))).continuousWithinAt
[GOAL]
case refine'_1
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ z.proj ∈ e.baseSet
[PROOFSTEP]
exact a.mem_base_pretrivializationAt z.proj
[GOAL]
case refine'_2
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ IsOpen ((s ∩ (pretrivializationAt a z.proj).baseSet) ×ˢ univ)
[PROOFSTEP]
exact (hs.inter (a.pretrivializationAt z.proj).open_baseSet).prod isOpen_univ
[GOAL]
case refine'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ ↑e z ∈ (s ∩ (pretrivializationAt a z.proj).baseSet) ×ˢ univ
[PROOFSTEP]
refine' ⟨_, mem_univ _⟩
[GOAL]
case refine'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ (↑e z).fst ∈ s ∩ (pretrivializationAt a z.proj).baseSet
[PROOFSTEP]
rw [e.coe_fst]
[GOAL]
case refine'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ z.proj ∈ s ∩ (pretrivializationAt a z.proj).baseSet
[PROOFSTEP]
exact ⟨hz, a.mem_base_pretrivializationAt z.proj⟩
[GOAL]
case refine'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ z ∈ e.source
[PROOFSTEP]
rw [e.mem_source]
[GOAL]
case refine'_3
ι : Type u_1
B : Type u_2
F : Type u_3
X✝ : Type u_4
inst✝⁴ : TopologicalSpace X✝
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf :
  ∀ (b : B),
    b ∈ s →
      ContinuousOn (f ∘ ↑(LocalEquiv.symm (pretrivializationAt a b).toLocalEquiv))
        ((s ∩ (pretrivializationAt a b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := totalSpaceTopology a
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a z.proj ∈ a.pretrivializationAtlas)
⊢ z.proj ∈ e.baseSet
[PROOFSTEP]
exact a.mem_base_pretrivializationAt z.proj
