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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
⊢ ContinuousOn f₂ (e₁.source ×ˢ e₂.source)

Tactic:
have hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source) :=
    e₁.toOpenPartialHomeomorph.continuousOn.prodMap e₂.toOpenPartialHomeomorph.continuousOn
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃

Tactic:
fun_prop
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃

Tactic:
have hf₃ : Continuous f₃ := by fun_prop
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
⊢ ContinuousOn (toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
    (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))

Tactic:
((hf₃.comp_continuousOn hf₂).comp hf₁.continuousOn ?_).congr ?_

Premises used: Continuous.continuousOn, Continuous.comp_continuousOn, ContinuousOn.comp, ContinuousOn.congr
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
refine_1 :
  MapsTo f₁ (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    (e₁.source ×ˢ e₂.source)
refine_2 :
  EqOn (toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂) ((f₃ ∘ f₂) ∘ f₁)
    (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
⊢ ContinuousOn (toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
    (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))

Tactic:
refine ((hf₃.comp_continuousOn hf₂).comp hf₁.continuousOn ?_).congr ?_

Premises used: Continuous.continuousOn, Continuous.comp_continuousOn, ContinuousOn.comp, ContinuousOn.congr
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
refine_1 :
  MapsTo f₁ (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    (SProd.sprod (α := Set (TotalSpace F₁ E₁)) (β := Set (TotalSpace F₂ E₂)) (TotalSpace.proj (E := E₁) ⁻¹' e₁.baseSet)
      (TotalSpace.proj (E := E₂) ⁻¹' e₂.baseSet))
⊢ MapsTo f₁ (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    (e₁.source ×ˢ e₂.source)

Tactic:
rw [e₁.source_eq, e₂.source_eq]

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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
⊢ MapsTo f₁ (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    (SProd.sprod (α := Set (TotalSpace F₁ E₁)) (β := Set (TotalSpace F₂ E₂)) (TotalSpace.proj (E := E₁) ⁻¹' e₁.baseSet)
      (TotalSpace.proj (E := E₂) ⁻¹' e₂.baseSet))

Tactic:
mapsTo_preimage _ _

Premises used: Set.Mem, setOf, Set.prod, Set.mapsTo_preimage, Set.preimage, Set.MapsTo
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
⊢ MapsTo f₁ (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    (SProd.sprod (α := Set (TotalSpace F₁ E₁)) (β := Set (TotalSpace F₂ E₂)) (TotalSpace.proj (E := E₁) ⁻¹' e₁.baseSet)
      (TotalSpace.proj (E := E₂) ⁻¹' e₂.baseSet))

Tactic:
exact mapsTo_preimage _ _

Premises used: Set.mapsTo_preimage
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₁.baseSet
right :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₂.baseSet
refine_2 : b = ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) (TotalSpace.mk (E := E₁) b v₁)).1
⊢ toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) =
    ((f₃ ∘ f₂) ∘ f₁) (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂))

Tactic:
simp only [f₁, f₂, f₃, Prod.toFun', Prod.mk_inj, Function.comp_apply, and_true]

Premises used: and_true, Prod.mk_inj, Function.comp_apply, Bundle.Trivialization.Prod.toFun'
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₁.baseSet
right :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₂.baseSet
refine_2 : TotalSpace.mk (E := E₁) b v₁ ∈ e₁.source
⊢ b = ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) (TotalSpace.mk (E := E₁) b v₁)).1

Tactic:
rw [e₁.coe_fst]

Premises used: Bundle.Trivialization.coe_fst
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₁.baseSet
right :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₂.baseSet
refine_2 : TotalSpace.proj.{u_1, u_2, u_3} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) b v₁) ∈ e₁.baseSet
⊢ TotalSpace.mk (E := E₁) b v₁ ∈ e₁.source

Tactic:
rw [e₁.source_eq, mem_preimage]

Premises used: Bundle.Trivialization.source_eq, Set.mem_preimage
-- 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₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → 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)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₁.baseSet
right :
  TotalSpace.proj (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) b (v₁, v₂)) ∈
    e₂.baseSet
⊢ TotalSpace.proj.{u_1, u_2, u_3} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) b v₁) ∈ e₁.baseSet

Tactic:
hb₁

Premises used: Set.Mem