awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc_1 : c ∈ Icc a b
hlt : a < c
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hc : c ∈ ec.baseSet
c' : B
hc' : c' ∈ Ico a c
hc'e : Ioc c' c ⊆ ec.baseSet
inr :
  ∀ (d : B) (hd : d ∈ Ioc c' c) (hdab : d ∈ Icc a b)
    (ead : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) (had : Icc a d ⊆ ead.baseSet),
    ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet

Tactic:
obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2

Premises used: Set.Ioc, IsLUB.exists_between, And.right
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc_1 : c ∈ Icc a b
hlt : a < c
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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 (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
had : Icc a d ⊆ ead.baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet

Tactic:
⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 ?_⟩

Premises used: Iff.mpr, le_rfl, Set.subset_ite, And.left, And.intro, Exists.intro, Bundle.Trivialization.piecewiseLe
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc_1 : c ∈ Icc a b
hlt : a < c
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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 (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
had : Icc a d ⊆ ead.baseSet
inr :
  Icc a c ∩ Iic d ⊆ ead.baseSet ∧ Icc a c \ Iic d ⊆ (ec.transFiberHomeomorph (ec.coordChangeHomeomorph ead ⋯ ⋯)).baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet

Tactic:
refine ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 ?_⟩
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc_1 : c ∈ Icc a b
hlt : a < c
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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 (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
had : Icc a d ⊆ ead.baseSet
⊢ Icc a c ∩ Iic d ⊆ ead.baseSet ∧ Icc a c \ Iic d ⊆ (ec.transFiberHomeomorph (ec.coordChangeHomeomorph ead ⋯ ⋯)).baseSet

Tactic:
⟨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⟩⟩

Premises used: not_le, And.right, And.left, And.intro, Iff.mp, LT.lt.trans
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc_1 : c ∈ Icc a b
hlt : a < c
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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 (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
had : Icc a d ⊆ ead.baseSet
⊢ Icc a c ∩ Iic d ⊆ ead.baseSet ∧ Icc a c \ Iic d ⊆ (ec.transFiberHomeomorph (ec.coordChangeHomeomorph ead ⋯ ⋯)).baseSet

Tactic:
exact ⟨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⟩⟩
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
inr :
  ∀ (ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) (hec : Icc a c ⊆ ec.baseSet),
    ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
obtain ⟨-, ec : Trivialization F (π F E), hec : Icc a c ⊆ ec.baseSet⟩ : c ∈ s := by
    rcases 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_nhdsLE_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 ?_⟩
    exact ⟨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⟩⟩

Premises used: Bundle.TotalSpace.proj, Set.Icc, Bundle.Trivialization
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
inr :
  ∀ (heq : c = b),
    ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
inr₁ :
  ∀ (hlt : c < b),
    ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
rcases hc.2.eq_or_lt with heq | hlt

Premises used: LE.le.eq_or_lt, And.right
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
heq : c = b
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
⟨ec, heq ▸ hec⟩

Premises used: Eq.rec, Exists.intro
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
heq : c = b
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
exact ⟨ec, heq ▸ hec⟩
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
inr :
  ∀ (d : B) (hdcb : d ∈ Ioc c b)
    (hd : ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet),
    ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
rsuffices :
  ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
rsuffices ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, ∃ e : Trivialization F (π F E), Icc a d ⊆ e.baseSet

Premises used: Set.Ioc, Bundle.TotalSpace.proj, Bundle.Trivialization
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
((hsc.1 ⟨⟨hc.1.trans hdcb.1.le, hdcb.2⟩, hd⟩).not_gt hdcb.1).elim

Premises used: False.elim, LT.lt.le, And.right, LE.le.not_gt, And.left, And.intro, LE.le.trans
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
exact ((hsc.1 ⟨⟨hc.1.trans hdcb.1.le, hdcb.2⟩, hd⟩).not_gt hdcb.1).elim

Premises used: False.elim, LT.lt.le, And.right, LE.le.not_gt, And.left, And.intro, LE.le.trans
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
⊢ ∃ d ∈ Ioc c b, Ico c d ⊆ ec.baseSet

Tactic:
(mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hlt).1
      (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet (hec ⟨hc.1, le_rfl⟩))

Premises used: le_rfl, Set.Mem, Bundle.Trivialization.open_baseSet, mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset, mem_nhdsWithin_of_mem_nhds, And.left, And.intro, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
obtain :
  ∀ (d : B) (hdcb : d ∈ Ioc c b) (hd : Ico c d ⊆ ec.baseSet),
    ∃ d ∈ Ioc c b,
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet

Tactic:
obtain ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, Ico c d ⊆ ec.baseSet :=
    (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hlt).1
      (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet (hec ⟨hc.1, le_rfl⟩))

Premises used: Set.Ioc, le_rfl, Bundle.Trivialization.open_baseSet, mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset, mem_nhdsWithin_of_mem_nhds, And.left, And.intro, IsOpen.mem_nhds, Iff.mp, Bundle.Trivialization.baseSet
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
⊢ Ico a d ⊆ ec.baseSet

Tactic:
have had : Ico a d ⊆ ec.baseSet := Ico_subset_Icc_union_Ico.trans (union_subset hec hd)
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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
pos :
  ∀ (he : Disjoint (Iio d) (Ioi c)),
    ∃ d ∈ Ioc c b,
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
neg :
  ∀ (he : ¬Disjoint (Iio d) (Ioi c)),
    ∃ d ∈ Ioc c b,
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet

Tactic:
by_cases he : Disjoint (Iio d) (Ioi c)

Premises used: Set.Ioi, Disjoint, Set.Iio
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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 (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), d ∈ ed.baseSet

Tactic:
⟨trivializationAt F E d, mem_baseSet_trivializationAt F E d⟩

Premises used: FiberBundle.trivializationAt, Exists.intro, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : ConditionallyCompleteLinearOrder B
inst_5 : OrderTopology B
inst_6 : FiberBundle F E
a b : B
ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B :=
  {x : B |
    x ∈ Icc a b ∧
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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)
pos :
  ∀ (ed : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) (hed : d ∈ ed.baseSet),
    ∃ d ∈ Ioc c b,
      ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet

Tactic:
obtain ⟨ed, hed⟩ : ∃ ed : Trivialization F (π F E), d ∈ ed.baseSet :=
      ⟨trivializationAt F E d, mem_baseSet_trivializationAt F E d⟩

Premises used: Bundle.TotalSpace.proj, Bundle.Trivialization