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₁
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:
exact hb₁
-- 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)
h :
  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
obtain :
  ∀ (x : B) (v₁ : E₁ x) (v₂ : E₂ x)
    (h :
      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))
        (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (v₁, v₂))),
    invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂
        (toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂
          (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (v₁, v₂))) =
      TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (v₁, v₂)
⊢ invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ x) = x

Tactic:
obtain ⟨x, v₁, v₂⟩ := x
-- 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
v₁ : E₁ x
v₂ : E₂ x
h :
  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))
    (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (v₁, v₂))
⊢ x ∈ e₁.baseSet

Tactic:
obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h

Premises used: Bundle.Trivialization.baseSet
-- 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
v₁ : E₁ x
v₂ : E₂ x
h :
  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))
    (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (v₁, v₂))
h₁ : x ∈ e₁.baseSet
⊢ x ∈ e₂.baseSet

Tactic:
obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h

Premises used: Bundle.Trivialization.baseSet
-- 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
v₁ : E₁ x
v₂ : E₂ x
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂
      (toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂
        (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (v₁, v₂))) =
    TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) x (v₁, v₂)

Tactic:
simp [Prod.toFun', Prod.invFun', h₁, h₂]

Premises used: Bundle.Trivialization.Prod.toFun', Bundle.Trivialization.Prod.invFun'
-- 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 × F₁ × F₂
h : x ∈ SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ
obtain :
  ∀ (x : B) (w₁ : F₁) (w₂ : F₂) (h : (x, w₁, w₂) ∈ SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ),
    toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
⊢ toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ x) = x

Tactic:
obtain ⟨x, w₁, w₂⟩ := x
-- 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₂
h : (x, w₁, w₂) ∈ SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ
⊢ x ∈ e₁.baseSet

Tactic:
obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h

Premises used: Bundle.Trivialization.baseSet
-- 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₂
h : (x, w₁, w₂) ∈ SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ
h₁ : x ∈ e₁.baseSet
⊢ x ∈ e₂.baseSet

Tactic:
obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h

Premises used: Bundle.Trivialization.baseSet
-- 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₂
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)

Tactic:
simp [Prod.toFun', Prod.invFun', h₁, h₂]

Premises used: Bundle.Trivialization.Prod.toFun', Bundle.Trivialization.Prod.invFun'
-- 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)
rw :
  ContinuousOn (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)) ∘
      invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
⊢ ContinuousOn (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂) (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)

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

Premises used: FiberBundle.Prod.isInducing_diag, Topology.IsInducing.continuousOn_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₂)
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)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)

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₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)

Tactic:
have H₁ : Continuous fun p : B × F₁ × F₂ ↦ ((p.1, p.2.1), (p.1, p.2.2)) := 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₂))
inst_5 : (x : B) → Zero (E₁ x)
inst_6 : (x : B) → Zero (E₂ x)
H₁ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)
⊢ ContinuousOn (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)) ∘
      invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)

Tactic:
(e₁.continuousOn_symm.prodMap e₂.continuousOn_symm).comp H₁.continuousOn ?_

Premises used: Bundle.Trivialization.symm, Continuous.continuousOn, Set.Mem, ContinuousOn.prodMap, Bundle.Trivialization.continuousOn_symm, Prod.map, dite, ContinuousOn.comp, Bundle.Pretrivialization.symm
-- 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)
H₁ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)
refine :
  MapsTo (fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2))
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
    (SProd.sprod (β := Set F₁) e₁.baseSet univ ×ˢ SProd.sprod (β := Set F₂) e₂.baseSet univ)
⊢ ContinuousOn (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)) ∘
      invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂)
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)

Tactic:
refine (e₁.continuousOn_symm.prodMap e₂.continuousOn_symm).comp H₁.continuousOn ?_

Premises used: Continuous.continuousOn, ContinuousOn.prodMap, Bundle.Trivialization.continuousOn_symm, ContinuousOn.comp
-- 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)
H₁ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)
⊢ MapsTo (fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2))
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
    (SProd.sprod (β := Set F₁) e₁.baseSet univ ×ˢ SProd.sprod (β := Set F₂) e₂.baseSet univ)

Tactic:
fun x h ↦ ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩

Premises used: Set.Mem, setOf, Set.prod, Prod.mk, Prod.fst, And.right, And.left, Set.MapsTo, And.intro, Set.mem_univ, Prod.snd
-- 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)
H₁ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2)
⊢ MapsTo (fun (p : B × F₁ × F₂) ↦ ((p.1, p.2.1), p.1, p.2.2))
    (SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ)
    (SProd.sprod (β := Set F₁) e₁.baseSet univ ×ˢ SProd.sprod (β := Set F₂) e₂.baseSet univ)

Tactic:
exact fun x h ↦ ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩
-- 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)
⊢ IsOpen[Prod.topologicalSpace F₁ E₁ 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)) ⁻¹'
      e₁.source ×ˢ e₂.source)

Tactic:
(e₁.open_source.prod e₂.open_source).preimage
        (FiberBundle.Prod.isInducing_diag F₁ E₁ F₂ E₂).continuous

Premises used: OpenPartialHomeomorph.open_source, FiberBundle.Prod.isInducing_diag, Topology.IsInducing.continuous, IsOpen.preimage, Bundle.Trivialization.toOpenPartialHomeomorph, IsOpen.prod
-- 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)
h :
  Eq (α := 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))
    ((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)
⊢ IsOpen[Prod.topologicalSpace F₁ E₁ F₂ E₂]
    (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet))

Tactic:
convert!
      (e₁.open_source.prod e₂.open_source).preimage
        (FiberBundle.Prod.isInducing_diag F₁ E₁ F₂ E₂).continuous

Premises used: OpenPartialHomeomorph.open_source, FiberBundle.Prod.isInducing_diag, Topology.IsInducing.continuous, IsOpen.preimage, Bundle.Trivialization.toOpenPartialHomeomorph, IsOpen.prod
-- 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)
h :
  ∀ (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
⊢ Eq (α := 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))
    ((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)

Tactic:
ext x