awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
x : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)
⊢ Membership.mem (γ := Set (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
      (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) x ↔
    Membership.mem (γ := Set (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
      ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
          (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
            TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ⁻¹'
        e₁.source ×ˢ e₂.source)
      x

Tactic:
simp only [Trivialization.source_eq, mfld_simps]

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
⊢ (↑(e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).symm : B × F₁ × F₂ → TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x)
      (x, w₁, w₂) =
    TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (e₁.symm (E := E₁) x w₁, e₂.symm (E := E₂) x w₂)

Tactic:
rfl

Premises used: Bundle.Trivialization.Prod.invFun', rfl
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
inst_7 : (x : B) → TopologicalSpace (E₁ x)
inst_8 : (x : B) → TopologicalSpace (E₂ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : FiberBundle F₂ E₂
b : B
rw :
  IsInducing (X := Prod.{u_3, u_5} (E₁ b) (E₂ b)) (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
    ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
          (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
            TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ∘
        TotalSpace.mk (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b :
      Prod.{u_3, u_5} (E₁ b) (E₂ b) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
⊢ IsInducing (X := Prod.{u_3, u_5} (E₁ b) (E₂ b)) (Y :=
    TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
    (TotalSpace.mk (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b)

Tactic:
rw [← (Prod.isInducing_diag F₁ E₁ F₂ E₂).of_comp_iff]

Premises used: FiberBundle.Prod.isInducing_diag, Topology.IsInducing.of_comp_iff
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
inst_7 : (x : B) → TopologicalSpace (E₁ x)
inst_8 : (x : B) → TopologicalSpace (E₂ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : FiberBundle F₂ E₂
b : B
⊢ IsInducing (X := Prod.{u_3, u_5} (E₁ b) (E₂ b)) (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
    ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
          (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
            TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ∘
        TotalSpace.mk (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b :
      Prod.{u_3, u_5} (E₁ b) (E₂ b) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂)

Tactic:
(totalSpaceMk_isInducing F₁ E₁ b).prodMap (totalSpaceMk_isInducing F₂ E₂ b)

Premises used: Topology.IsInducing.prodMap, FiberBundle.totalSpaceMk_isInducing
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
inst_7 : (x : B) → TopologicalSpace (E₁ x)
inst_8 : (x : B) → TopologicalSpace (E₂ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : FiberBundle F₂ E₂
b : B
⊢ IsInducing (X := Prod.{u_3, u_5} (E₁ b) (E₂ b)) (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
    ((fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
          (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
            TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
              p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)) ∘
        TotalSpace.mk (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b :
      Prod.{u_3, u_5} (E₁ b) (E₂ b) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂)

Tactic:
exact (totalSpaceMk_isInducing F₁ E₁ b).prodMap (totalSpaceMk_isInducing F₂ E₂ b)

Premises used: Topology.IsInducing.prodMap, FiberBundle.totalSpaceMk_isInducing
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
rw :
  induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
    induced (TotalSpace.proj (E := f *ᵖ E)) inst
⊢ Continuous[TotalSpace.topologicalSpace F E f, inst] (TotalSpace.proj (E := f *ᵖ E))

Tactic:
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]

Premises used: Pullback.TotalSpace.topologicalSpace, pullbackTopology_def, continuous_iff_le_induced
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
    induced (TotalSpace.proj (E := f *ᵖ E)) inst

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
    induced (TotalSpace.proj (E := f *ᵖ E)) inst

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
rw :
  induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
    induced (Pullback.lift (E := E) f) inst_1
⊢ Continuous[TotalSpace.topologicalSpace F E f, inst_1] (Pullback.lift (E := E) f)

Tactic:
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]

Premises used: Pullback.TotalSpace.topologicalSpace, pullbackTopology_def, continuous_iff_le_induced
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
    induced (Pullback.lift (E := E) f) inst_1

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 ≤
    induced (Pullback.lift (E := E) f) inst_1

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
eq_induced :
  Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding (E := E) f) instTopologicalSpaceProd
⊢ IsInducing (X := TotalSpace F (f *ᵖ E)) (pullbackTotalSpaceEmbedding (E := E) f)

Tactic:
constructor
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
eq_induced :
  induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 =
    induced (Prod.fst ∘ pullbackTotalSpaceEmbedding (E := E) f) inst ⊓
      induced (Prod.snd ∘ pullbackTotalSpaceEmbedding (E := E) f) inst_1
⊢ Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding (E := E) f) instTopologicalSpaceProd

Tactic:
simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose,
    Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]

Premises used: induced_inf, Pullback.TotalSpace.topologicalSpace, instTopologicalSpaceProd, pullbackTopology_def, induced_compose
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced (TotalSpace.proj (E := f *ᵖ E)) inst ⊓ induced (Pullback.lift (E := E) f) inst_1 =
    induced (Prod.fst ∘ pullbackTotalSpaceEmbedding (E := E) f) inst ⊓
      induced (Prod.snd ∘ pullbackTotalSpaceEmbedding (E := E) f) inst_1

Tactic:
rfl
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (x : B) → TopologicalSpace (E x)
inst_5 : FiberBundle F E
f : B' → B
x : B'
simp :
  instTopologicalSpacePullback E f x ≤
    induced (fun (x_1 : (f *ᵖ E) x) ↦ Pullback.lift (E := E) f (TotalSpace.mk (E := f *ᵖ E) x x_1)) inst_1
⊢ Continuous[instTopologicalSpacePullback E f x, TotalSpace.topologicalSpace F E f] (TotalSpace.mk (E := f *ᵖ E) x)

Tactic:
simp only [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, induced_compose,
    induced_inf, Function.comp_def, induced_const, top_inf_eq, pullbackTopology_def]

Premises used: induced_inf, induced_const, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def, induced_compose, top_inf_eq, continuous_iff_le_induced, Function.comp_def
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (x : B) → TopologicalSpace (E x)
inst_5 : FiberBundle F E
f : B' → B
x : B'
⊢ instTopologicalSpacePullback E f x ≤
    induced (fun (x_1 : (f *ᵖ E) x) ↦ Pullback.lift (E := E) f (TotalSpace.mk (E := f *ᵖ E) x x_1)) inst_1

Tactic:
(FiberBundle.totalSpaceMk_isInducing F E (f x)).eq_induced.le

Premises used: Bundle.Pullback, Eq.le, instTopologicalSpacePullback._aux_1, Bundle.Pullback.lift, FiberBundle.totalSpaceMk_isInducing, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (x : B) → TopologicalSpace (E x)
inst_5 : FiberBundle F E
f : B' → B
x : B'
⊢ instTopologicalSpacePullback E f x ≤
    induced (fun (x_1 : (f *ᵖ E) x) ↦ Pullback.lift (E := E) f (TotalSpace.mk (E := f *ᵖ E) x x_1)) inst_1

Tactic:
exact (FiberBundle.totalSpaceMk_isInducing F E (f x)).eq_induced.le

Premises used: Eq.le, FiberBundle.totalSpaceMk_isInducing, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h :
  Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source) x
⊢ Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)

Tactic:
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj] at h

Premises used: Bundle.Trivialization.source_eq, Set.mem_preimage, Bundle.Pullback.lift_proj
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
simp_rw :
  Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) ∧
    Membership.mem (γ := Set F) univ ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2
simp_rw₁ :
  Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) ∧ True
simp_rw₂ : Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' e.baseSet) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E))
simp_rw₃ : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
⊢ (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
      ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) ∈
    SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ

Tactic:
simp_rw [prodMk_mem_set_prod_eq, mem_univ, and_true, mem_preimage, h]

Premises used: and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ, Set.mem_preimage
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
y : B' × F
h : y ∈ SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
⊢ Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B) ∧ Membership.mem (γ := Set F) univ y.2

Tactic:
rw [mem_prod, mem_preimage] at h

Premises used: Set.mem_prod, Set.mem_preimage
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
y : B' × F
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B) ∧ Membership.mem (γ := Set F) univ y.2
simp_rw :
  Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' TotalSpace.proj (E := E) ⁻¹' e.baseSet)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
simp_rw₁ :
  TotalSpace.proj.{u, v, w₁} (F := F) (E := E)
      (Pullback.lift (E := E) (⇑f : (a : B') → B)
        (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))) ∈
    e.baseSet
simp_rw₂ : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) y.1 : B)
⊢ Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
    (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))

Tactic:
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]

