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 : 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
⊢ ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a b ⊆ e.baseSet
have rsuffices : ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
Tactic: rsuffices ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, ∃ e : Trivialization F (π F E), Icc a d ⊆ e.baseSet
-- 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
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
have 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
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⟩))
-- 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
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
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
have had : Ico a d ⊆ ec.baseSet
Tactic: have had : Ico a d ⊆ ec.baseSet := Ico_subset_Icc_union_Ico.trans (union_subset hec hd)
-- 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
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a 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
have 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
Tactic: by_cases he : Disjoint (Iio d) (Ioi 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 : 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
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
have 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
Tactic: by_cases he : Disjoint (Iio d) (Ioi 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 : 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)
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
have 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
Tactic: obtain ⟨ed, hed⟩ : ∃ ed : Trivialization F (π F E), d ∈ ed.baseSet :=
      ⟨trivializationAt F E d, mem_baseSet_trivializationAt F E d⟩
-- 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
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))
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
have pos : ∀ (x : B) (hx : x ∈ Icc a d), x ∈ ((ec.restrOpen (Iio d) sorry).disjointUnion (ed.restrOpen (Ioi c) sorry) sorry).baseSet
Tactic: 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 => ?_⟩
-- 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
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))
hed : d ∈ ed.baseSet
x : B
hx : x ∈ Icc a d
⊢ x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet
have pos : ∀ (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 ∈ ((ec.restrOpen (Iio x) sorry).disjointUnion (ed.restrOpen (Ioi c) sorry) sorry).baseSet
Tactic: rcases hx.2.eq_or_lt with (rfl | hxd)
Cleared hypotheses: d, hdcb, hd, had, he, hed, hx
-- 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
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))
hed : d ∈ ed.baseSet
x : B
hx : x ∈ Icc a d
pos :
  ∀ (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 ∈ ((ec.restrOpen (Iio x) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet
⊢ x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet
have pos₁ : ∀ (hxd : x < d), x ∈ ((ec.restrOpen (Iio d) sorry).disjointUnion (ed.restrOpen (Ioi c) sorry) sorry).baseSet
Tactic: rcases hx.2.eq_or_lt with (rfl | hxd)
-- 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
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)
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
have he₁ : ¬∀ ⦃a : B⦄, a ∈ Iio d → a ∉ Ioi c
Tactic: rw [disjoint_left] at he
Cleared hypotheses: he
-- 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
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 : ¬∀ ⦃a : B⦄, a ∈ Iio d → a ∉ Ioi c
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
have he₁ : ∃ a ∈ Iio d, a ∈ Ioi c
Tactic: push Not at he
Cleared hypotheses: he
-- 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
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : ∃ a ∈ Iio d, a ∈ Ioi c
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet
have neg : ∀ (d' : B) (hdd' : d' < d) (hd'c : 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
Tactic: rcases he with ⟨d', hdd' : d' < d, hd'c⟩
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x, v) ∈ SProd.sprod (β := Set F) (Z.baseSet i ∩ Z.baseSet j) univ
⊢ (((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).1,
      Z.coordChange j i ((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).1
        ((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).2) =
    (x, v)
have hx₁ : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
Tactic: simp only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).1,
      Z.coordChange j i ((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).1
        ((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).2) =
    (x, v)
have dsimp : (x, Z.coordChange j i x (Z.coordChange i j x v)) = (x, v)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (x, Z.coordChange j i x (Z.coordChange i j x v)) = (x, v)
have a : x ∈ Z.baseSet i
Tactic: rw [coordChange_comp, Z.coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
a : x ∈ Z.baseSet i
⊢ (x, Z.coordChange j i x (Z.coordChange i j x v)) = (x, v)
have a₁ : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet i
Tactic: rw [coordChange_comp, Z.coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x, v) ∈ SProd.sprod (β := Set F) (Z.baseSet i ∩ Z.baseSet j) univ
⊢ (((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).1,
      Z.coordChange i j ((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).1
        ((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).2) =
    (x, v)
have hx₁ : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
Tactic: simp only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).1,
      Z.coordChange i j ((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).1
        ((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).2) =
    (x, v)
have dsimp : (x, Z.coordChange i j x (Z.coordChange j i x v)) = (x, v)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (x, Z.coordChange i j x (Z.coordChange j i x v)) = (x, v)
have a : x ∈ Z.baseSet j
Tactic: rw [Z.coordChange_comp, Z.coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
a : x ∈ Z.baseSet j
⊢ (x, Z.coordChange i j x (Z.coordChange j i x v)) = (x, v)
have a₁ : x ∈ Z.baseSet j ∩ Z.baseSet i ∩ Z.baseSet j
Tactic: rw [Z.coordChange_comp, Z.coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : TotalSpace.mk (E := Z.Fiber) x v ∈ Z.proj ⁻¹' Z.baseSet i
⊢ Eq (α := Z.TotalSpace)
    (TotalSpace.mk (E := Z.Fiber)
      (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
          Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
            (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
            (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).1
      (Z.coordChange i
        (Z.indexAt
          (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
              Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
                (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
                (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).1)
        (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
            Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
              (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
              (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).1
        (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v),
            Z.coordChange (Z.indexAt (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))) i
              (TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))
              (TotalSpace.snd (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) x v))).2))
    (TotalSpace.mk (E := Z.Fiber) x v)
have hx₁ : x ∈ Z.baseSet i
Tactic: replace hx : x ∈ Z.baseSet i := hx
Cleared hypotheses: hx