awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
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)
⊢ 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))
have hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
Tactic: have hf₁ : Continuous f₁ := (Prod.isInducing_diag F₁ E₁ F₂ E₂).continuous
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
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 (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))
have hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
Tactic: have hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source) :=
    e₁.toOpenPartialHomeomorph.continuousOn.prodMap e₂.toOpenPartialHomeomorph.continuousOn
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
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)
⊢ 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))
have hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
Tactic: have hf₃ : Continuous f₃ := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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))
have 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)
Tactic: refine ((hf₃.comp_continuousOn hf₂).comp hf₁.continuousOn ?_).congr ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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)
⊢ 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))
have 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))
Tactic: refine ((hf₃.comp_continuousOn hf₂).comp hf₁.continuousOn ?_).congr ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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))
    (e₁.source ×ˢ e₂.source)
have 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))
Tactic: rw [e₁.source_eq, e₂.source_eq]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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
⊢ 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₂))
have refine_2 : b = ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) (TotalSpace.mk (E := E₁) b v₁)).1
Tactic: simp only [f₁, f₂, f₃, Prod.toFun', Prod.mk_inj, Function.comp_apply, and_true]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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
⊢ b = ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) (TotalSpace.mk (E := E₁) b v₁)).1
have refine_2 : TotalSpace.mk (E := E₁) b v₁ ∈ e₁.source
Tactic: rw [e₁.coe_fst]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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.mk (E := E₁) b v₁ ∈ e₁.source
have refine_2 : TotalSpace.proj.{u_1, u_2, u_3} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) b v₁) ∈ e₁.baseSet
Tactic: rw [e₁.source_eq, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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
⊢ invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ x) = x
have 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₂)
Tactic: obtain ⟨x, v₁, v₂⟩ := x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
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₂))
⊢ 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₂)
have h₁ : x ∈ e₁.baseSet
Tactic: obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
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
⊢ 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₂)
have h₂ : x ∈ e₂.baseSet
Tactic: obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
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
⊢ toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ x) = x
have 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₂)
Tactic: obtain ⟨x, w₁, w₂⟩ := x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
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
⊢ toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
have h₁ : x ∈ e₁.baseSet
Tactic: obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
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
⊢ toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
have h₂ : x ∈ e₂.baseSet
Tactic: obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h
Cleared hypotheses: h