awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ 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₀
have 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₀
Tactic: simp_rw [continuousWithinAt_totalSpace, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ 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₀
have 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₀
Tactic: simp_rw [← continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have 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
Tactic: obtain ⟨ea, hea⟩ : ∃ ea : Trivialization F (π F E), a ∈ ea.baseSet :=
    ⟨trivializationAt F E a, mem_baseSet_trivializationAt F E a⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have inl : b < a → ∃ (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
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have inr : ∀ (hab : a ≤ b), ∃ (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
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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}
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have ha : a ∈ s
Tactic: have ha : a ∈ s := ⟨left_mem_Icc.2 hab, ea, by simp [hea]⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have sne : s.Nonempty
Tactic: have sne : s.Nonempty := ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have hsb : b ∈ upperBounds s
Tactic: have hsb : b ∈ upperBounds s := fun x hx => hx.1.2
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have sbd : BddAbove s
Tactic: have sbd : BddAbove s := ⟨b, hsb⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have hsc : IsLUB s c
Tactic: have hsc : IsLUB s c := isLUB_csSup sne sbd
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have hc : c ∈ Icc a b
Tactic: have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ c ∈ s
have inl : ∀ (heq : a = c), c ∈ s
Tactic: rcases hc.1.eq_or_lt with heq | hlt
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ c ∈ s
have inr : ∀ (hlt : a < c), c ∈ s
Tactic: rcases hc.1.eq_or_lt with heq | hlt
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
have inr : ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet
Tactic: refine ⟨hc, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet
have 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
Tactic: obtain ⟨ec, hc⟩ : ∃ ec : Trivialization F (π F E), c ∈ ec.baseSet :=
      ⟨trivializationAt F E c, mem_baseSet_trivializationAt F E c⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet
have 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
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)
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a c ⊆ e.baseSet
have 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
Tactic: obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
have inr : Icc a c ∩ Iic d ⊆ ead.baseSet ∧ Icc a c \ Iic d ⊆ (ec.transFiberHomeomorph (ec.coordChangeHomeomorph ead sorry sorry)).baseSet
Tactic: refine ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have inr : ∀ (heq : c = b), ∃ (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
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have inr₁ : ∀ (hlt : c < b), ∃ (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
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have 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
Tactic: rsuffices ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, ∃ e : Trivialization F (π F E), Icc a d ⊆ e.baseSet