awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₂ :
  Continuous (X := F₁ →L[𝕜₁] F₁) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
      (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₃ :
  ContinuousOn.{u_3, u_4} (Y := F₁ →L[𝕜₁] F₁)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₄ :
  ContinuousOn.{u_3, u_6} (Y := F₂ →L[𝕜₂] F₂)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b) : F₂ →L[𝕜₂] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ ContinuousOn (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (continuousLinearMapCoordChange σ (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
((h₁.comp_continuousOn (h₄.mono ?_)).clm_comp (h₂.comp_continuousOn (h₃.mono ?_))).congr ?_

Premises used: Continuous.comp_continuousOn, ContinuousOn.clm_comp, ContinuousOn.congr, ContinuousOn.mono
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₂ :
  Continuous (X := F₁ →L[𝕜₁] F₁) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
      (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₃ :
  ContinuousOn.{u_3, u_4} (Y := F₁ →L[𝕜₁] F₁)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₄ :
  ContinuousOn.{u_3, u_6} (Y := F₂ →L[𝕜₂] F₂)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b) : F₂ →L[𝕜₂] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
refine_1 refine_1₁ refine_1₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
refine_1₃ refine_1₄ :
  ∀ ⦃my_y : B⦄,
    (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet

Tactic:
mfld_set_tac
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₂ :
  Continuous (X := F₁ →L[𝕜₁] F₁) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
      (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₃ :
  ContinuousOn.{u_3, u_4} (Y := F₁ →L[𝕜₁] F₁)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₄ :
  ContinuousOn.{u_3, u_6} (Y := F₂ →L[𝕜₂] F₂)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b) : F₂ →L[𝕜₂] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
refine_2 refine_2₁ refine_2₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
refine_2₃ refine_2₄ :
  ∀ ⦃my_y : B⦄,
    (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet

Tactic:
mfld_set_tac
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
x_1 : TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
x : B
L : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
h :
  Membership.mem (γ :=
    Set (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
    (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) ⁻¹'
      (e₁.baseSet ∩ e₂.baseSet))
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)
h₁ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₁.baseSet
h₂ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₂.baseSet
v : E₁ x
⊢ x ∈ e₁.baseSet

Tactic:
h₁

Premises used: Set.Mem
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
x_1 : TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
x : B
L : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
h :
  Membership.mem (γ :=
    Set (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
    (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) ⁻¹'
      (e₁.baseSet ∩ e₂.baseSet))
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)
h₁ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₁.baseSet
h₂ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₂.baseSet
v : E₁ x
⊢ x ∈ e₂.baseSet

Tactic:
h₂

Premises used: Set.Mem
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
x_1 : TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
x : B
L : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
h :
  Membership.mem (γ :=
    Set (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
    (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) ⁻¹'
      (e₁.baseSet ∩ e₂.baseSet))
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)
h₁ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₁.baseSet
h₂ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₂.baseSet
v : E₁ x
⊢ x ∈ e₁.baseSet

Tactic:
exacts [h₁, h₂]
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
x_1 : B × (F₁ →SL[σ] F₂)
x : B
f : F₁ →SL[σ] F₂
h_1 : (x, f) ∈ SProd.sprod (β := Set (F₁ →SL[σ] F₂)) (e₁.baseSet ∩ e₂.baseSet) univ
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
right : Membership.mem (γ := Set (F₁ →SL[σ] F₂)) univ (x, f).2
h :
  ∀ (v : F₁),
    Eq.{u_6 + 1} (α := F₂)
      ((Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂ x ∘SL
              comp (σ₂₃ := σ)
                (comp.{u_1, u_2, u_2, u_5, u_6, u_7} (R₂ := 𝕜₂) (σ₁₂ := σ) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₂)
                  (Trivialization.symmL 𝕜₂ (E := E₂) e₂ x)
                  (f.comp (σ₁₂ := RingHom.id 𝕜₁) (Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ x)))
                (Trivialization.symmL 𝕜₁ (E := E₁) e₁ x) :
            (a : F₁) → F₂)
          v :
        F₂)
      ((f : (a : F₁) → F₂) v : F₂)
⊢ Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂ x ∘SL
      comp (σ₂₃ := σ)
        (comp.{u_1, u_2, u_2, u_5, u_6, u_7} (R₂ := 𝕜₂) (σ₁₂ := σ) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₂)
          (Trivialization.symmL 𝕜₂ (E := E₂) e₂ x)
          (f.comp (σ₁₂ := RingHom.id 𝕜₁) (Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ x)))
        (Trivialization.symmL 𝕜₁ (E := E₁) e₁ x) =
    f

Tactic:
ext v
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
x_1 : B × (F₁ →SL[σ] F₂)
x : B
f : F₁ →SL[σ] F₂
h_1 : (x, f) ∈ SProd.sprod (β := Set (F₁ →SL[σ] F₂)) (e₁.baseSet ∩ e₂.baseSet) univ
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
right : Membership.mem (γ := Set (F₁ →SL[σ] F₂)) univ (x, f).2
v : F₁
h :
  Eq.{u_6 + 1} (α := F₂)
    (((Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂ x :
            ContinuousLinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ x) F₂) :
          (a : E₂ x) → F₂)
        (((Trivialization.symmL 𝕜₂ (E := E₂) e₂ x :
                ContinuousLinearMap.{u_2, u_2, u_6, u_7} (RingHom.id 𝕜₂) F₂ (E₂ x)) :
              (a : F₂) → E₂ x)
            ((f : (a : F₁) → F₂)
              (((Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ x :
                      ContinuousLinearMap.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ x) F₁) :
                    (a : E₁ x) → F₁)
                  (((Trivialization.symmL 𝕜₁ (E := E₁) e₁ x :
                          ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜₁) F₁ (E₁ x)) :
                        (a : F₁) → E₁ x)
                      v :
                    E₁ x) :
                F₁)) :
          E₂ x) :
      F₂)
    ((f : (a : F₁) → F₂) v : F₂)