Premises used: Bundle.Trivialization.source_eq, And.left, Set.mem_preimage, Bundle.Pullback.lift_proj
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h :
  Membership.mem (γ := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source) x
⊢ Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)

Tactic:
simp_rw [mem_preimage, e.mem_source, Pullback.lift_proj] at h

Premises used: Bundle.Trivialization.mem_source, Set.mem_preimage, Bundle.Pullback.lift_proj
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
simp_rw simp_rw₁ :
  TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E))
      (e.symm (E := E) ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)))
        ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) =
    x
simp_rw₂ :
  TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E))
      (e.symm (E := E) ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)))
        ((↑e : TotalSpace F E → B × F)
            (TotalSpace.mk (E := E) ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)))
              (x.snd (E := (⇑f : (a : B') → B) *ᵖ E)))).2) =
    x
⊢ TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E)
      (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
          ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1
      (e.symm (E := E)
        ((f : (a : B') → B)
          (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
              ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1)
        (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
            ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).2) =
    x

Tactic:
simp_rw [Pullback.lift, e.symm_apply_apply_mk h]

Premises used: Bundle.Pullback.lift, Bundle.Trivialization.symm_apply_apply_mk
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : B' × F
h : x ∈ SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
⊢ Membership.mem (α := B) e.baseSet ((f : (a : B') → B) x.1 : B)

Tactic:
simp_rw [mem_prod, mem_preimage, mem_univ, and_true] at h

Premises used: and_true, Set.mem_prod, Set.mem_univ, Set.mem_preimage
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : B' × F
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) x.1 : B)
simp_rw simp_rw₁ :
  (x.1,
      ((↑e : TotalSpace F E → B × F)
          (Pullback.lift (E := E) (⇑f : (a : B') → B)
            (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))).2) =
    x
simp_rw₂ :
  (x.1,
      ((↑e : TotalSpace F E → B × F)
          (TotalSpace.mk (E := E) ((f : (a : B') → B) x.1) (e.symm (E := E) ((f : (a : B') → B) x.1) x.2))).2) =
    x
⊢ (TotalSpace.proj.{w₂, v, w₁} (F := F) (E := (⇑f : (a : B') → B) *ᵖ E)
        (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)),
      ((↑e : TotalSpace F E → B × F)
          (Pullback.lift (E := E) (⇑f : (a : B') → B)
            (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))).2) =
    x

Tactic:
simp_rw [Pullback.lift_mk, e.apply_mk_symm h]

Premises used: Bundle.Pullback.lift_mk, Bundle.Trivialization.apply_mk_symm
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
simp_rw :
  IsOpen[Pullback.TotalSpace.topologicalSpace F E (⇑f : (a : B') → B)]
    (TotalSpace.proj (E := E) ∘ Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.baseSet)
⊢ IsOpen[Pullback.TotalSpace.topologicalSpace F E (⇑f : (a : B') → B)]
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)

Tactic:
simp_rw [e.source_eq, ← preimage_comp]

Premises used: Bundle.Trivialization.source_eq, Set.preimage_comp