awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₁
⊢ 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₂)
have h : x ∈ e₁.baseSet
Tactic: rw [Trivialization.continuousLinearMapAt_symmL, Trivialization.continuousLinearMapAt_symmL]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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
⊢ 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₂)
have h₃ : x ∈ e₂.baseSet
Tactic: rw [Trivialization.continuousLinearMapAt_symmL, Trivialization.continuousLinearMapAt_symmL]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₁
⊢ 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₂)
have h : b ∈ e₁'.baseSet ∩ e₁.baseSet
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]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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
⊢ 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₂)
have h₁ : b ∈ e₂.baseSet ∩ e₂'.baseSet
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]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (hypothesis)
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 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
⊢ IsInducing (X := ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) (Y := B × (F₁ →SL[σ] F₂))
    (Function.comp (β :=
      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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
        (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
      (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
        b))
have this : IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
  (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
Tactic: have : IsInducing fun x ↦ (b, φ x) := isInducing_const_prod.mpr φ.toHomeomorph.isInducing
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
⊢ IsInducing (X := ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) (Y := B × (F₁ →SL[σ] F₂))
    (Function.comp (β :=
      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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
        (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
      (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
        b))
have h : ∀ (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)),
  Eq (α := F₁ →SL[σ] F₂)
    (Function.comp (β :=
        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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
          (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
        (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
          b)
        x).2
    ((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)
⊢ Eq (α := F₁ →SL[σ] F₂)
    (Function.comp (β :=
        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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
          (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
        (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
          b)
        x).2
    ((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
have h : ∀ (f : F₁),
  Eq.{u_6 + 1} (α := F₂)
    (((Function.comp (β :=
              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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
                (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
              (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) b)
              x).2 :
          (a : F₁) → F₂)
        f :
      F₂)
    ((((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x : F₁ →SL[σ] F₂) : (a : F₁) → F₂) f : F₂)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)
f : F₁
⊢ Eq.{u_6 + 1} (α := F₂)
    (((Function.comp (β :=
              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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
                (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
              (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) b)
              x).2 :
          (a : F₁) → F₂)
        f :
      F₂)
    ((((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x : F₁ →SL[σ] F₂) : (a : F₁) → F₂) f : F₂)
have h : Eq.{u_6 + 1} (α := F₂)
  (((Trivialization.linearMapAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b :
          LinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂) :
        (a : E₂ b) → F₂)
      ((x : (a : E₁ b) → E₂ b) (Trivialization.symm (E := E₁) (trivializationAt F₁ E₁ b) b f) : E₂ b) :
    F₂)
  ((((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x : F₁ →SL[σ] F₂) : (a : F₁) → F₂) f : F₂)
Tactic: dsimp [Pretrivialization.continuousLinearMap_apply]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s
    m₀
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) s m₀
hb₂ : ContinuousWithinAt b₂ s m₀
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m))) s m₀
have rw : ∀
  (hϕ :
    ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
      (insert m₀ s) m₀)
  (hv :
    ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) (insert m₀ s) m₀)
  (hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀),
  ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m))) (insert m₀ s) m₀
Tactic: rw [← continuousWithinAt_insert_self] at hϕ hv hb₂ ⊢
Cleared hypotheses: hϕ, hv, hb₂