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 : FiberBundle F E
x : TotalSpace F E
⊢ ((↑(trivializationAt F E (x.proj (E := E))) : TotalSpace F E → B × F) x).1 = x.proj (E := E)

Tactic:
Trivialization.coe_fst' _ <| mem_baseSet_trivializationAt F E x.proj

Premises used: Bundle.Trivialization.coe_fst', Bundle.TotalSpace.proj, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
E : B → Type u_5
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (b : B) → TopologicalSpace (E b)
inst_5 : FiberBundle F E
f : X → TotalSpace F E
s : Set X
x₀ : X
⊢ ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt.{u_4, u_2} (Y := B) (fun (x : X) ↦ (f x).proj (E := E)) s x₀ ∧
      ContinuousWithinAt.{u_4, u_3} (Y := F)
        (fun (x : X) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀

Tactic:
(trivializationAt F E (f x₀).proj).tendsto_nhds_iff mem_trivializationAt_proj_source

Premises used: ContinuousWithinAt, Bundle.TotalSpace.proj, Bundle.Trivialization.tendsto_nhds_iff, FiberBundle.trivializationAt, FiberBundle.mem_trivializationAt_proj_source
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
E : B → Type u_5
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (b : B) → TopologicalSpace (E b)
inst_5 : FiberBundle F E
f : X → TotalSpace F E
x₀ : X
⊢ ContinuousAt f x₀ ↔
    ContinuousAt.{u_4, u_2} (Y := B) (fun (x : X) ↦ (f x).proj (E := E)) x₀ ∧
      ContinuousAt.{u_4, u_3} (Y := F)
        (fun (x : X) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
(trivializationAt F E (f x₀).proj).tendsto_nhds_iff mem_trivializationAt_proj_source

Premises used: ContinuousAt, Bundle.TotalSpace.proj, Bundle.Trivialization.tendsto_nhds_iff, FiberBundle.trivializationAt, FiberBundle.mem_trivializationAt_proj_source
-- 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 : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
simp_rw :
  ContinuousWithinAt.{u_2, u_3} (Y := F)
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a
      x₀ →
    ContinuousWithinAt (Y := B) (fun (x : B) ↦ x) a x₀
⊢ ContinuousWithinAt (Y := TotalSpace F E) (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a x₀ ↔
    ContinuousWithinAt.{u_2, u_3} (Y := F)
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀

Tactic:
simp_rw [continuousWithinAt_totalSpace, and_iff_right_iff_imp]

Premises used: FiberBundle.continuousWithinAt_totalSpace, and_iff_right_iff_imp
-- 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 : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
h :
  ContinuousWithinAt.{u_2, u_3} (Y := F)
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀
⊢ ContinuousWithinAt (Y := B) (fun (x : B) ↦ x) a x₀

Tactic:
continuousWithinAt_id

Premises used: continuousWithinAt_id
-- 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 : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
h :
  ContinuousWithinAt.{u_2, u_3} (Y := F)
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀
⊢ ContinuousWithinAt (Y := B) (fun (x : B) ↦ x) a x₀

Tactic:
exact continuousWithinAt_id

Premises used: continuousWithinAt_id
-- 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 : FiberBundle F E
s : (x : B) → E x
x₀ : B
simp_rw :
  ContinuousWithinAt (Y := TotalSpace F E) (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) univ x₀ ↔
    ContinuousWithinAt.{u_2, u_3} (Y := F)
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) univ x₀
⊢ ContinuousAt (Y := TotalSpace F E) (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) x₀ ↔
    ContinuousAt.{u_2, u_3} (Y := F)
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) x₀

Tactic:
simp_rw [← continuousWithinAt_univ]

Premises used: continuousWithinAt_univ
-- 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 : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContinuousWithinAt (Y := TotalSpace F E) (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) univ x₀ ↔
    ContinuousWithinAt.{u_2, u_3} (Y := F)
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) univ x₀

Tactic:
continuousWithinAt_section F

Premises used: FiberBundle.continuousWithinAt_section
-- 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 : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContinuousWithinAt (Y := TotalSpace F E) (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) univ x₀ ↔
    ContinuousWithinAt.{u_2, u_3} (Y := F)
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) univ x₀

Tactic:
exact continuousWithinAt_section F

Premises used: FiberBundle.continuousWithinAt_section
-- 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))), a ∈ ea.baseSet

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

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
obtain :
  ∀ (ea : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) (hea : a ∈ ea.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 ⟨ea, hea⟩ : ∃ ea : Trivialization F (π F E), a ∈ ea.baseSet :=
    ⟨trivializationAt F E a, mem_baseSet_trivializationAt F E a⟩

Premises used: 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
inl : b < a → ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
inr :
  ∀ (hab : a ≤ 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 lt_or_ge b a with _ | hab

Premises used: lt_or_ge
-- 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
h : b < a
⊢ Icc a b ⊆ ea.baseSet

Tactic:
simp [*]
-- 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
h : b < a
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet

Tactic:
exact ⟨ea, by simp [*]⟩
-- 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}
⊢ Icc a a ⊆ ea.baseSet

Tactic:
simp [hea]
-- 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}
⊢ a ∈ s

Tactic:
have ha : a ∈ s := ⟨left_mem_Icc.2 hab, ea, by simp [hea]⟩
-- 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
⊢ s.Nonempty

Tactic:
have sne : s.Nonempty := ⟨a, ha⟩
-- 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
⊢ b ∈ upperBounds s

Tactic:
have hsb : b ∈ upperBounds s := fun x hx => 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
⊢ BddAbove s

Tactic:
have sbd : BddAbove s := ⟨b, hsb⟩
-- 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
⊢ IsLUB s c

Tactic:
have hsc : IsLUB s c := isLUB_csSup sne sbd
-- 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
⊢ c ∈ Icc a b

Tactic:
have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
-- 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
inl : ∀ (heq : a = c), c ∈ s
inr : ∀ (hlt : a < c), c ∈ s
⊢ c ∈ s

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

Premises used: LE.le.eq_or_lt, And.left
-- 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
heq : a = c
inl inl₁ inl₂ inl₃ : a ∈ s
⊢ c ∈ s

Tactic:
rwa [← heq]
-- 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
hlt : a < c
⊢ c ∈ s

Tactic:
⟨hc, ?_⟩

Premises used: Set.Mem, setOf, And.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
hlt : a < c
inr : ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet
⊢ c ∈ s

Tactic:
refine ⟨hc, ?_⟩
-- 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
hlt : a < c
⊢ ∃ (ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), c ∈ ec.baseSet

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

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
hlt : a < c
inr :
  ∀ (ec : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) (hc : c ∈ ec.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 ⟨ec, hc⟩ : ∃ ec : Trivialization F (π F E), c ∈ ec.baseSet :=
      ⟨trivializationAt F E c, mem_baseSet_trivializationAt F E c⟩

Premises used: 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_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' ∈ Ico a c, Ioc c' c ⊆ ec.baseSet

Tactic:
(mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset hlt).1
        (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet hc)

Premises used: Set.Mem, Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, Iff.mp, mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset
-- 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
inr :
  ∀ (c' : B) (hc' : c' ∈ Ico a c) (hc'e : Ioc c' c ⊆ ec.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 ⟨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)

Premises used: Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, Set.Ico, IsOpen.mem_nhds, Iff.mp, Bundle.Trivialization.baseSet, mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset
-- 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 ∈ s, d ∈ Ioc c' c

Tactic:
hsc.exists_between hc'.2

Premises used: Set.Ioc, Set.Mem, IsLUB.exists_between, setOf, And.right