⊢ Eq.{u_6 + 1} (α := F₂)
    ((Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂ x ∘SL
            comp (σ₂₃ := σ)
              (comp.{u_1, u_2, u_2, u_5, u_6, u_7} (R₂ := 𝕜₂) (σ₁₂ := σ) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₂)
                (Trivialization.symmL 𝕜₂ (E := E₂) e₂ x)
                (f.comp (σ₁₂ := RingHom.id 𝕜₁) (Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ x)))
              (Trivialization.symmL 𝕜₁ (E := E₁) e₁ x) :
          (a : F₁) → F₂)
        v :
      F₂)
    ((f : (a : F₁) → F₂) v : F₂)

Tactic:
dsimp only [comp_apply]

Premises used: ContinuousLinearMap.comp_apply
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
x_1 : B × (F₁ →SL[σ] F₂)
x : B
f : F₁ →SL[σ] F₂
h_1 : (x, f) ∈ SProd.sprod (β := Set (F₁ →SL[σ] F₂)) (e₁.baseSet ∩ e₂.baseSet) univ
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
right : Membership.mem (γ := Set (F₁ →SL[σ] F₂)) univ (x, f).2
v : F₁
h : x ∈ e₁.baseSet
h₃ : x ∈ e₂.baseSet
⊢ Eq.{u_6 + 1} (α := F₂)
    (((Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂ x :
            ContinuousLinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ x) F₂) :
          (a : E₂ x) → F₂)
        (((Trivialization.symmL 𝕜₂ (E := E₂) e₂ x :
                ContinuousLinearMap.{u_2, u_2, u_6, u_7} (RingHom.id 𝕜₂) F₂ (E₂ x)) :
              (a : F₂) → E₂ x)
            ((f : (a : F₁) → F₂)
              (((Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ x :
                      ContinuousLinearMap.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ x) F₁) :
                    (a : E₁ x) → F₁)
                  (((Trivialization.symmL 𝕜₁ (E := E₁) e₁ x :
                          ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜₁) F₁ (E₁ x)) :
                        (a : F₁) → E₁ x)
                      v :
                    E₁ x) :
                F₁)) :
          E₂ x) :
      F₂)
    ((f : (a : F₁) → F₂) v : F₂)

Tactic:
rw [Trivialization.continuousLinearMapAt_symmL, Trivialization.continuousLinearMapAt_symmL]

Premises used: Bundle.Trivialization.continuousLinearMapAt_symmL
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
x_1 : B × (F₁ →SL[σ] F₂)
x : B
f : F₁ →SL[σ] F₂
h : (x, f) ∈ SProd.sprod (β := Set (F₁ →SL[σ] F₂)) (e₁.baseSet ∩ e₂.baseSet) univ
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
right : Membership.mem (γ := Set (F₁ →SL[σ] F₂)) univ (x, f).2
v : F₁
⊢ x ∈ e₁.baseSet

Tactic:
h₁

Premises used: Set.Mem