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 : 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

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

Premises used: Set.Ioi, isOpen_Iio, isOpen_Ioi, And.intro, Exists.intro, Disjoint.mono, Bundle.Trivialization.disjointUnion, Set.Iio, Bundle.Trivialization.restrOpen, Set.inter_subset_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
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
pos : ∀ (x : B) (hx : x ∈ Icc a d), x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.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 => ?_⟩
-- 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))
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
pos₁ : ∀ (hxd : x < d), x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet
⊢ x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet

Tactic:
rcases hx.2.eq_or_lt with (rfl | hxd)

Premises used: LE.le.eq_or_lt, And.right, rfl
-- 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
ed : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : B
hdcb : x ∈ Ioc c b
hd : Ico c x ⊆ ec.baseSet
had : Ico a x ⊆ ec.baseSet
he : Disjoint (Iio x) (Ioi c)
hed : x ∈ ed.baseSet
hx : x ∈ Icc a x
⊢ x ∈ ((ec.restrOpen (Iio x) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet

Tactic:
Or.inr ⟨hed, hdcb.1⟩

Premises used: Set.union, Set.Mem, setOf, And.left, And.intro, Or.inr
-- 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))
hed : d ∈ ed.baseSet
x : B
hx : x ∈ Icc a d
hxd : x < d
⊢ x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet

Tactic:
Or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩

Premises used: Set.union, Set.Mem, setOf, And.left, And.intro, Or.inl
-- 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
ed : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : B
hdcb : x ∈ Ioc c b
hd : Ico c x ⊆ ec.baseSet
had : Ico a x ⊆ ec.baseSet
he : Disjoint (Iio x) (Ioi c)
hed : x ∈ ed.baseSet
hx : x ∈ Icc a x
⊢ x ∈ ((ec.restrOpen (Iio x) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet

Tactic:
exacts [Or.inr ⟨hed, hdcb.1⟩, Or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩]

Premises used: Or.inl, Or.inr
-- 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)
⊢ ¬∀ ⦃a : B⦄, a ∈ Iio d → a ∉ Ioi c

Tactic:
rw [disjoint_left] at he

Premises used: Set.disjoint_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
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
⊢ ∃ a ∈ Iio d, a ∈ Ioi c

Tactic:
push Not at he

Premises used: Not
-- 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 : ∃ a ∈ Iio d, a ∈ Ioi c
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
⊢ ∃ 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⟩
-- 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
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:
⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩

Premises used: HasSubset.Subset.trans, LT.lt.le, And.right, And.intro, Exists.intro, LE.le.trans, Set.Icc_subset_Ico_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
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
d' : B
hdd' : d' < d
hd'c : d' ∈ Ioi c
⊢ ∃ d ∈ Ioc c b, ∃ (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))), Icc a d ⊆ e.baseSet

Tactic:
exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩
-- Module: Mathlib.Topology.FiberBundle.Basic
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 : ι
p : B × F
hp : p ∈ SProd.sprod (β := Set F) (Z.baseSet i ∩ Z.baseSet j) univ
⊢ (p.1, Z.coordChange i j p.1 p.2) ∈ SProd.sprod (β := Set F) (Z.baseSet i ∩ Z.baseSet j) univ

Tactic:
simpa using hp
-- Module: Mathlib.Topology.FiberBundle.Basic
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 : ι
p : B × F
hp : p ∈ SProd.sprod (β := Set F) (Z.baseSet i ∩ Z.baseSet j) univ
⊢ (p.1, Z.coordChange j i p.1 p.2) ∈ SProd.sprod (β := Set F) (Z.baseSet i ∩ Z.baseSet j) univ

Tactic:
simpa using hp
-- Module: Mathlib.Topology.FiberBundle.Basic
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 ∈ Z.baseSet i ∧ x ∈ Z.baseSet j

Tactic:
simp only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx

Premises used: and_true, Set.mem_inter_iff, Set.prodMk_mem_set_prod_eq, Set.mem_univ
-- Module: Mathlib.Topology.FiberBundle.Basic
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
dsimp : (x, Z.coordChange j i x (Z.coordChange i j x v)) = (x, v)
⊢ (((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)

Tactic:
dsimp only
-- Module: Mathlib.Topology.FiberBundle.Basic
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
a₁ : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet i
⊢ (x, Z.coordChange j i x (Z.coordChange i j x v)) = (x, v)

Tactic:
rw [coordChange_comp, Z.coordChange_self]

Premises used: FiberBundleCore.coordChange_self, FiberBundleCore.coordChange_comp
-- Module: Mathlib.Topology.FiberBundle.Basic
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.baseSet i

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Topology.FiberBundle.Basic
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.baseSet i ∩ Z.baseSet j ∩ Z.baseSet i

Tactic:
⟨⟨hx.1, hx.2⟩, hx.1⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro
-- Module: Mathlib.Topology.FiberBundle.Basic
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.baseSet i

Tactic:
exacts [hx.1, ⟨⟨hx.1, hx.2⟩, hx.1⟩]

Premises used: And.left
-- Module: Mathlib.Topology.FiberBundle.Basic
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
dsimp : (x, Z.coordChange i j x (Z.coordChange j i x v)) = (x, v)
⊢ (((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)

Tactic:
dsimp only
-- Module: Mathlib.Topology.FiberBundle.Basic
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
a₁ : x ∈ Z.baseSet j ∩ Z.baseSet i ∩ Z.baseSet j
⊢ (x, Z.coordChange i j x (Z.coordChange j i x v)) = (x, v)

Tactic:
rw [Z.coordChange_comp, Z.coordChange_self]

Premises used: FiberBundleCore.coordChange_self, FiberBundleCore.coordChange_comp
-- Module: Mathlib.Topology.FiberBundle.Basic
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.baseSet j

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.Topology.FiberBundle.Basic
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.baseSet j

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Topology.FiberBundle.Basic
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.baseSet j ∩ Z.baseSet i ∩ Z.baseSet j

Tactic:
simp [hx]
-- Module: Mathlib.Topology.FiberBundle.Basic
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 : ι
⊢ ContinuousOn (Y := B × F) (fun (p : B × F) ↦ (p.1, Z.coordChange j i p.1 p.2))
    (SProd.sprod (β := Set F) (Z.baseSet i ∩ Z.baseSet j) univ)

Tactic:
simpa [inter_comm] using continuous_fst.continuousOn.prodMk (Z.continuousOn_coordChange j i)

Premises used: Continuous.continuousOn, continuous_fst, Set.inter_comm, ContinuousOn.prodMk, FiberBundleCore.continuousOn_coordChange
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∩ Z.baseSet j ∧ Membership.mem (γ := Set F) univ p.2 ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Tactic:
simp
-- Module: Mathlib.Topology.FiberBundle.Basic
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 : ι
p : Z.TotalSpace
hp : p ∈ Z.proj ⁻¹' Z.baseSet i
⊢ (p.proj (E := Z.Fiber),
      Z.coordChange (Z.indexAt (p.proj (E := Z.Fiber))) i (p.proj (E := Z.Fiber)) (p.snd (E := Z.Fiber))) ∈
    SProd.sprod (β := Set F) (Z.baseSet i) univ

Tactic:
simpa only [Set.mem_preimage, and_true, Set.mem_univ, Set.prodMk_mem_set_prod_eq] using hp

Premises used: and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ, Set.mem_preimage
-- Module: Mathlib.Topology.FiberBundle.Basic
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 : ι
p : B × F
hp : p ∈ SProd.sprod (β := Set F) (Z.baseSet i) univ
⊢ TotalSpace.mk (E := Z.Fiber) p.1 (Z.coordChange i (Z.indexAt p.1) p.1 p.2) ∈ Z.proj ⁻¹' Z.baseSet i

Tactic:
simpa only [Set.mem_preimage, and_true, Set.mem_univ, Set.mem_prod] using hp

Premises used: and_true, Set.mem_prod, Set.mem_univ, Set.mem_preimage
-- Module: Mathlib.Topology.FiberBundle.Basic
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
⊢ x ∈ Z.baseSet i

Tactic:
replace hx : x ∈ Z.baseSet i := hx
-- Module: Mathlib.Topology.FiberBundle.Basic
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 : x ∈ Z.baseSet i
dsimp :
  Eq (α := Z.TotalSpace)
    (TotalSpace.mk (E := Z.Fiber) x (Z.coordChange i (Z.indexAt x) x (Z.coordChange (Z.indexAt x) i x v)))
    (TotalSpace.mk (E := Z.Fiber) x v)
⊢ 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)

Tactic:
dsimp only