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 : 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
-- 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:
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₂'
inst_21 : ∀ (x : B), ContinuousAdd.{u_7} (E₂ x)
inst_22 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
x : B
h :
  x ∈
    baseSet (F := F₁ →SL[σ] F₂) (Z :=
      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂)
L L' : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
⊢ ((↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
          (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
        (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x (L + L'))).2 =
    HAdd.hAdd (α := F₁ →SL[σ] F₂)
      ((↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
            (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
          (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)).2
      ((↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
            (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
          (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L')).2

Tactic:
simp [continuousLinearMap, Pretrivialization.toFun']

Premises used: Bundle.Pretrivialization.continuousLinearMap, Bundle.Pretrivialization.toFun'
-- 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₂'
inst_21 : ∀ (x : B), ContinuousAdd.{u_7} (E₂ x)
inst_22 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
x : B
h :
  x ∈
    baseSet (F := F₁ →SL[σ] F₂) (Z :=
      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂)
c : 𝕜₂
L : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
⊢ ((↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
          (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
        (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x (c • L))).2 =
    HSMul.hSMul (β := F₁ →SL[σ] F₂) c
      ((↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
            (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
          (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)).2

Tactic:
simp [continuousLinearMap, Pretrivialization.toFun']

Premises used: Bundle.Pretrivialization.continuousLinearMap, Bundle.Pretrivialization.toFun'
-- 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₁ : 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_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₂
p : TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
⊢ (↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
        (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
      p =
    (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)),
      comp (σ₁₂ := σ) (M₂ := E₂ (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
        (Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂
          (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
        (p.snd (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)).comp (σ₁₂ := RingHom.id 𝕜₁)
          (Trivialization.symmL 𝕜₁ (E := E₁) e₁
            (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))))

Tactic:
rfl

Premises used: Bundle.Pretrivialization.toFun', rfl
-- 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₁ : 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_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₂
p : B × (F₁ →SL[σ] F₂)
⊢ Eq (α := TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
    ((↑(PartialEquiv.symm (toPartialEquiv (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
        B × (F₁ →SL[σ] F₂) → TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x)
      p)
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) p.1
      (comp.{u_1, u_2, u_2, u_5, u_6, u_7} (R₂ := 𝕜₂) (σ₁₂ := σ) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₂)
        (Trivialization.symmL 𝕜₂ (E := E₂) e₂ p.1)
        (p.2.comp (σ₁₂ := RingHom.id 𝕜₁) (Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ p.1))))

Tactic:
rfl

Premises used: rfl
-- 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₁ : 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_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₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ Eq (α := ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b))
    (cast (α :=
        ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ
          (E₁
            (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
              ((↑(PartialEquiv.symm (toPartialEquiv (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
                  B × (F₁ →SL[σ] F₂) → TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x)
                (b, L))))
          (E₂
            (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
              ((↑(PartialEquiv.symm (toPartialEquiv (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
                  B × (F₁ →SL[σ] F₂) → TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x)
                (b, L)))))
        ⋯
        (TotalSpace.snd (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
          ((↑(PartialEquiv.symm (toPartialEquiv (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
              B × (F₁ →SL[σ] F₂) → TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x)
            (b, L))) :
      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b))
    (comp.{u_1, u_2, u_2, u_5, u_6, u_7} (R₂ := 𝕜₂) (σ₁₂ := σ) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₂)
        (Trivialization.symmL 𝕜₂ (E := E₂) e₂ b)
        (L.comp (σ₁₂ := RingHom.id 𝕜₁) (Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ b)) :
      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b))

Tactic:
rfl
-- 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₁ : 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_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₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ b ∈
    baseSet (F := F₁ →SL[σ] F₂) (Z :=
      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂)

Tactic:
hb

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₁ : 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_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₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ b ∈
    baseSet (F := F₁ →SL[σ] F₂) (Z :=
      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂)

Tactic:
exact hb
-- 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₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
h : b ∈ e₁'.baseSet ∩ e₁.baseSet
h₁ : b ∈ e₂.baseSet ∩ e₂'.baseSet
⊢ Eq (α := F₂)
    ((Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b : (a : F₂) → F₂)
        ((L : (a : F₁) → F₂) ((Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b : (a : F₁) → F₁) v : F₁) : F₂) :
      F₂)
    (((Trivialization.linearMapAt 𝕜₂ (E := E₂) e₂' b : LinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂) :
          (a : E₂ b) → F₂)
        (e₂.symm (E := E₂) b
          ((L : (a : F₁) → F₂)
            (((Trivialization.linearMapAt 𝕜₁ (E := E₁) e₁ b :
                    LinearMap.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁) :
                  (a : E₁ b) → F₁)
                (e₁'.symm (E := E₁) b v) :
              F₁))) :
      F₂)

Tactic:
rw [e₂.coordChangeL_apply e₂', e₁'.coordChangeL_apply e₁, e₁.coe_linearMapAt_of_mem hb.1.1,
    e₂'.coe_linearMapAt_of_mem hb.2.2]

Premises used: Bundle.Trivialization.coordChangeL_apply, Bundle.Trivialization.coe_linearMapAt_of_mem, And.right, And.left
-- 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₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ b ∈ e₁'.baseSet ∩ e₁.baseSet

Tactic:
⟨hb.2.1, hb.1.1⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro
-- 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₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ b ∈ e₂.baseSet ∩ e₂'.baseSet

Tactic:
⟨hb.1.2, hb.2.2⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro
-- 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₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ b ∈ e₁'.baseSet ∩ e₁.baseSet

Tactic:
exacts [⟨hb.2.1, hb.1.1⟩, ⟨hb.1.2, hb.2.2⟩]