awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
h :
  (↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F) ∘
      Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) =
    (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F)
⊢ ContinuousOn
    ((↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F) ∘
      Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s))
    e.toPretrivialization.source

Tactic:
convert! e.continuousOn_toFun

Premises used: OpenPartialHomeomorph.continuousOn_toFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
h :
  ∀ (x : Z) (hx : proj x ∈ s),
    comp (α := { x : Z // x ∈ proj ⁻¹' s }) (↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F)
        (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) x hx) =
      (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F) (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) x hx)
⊢ (↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F) ∘
      Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) =
    (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F)

Tactic:
ext1 ⟨x, (hx : proj x ∈ s)⟩
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
x : Z
hx : proj x ∈ s
⊢ comp (α := { x : Z // x ∈ proj ⁻¹' s }) (↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F)
      (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) x hx) =
    (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F) (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) x hx)

Tactic:
simpa [Pretrivialization.domExtend] using dif_pos hx

Premises used: dif_pos, Bundle.Pretrivialization.domExtend
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
⊢ ContinuousOn e.invFun e.target

Tactic:
e.continuousOn_invFun

Premises used: OpenPartialHomeomorph.continuousOn_invFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
⊢ ContinuousOn e.toPretrivialization.invFun e.toPretrivialization.domExtend (s := s).target

Tactic:
convert! e.continuousOn_invFun

Premises used: OpenPartialHomeomorph.continuousOn_invFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj_1 : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
⊢ ContinuousOn e.invFun e.target

Tactic:
e.continuousOn_invFun

