case intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
obtain ⟨ea, hea⟩ : ∃ ea : Trivialization F (π E), a ∈ ea.baseSet :=
  ⟨trivializationAt F E a, mem_baseSet_trivializationAt F E a⟩
case intro.inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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

case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
cases' lt_or_le b a with hab hab
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
set s : Set B := { x ∈ Icc a b | ∃ e : Trivialization F (π E), Icc a x ⊆ e.baseSet }
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
have ha : a ∈ s := ⟨left_mem_Icc.2 hab, ea, by simp [hea]⟩
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
have sne : s.Nonempty := ⟨a, ha⟩
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
have hsb : b ∈ upperBounds s := fun x hx => hx.1.2
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
have sbd : BddAbove s := ⟨b, hsb⟩
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
set c := sSup s
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
have hsc : IsLUB s c := isLUB_csSup sne sbd
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
case intro.inr.intro.intro.inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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

case intro.inr.intro.intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
cases' hc.2.eq_or_lt with heq hlt
case intro.inr.intro.intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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

case this
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr.intro.intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
suffices : ∃ d ∈ Ioc c b, ∃ e : Trivialization F (π E), Icc a d ⊆ e.baseSet
case this.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case this
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
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⟩))
case this.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case this.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
have had : Ico a d ⊆ ec.baseSet := Ico_subset_Icc_union_Ico.trans (union_subset hec hd)
case pos
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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

case neg
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case this.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
by_cases he : Disjoint (Iio d) (Ioi c)
no goals
case intro.inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
exact ⟨ea, by simp [*]⟩
no goals
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
simp [*]
no goals
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
simp [hea]
case inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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

case inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
cases' hc.1.eq_or_lt with heq hlt
case inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
refine ⟨hc, ?_⟩
case inr.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
obtain ⟨ec, hc⟩ : ∃ ec : Trivialization F (π E), c ∈ ec.baseSet :=
  ⟨trivializationAt F E c, mem_baseSet_trivializationAt F E c⟩
case inr.intro.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case inr.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
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)
case inr.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case inr.intro.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2
case inr.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case inr.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
refine' ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 _⟩
no goals
case inr.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
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⟩⟩
no goals
case inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
rwa [← heq]
no goals
case intro.inr.intro.intro.inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
exact ⟨ec, heq ▸ hec⟩
case intro.inr.intro.intro.inr.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case intro.inr.intro.intro.inr
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
rcases this with  ⟨d, hdcb, hd⟩
no goals
case intro.inr.intro.intro.inr.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
exact ((hsc.1 ⟨⟨hc.1.trans hdcb.1.le, hdcb.2⟩, hd⟩).not_lt hdcb.1).elim
case pos.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case pos
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
obtain ⟨ed, hed⟩ : ∃ ed : Trivialization F (π E), d ∈ ed.baseSet :=
  ⟨trivializationAt F E d, mem_baseSet_trivializationAt F E d⟩
case pos.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case pos.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
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 => _⟩
case pos.intro.inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case pos.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
rcases hx.2.eq_or_lt with (rfl | hxd)
no goals
case pos.intro.inl
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
exacts [Or.inr ⟨hed, hdcb.1⟩, Or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩]
case neg
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case neg
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
rw [disjoint_left] at he
case neg
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case neg
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
push_neg  at he
case neg.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
case neg
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
rcases he with ⟨d', hdd' : d' < d, hd'c⟩
no goals
case neg.intro.intro
ι : Type ?u.12142
B : Type u_1
F : Type u_2
X : Type ?u.12151
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace 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
exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