Premises used: OpenPartialHomeomorph.continuousOn_invFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj_1 : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
h :
  (Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
      Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id =
    e.invFun
⊢ ContinuousOn
    ((Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
      Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id)
    e.toPretrivialization.target

Tactic:
convert! e.continuousOn_invFun

Premises used: OpenPartialHomeomorph.continuousOn_invFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj_1 : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
h :
  ∀ (x : Prod.{u_1, u_2} { x : B // x ∈ s } F),
    ((Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
          Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id)
        x =
      e.invFun x
⊢ (Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
      Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id =
    e.invFun

Tactic:
ext
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj_1 : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
x_1 : Prod.{u_1, u_2} { x : B // x ∈ s } F
h : (↑e.toPretrivialization.symm : (↑s : Type u_1) × F → Z) x_1 = (↑e.symm : (↑s : Type u_1) × F → Z) x_1
⊢ ((Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
        Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id)
      x_1 =
    e.invFun x_1

Tactic:
simp [Pretrivialization.codExtend']

Premises used: Bundle.Pretrivialization.codExtend'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj_1 : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
x_1 : Prod.{u_1, u_2} { x : B // x ∈ s } F
⊢ (↑e.toPretrivialization.symm : (↑s : Type u_1) × F → Z) x_1 = (↑e.symm : (↑s : Type u_1) × F → Z) x_1

Tactic:
rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
rw :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' frontier (SProd.sprod (β := Set F) s univ) =
    proj ⁻¹' (e.baseSet ∩ frontier s)
rw₁ :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' SProd.sprod (β := Set F) (frontier s) univ =
    proj ⁻¹' (e.baseSet ∩ frontier s)
rw₂ : e.source ∩ proj ⁻¹' frontier s = proj ⁻¹' (e.baseSet ∩ frontier s)
rw₃ : proj ⁻¹' e.baseSet ∩ proj ⁻¹' frontier s = proj ⁻¹' (e.baseSet ∩ frontier s)
rw₄ rw₅ : proj ⁻¹' e.baseSet ∩ proj ⁻¹' frontier s = proj ⁻¹' e.baseSet ∩ proj ⁻¹' frontier s
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)

Tactic:
rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
    (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]

Premises used: Set.preimage_inter, Bundle.Trivialization.source_eq, Bundle.Trivialization.isImage_preimage_prod, frontier_prod_univ_eq, OpenPartialHomeomorph.IsImage.preimage_eq, OpenPartialHomeomorph.IsImage.frontier
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
rw : proj ⁻¹' (e.baseSet ∩ frontier s) = e'.source ∩ frontier (proj ⁻¹' s)
rw₁ : proj ⁻¹' (e.baseSet ∩ frontier s) = proj ⁻¹' (e'.baseSet ∩ frontier s)
rw₂ rw₃ : proj ⁻¹' (e'.baseSet ∩ frontier s) = proj ⁻¹' (e'.baseSet ∩ frontier s)
⊢ e.source ∩ frontier (proj ⁻¹' s) = e'.source ∩ frontier (proj ⁻¹' s)

Tactic:
rw [e.frontier_preimage, e'.frontier_preimage, Hs]

Premises used: Bundle.Trivialization.frontier_preimage
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
rwa rwa₁ rwa₂ rwa₃ :
  EqOn (↑e.toOpenPartialHomeomorph : Z → B × F) (↑e'.toOpenPartialHomeomorph : Z → B × F)
    (proj ⁻¹' (e.baseSet ∩ frontier s))
⊢ EqOn (↑e.toOpenPartialHomeomorph : Z → B × F) (↑e'.toOpenPartialHomeomorph : Z → B × F)
    (e.source ∩ frontier (proj ⁻¹' s))

Tactic:
rwa [e.frontier_preimage]

Premises used: Bundle.Trivialization.frontier_preimage
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
⊢ (e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (SProd.sprod (β := Set F) s univ) ⋯ ⋯ ⋯ ⋯).source =
    proj ⁻¹' s.ite e.baseSet e'.baseSet

Tactic:
simp [source_eq]

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
⊢ (e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (SProd.sprod (β := Set F) s univ) ⋯ ⋯ ⋯ ⋯).target =
    SProd.sprod (β := Set F) (s.ite e.baseSet e'.baseSet) univ

Tactic:
simp [target_eq, prod_univ]

Premises used: Set.prod_univ, Bundle.Trivialization.target_eq
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e.source
hs : p ∈ proj ⁻¹' s
⊢ ((↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (SProd.sprod (β := Set F) s univ) ⋯ ⋯ ⋯ ⋯) : Z → B × F) p).1 =
    proj p

Tactic:
simp [*]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e'.source
hs : p ∉ proj ⁻¹' s
⊢ ((↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (SProd.sprod (β := Set F) s univ) ⋯ ⋯ ⋯ ⋯) : Z → B × F) p).1 =
    proj p

Tactic:
simp [*]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
⊢ x = a

Tactic:
mem_singleton_iff.1 (frontier_Iic_subset _ hx)

Premises used: Set.mem_singleton_iff, Iff.mp, frontier_Iic_subset
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
⊢ x ∈ e.baseSet

Tactic:
obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)

Premises used: Set.mem_singleton_iff, Iff.mp, frontier_Iic_subset, rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
He₁ : x ∈ e.baseSet
⊢ x ∈ e'.baseSet

Tactic:
obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)

Premises used: Set.mem_singleton_iff, Iff.mp, frontier_Iic_subset, rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
He₁ : x ∈ e.baseSet
He'₁ : x ∈ e'.baseSet
⊢ ∀ (p : Z), proj p = x → (↑e : Z → B × F) p = (↑e' : Z → B × F) p

Tactic:
obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)

Premises used: Set.mem_singleton_iff, Iff.mp, frontier_Iic_subset, rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
He₁ : x ∈ e.baseSet
He'₁ : x ∈ e'.baseSet
Heq₁ : ∀ (p : Z), proj p = x → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
⊢ x ∈ frontier (Iic x)

Tactic:
obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)

Premises used: Set.mem_singleton_iff, Iff.mp, frontier_Iic_subset, rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
x : B
He : x ∈ e.baseSet
He' : x ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = x → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
hx : x ∈ frontier (Iic x)
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet

Tactic:
simp [He, He']
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
fst : ((↑e : Z → B × F) p).1 = ((↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p).1
snd : ((↑e : Z → B × F) p).2 = ((↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p).2
⊢ (↑e : Z → B × F) p = (↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p

Tactic:
ext1
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
⊢ ((↑e : Z → B × F) p).1 = ((↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p).1

Tactic:
simp [*]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
⊢ ((↑e : Z → B × F) p).2 = ((↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p).2

Tactic:
simp [*]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
rw : Disjoint (proj ⁻¹' e.baseSet) (proj ⁻¹' e'.baseSet)
⊢ Disjoint e.source e'.source

Tactic:
rw [e.source_eq, e'.source_eq]

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint (proj ⁻¹' e.baseSet) (proj ⁻¹' e'.baseSet)

Tactic:
H.preimage _

Premises used: Disjoint.preimage
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint (proj ⁻¹' e.baseSet) (proj ⁻¹' e'.baseSet)

Tactic:
exact H.preimage _

Premises used: Disjoint.preimage