awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
F₃ : Type u_5
M : Type u_6
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_9
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_1, u_9} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
EB : Type u_10
inst_19 : NormedAddCommGroup EB
inst_20 : NormedSpace 𝕜 EB
HB : Type u_11
inst_21 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_22 : TopologicalSpace B
inst_23 : ChartedSpace HB B
EM : Type u_12
inst_24 : NormedAddCommGroup EM
inst_25 : NormedSpace 𝕜 EM
HM : Type u_13
inst_26 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_27 : TopologicalSpace M
inst_28 : ChartedSpace HM M
inst_29 : FiberBundle F₁ E₁
inst_30 : VectorBundle 𝕜 F₁ E₁
inst_31 : FiberBundle F₂ E₂
inst_32 : VectorBundle 𝕜 F₂ E₂
inst_33 : FiberBundle F₃ E₃
inst_34 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
x : M
inst_35 : ∀ (x : B), IsTopologicalAddGroup.{u_9} (E₃ x)
inst_36 : ∀ (x : B), ContinuousSMul.{u_1, u_9} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContMDiffAt IM (E' := EB × (F₁ →L[𝕜] F₂ →L[𝕜] F₃)) (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂ →L[𝕜] F₃)) (M' :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    n (fun (m : M) ↦ ⟨b m, ψ m⟩) x
hv : ContMDiffAt IM (IB.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b m, v m⟩) x
hw : ContMDiffAt IM (IB.prod 𝓘(𝕜, F₂)) (M' := TotalSpace F₂ E₂) n (fun (m : M) ↦ ⟨b m, w m⟩) x
⊢ ContMDiffAt IM (IB.prod 𝓘(𝕜, F₃)) (M' := TotalSpace F₃ E₃) n
    (fun (m : M) ↦
      ⟨b m,
        (((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)⟩)
    x

Tactic:
ContMDiffWithinAt.clm_bundle_apply₂ hψ hv hw

Premises used: ContMDiffWithinAt.clm_bundle_apply₂, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
F₃ : Type u_5
M : Type u_6
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_9
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_1, u_9} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
EB : Type u_10
inst_19 : NormedAddCommGroup EB
inst_20 : NormedSpace 𝕜 EB
HB : Type u_11
inst_21 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_22 : TopologicalSpace B
inst_23 : ChartedSpace HB B
EM : Type u_12
inst_24 : NormedAddCommGroup EM
inst_25 : NormedSpace 𝕜 EM
HM : Type u_13
inst_26 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_27 : TopologicalSpace M
inst_28 : ChartedSpace HM M
inst_29 : FiberBundle F₁ E₁
inst_30 : VectorBundle 𝕜 F₁ E₁
inst_31 : FiberBundle F₂ E₂
inst_32 : VectorBundle 𝕜 F₂ E₂
inst_33 : FiberBundle F₃ E₃
inst_34 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
inst_35 : ∀ (x : B), IsTopologicalAddGroup.{u_9} (E₃ x)
inst_36 : ∀ (x : B), ContinuousSMul.{u_1, u_9} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContMDiffOn IM (E' := EB × (F₁ →L[𝕜] F₂ →L[𝕜] F₃)) (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂ →L[𝕜] F₃)) (M' :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    n (fun (m : M) ↦ ⟨b m, ψ m⟩) s
hv : ContMDiffOn IM (IB.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n (fun (m : M) ↦ ⟨b m, v m⟩) s
hw : ContMDiffOn IM (IB.prod 𝓘(𝕜, F₂)) (M' := TotalSpace F₂ E₂) n (fun (m : M) ↦ ⟨b m, w m⟩) s
⊢ ContMDiffOn IM (IB.prod 𝓘(𝕜, F₃)) (M' := TotalSpace F₃ E₃) n
    (fun (m : M) ↦
      ⟨b m,
        (((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)⟩)
    s

Tactic:
fun x hx ↦ (hψ x hx).clm_bundle_apply₂ (hv x hx) (hw x hx)

Premises used: ContMDiffWithinAt.clm_bundle_apply₂, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
F₃ : Type u_5
M : Type u_6
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_9
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_1, u_9} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
EB : Type u_10
inst_19 : NormedAddCommGroup EB
inst_20 : NormedSpace 𝕜 EB
HB : Type u_11
inst_21 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_22 : TopologicalSpace B
inst_23 : ChartedSpace HB B
EM : Type u_12
inst_24 : NormedAddCommGroup EM
inst_25 : NormedSpace 𝕜 EM
HM : Type u_13
inst_26 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_27 : TopologicalSpace M
inst_28 : ChartedSpace HM M
inst_29 : FiberBundle F₁ E₁
inst_30 : VectorBundle 𝕜 F₁ E₁
inst_31 : FiberBundle F₂ E₂
inst_32 : VectorBundle 𝕜 F₂ E₂
inst_33 : FiberBundle F₃ E₃
inst_34 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst_35 : ∀ (x : B), IsTopologicalAddGroup.{u_9} (E₃ x)
inst_36 : ∀ (x : B), ContinuousSMul.{u_1, u_9} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContMDiff IM (E' := EB × (F₁ →L[𝕜] F₂ →L[𝕜] F₃)) (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂ →L[𝕜] F₃)) (M' :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    n fun (m : M) ↦ ⟨b m, ψ m⟩
hv : ContMDiff IM (IB.prod 𝓘(𝕜, F₁)) (M' := TotalSpace F₁ E₁) n fun (m : M) ↦ ⟨b m, v m⟩
hw : ContMDiff IM (IB.prod 𝓘(𝕜, F₂)) (M' := TotalSpace F₂ E₂) n fun (m : M) ↦ ⟨b m, w m⟩
⊢ ContMDiff IM (IB.prod 𝓘(𝕜, F₃)) (M' := TotalSpace F₃ E₃) n fun (m : M) ↦
    ⟨b m,
      (((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
            ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
          (a : E₂ (b m)) → E₃ (b m))
        (w m)⟩

Tactic:
fun x ↦ (hψ x).clm_bundle_apply₂ (hv x) (hw x)

Premises used: ContMDiff, ContMDiffAt.clm_bundle_apply₂
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
F₃ : Type u_5
M : Type u_6
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_9
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_1, u_9} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
EB : Type u_10
inst_19 : NormedAddCommGroup EB
inst_20 : NormedSpace 𝕜 EB
HB : Type u_11
inst_21 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_22 : TopologicalSpace B
inst_23 : ChartedSpace HB B
EM : Type u_12
inst_24 : NormedAddCommGroup EM
inst_25 : NormedSpace 𝕜 EM
HM : Type u_13
inst_26 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_27 : TopologicalSpace M
inst_28 : ChartedSpace HM M
inst_29 : FiberBundle F₁ E₁
inst_30 : VectorBundle 𝕜 F₁ E₁
inst_31 : FiberBundle F₂ E₂
inst_32 : VectorBundle 𝕜 F₂ E₂
inst_33 : FiberBundle F₃ E₃
inst_34 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_35 : ∀ (x : B), IsTopologicalAddGroup.{u_9} (E₃ x)
inst_36 : ∀ (x : B), ContinuousSMul.{u_1, u_9} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ : MDiffAt[s] (T% ψ) x
hv : MDiffAt[s] (T% v) x
hw : MDiffAt[s] (T% w) x
⊢ (MDiffAt[s] fun (m : M) ↦
      ⟨b m,
        (((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)⟩)
    x

Tactic:
hψ.clm_bundle_apply hv |>.clm_bundle_apply hw

Premises used: MDifferentiableWithinAt.clm_bundle_apply
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
F₃ : Type u_5
M : Type u_6
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_9
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_1, u_9} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
EB : Type u_10
inst_19 : NormedAddCommGroup EB
inst_20 : NormedSpace 𝕜 EB
HB : Type u_11
inst_21 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_22 : TopologicalSpace B
inst_23 : ChartedSpace HB B
EM : Type u_12
inst_24 : NormedAddCommGroup EM
inst_25 : NormedSpace 𝕜 EM
HM : Type u_13
inst_26 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_27 : TopologicalSpace M
inst_28 : ChartedSpace HM M
inst_29 : FiberBundle F₁ E₁
inst_30 : VectorBundle 𝕜 F₁ E₁
inst_31 : FiberBundle F₂ E₂
inst_32 : VectorBundle 𝕜 F₂ E₂
inst_33 : FiberBundle F₃ E₃
inst_34 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
x : M
inst_35 : ∀ (x : B), IsTopologicalAddGroup.{u_9} (E₃ x)
inst_36 : ∀ (x : B), ContinuousSMul.{u_1, u_9} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ : MDiffAt (T% ψ) x
hv : MDiffAt (T% v) x
hw : MDiffAt (T% w) x
⊢ (MDiffAt fun (m : M) ↦
      ⟨b m,
        (((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)⟩)
    x

Tactic:
MDifferentiableWithinAt.clm_bundle_apply₂ hψ hv hw

Premises used: MDifferentiableWithinAt.clm_bundle_apply₂, MDifferentiableAt, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
F₃ : Type u_5
M : Type u_6
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_9
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_1, u_9} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
EB : Type u_10
inst_19 : NormedAddCommGroup EB
inst_20 : NormedSpace 𝕜 EB
HB : Type u_11
inst_21 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_22 : TopologicalSpace B
inst_23 : ChartedSpace HB B
EM : Type u_12
inst_24 : NormedAddCommGroup EM
inst_25 : NormedSpace 𝕜 EM
HM : Type u_13
inst_26 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_27 : TopologicalSpace M
inst_28 : ChartedSpace HM M
inst_29 : FiberBundle F₁ E₁
inst_30 : VectorBundle 𝕜 F₁ E₁
inst_31 : FiberBundle F₂ E₂
inst_32 : VectorBundle 𝕜 F₂ E₂
inst_33 : FiberBundle F₃ E₃
inst_34 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
inst_35 : ∀ (x : B), IsTopologicalAddGroup.{u_9} (E₃ x)
inst_36 : ∀ (x : B), ContinuousSMul.{u_1, u_9} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ : MDiff[s] (T% ψ)
hv : MDiff[s] (T% v)
hw : MDiff[s] (T% w)
⊢ MDiff[s] fun (m : M) ↦
    ⟨b m,
      (((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
            ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
          (a : E₂ (b m)) → E₃ (b m))
        (w m)⟩

Tactic:
fun x hx ↦ (hψ x hx).clm_bundle_apply₂ (hv x hx) (hw x hx)

Premises used: MDifferentiableWithinAt.clm_bundle_apply₂, MDifferentiableOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
F₃ : Type u_5
M : Type u_6
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_7
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_9
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_1, u_9} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
EB : Type u_10
inst_19 : NormedAddCommGroup EB
inst_20 : NormedSpace 𝕜 EB
HB : Type u_11
inst_21 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_22 : TopologicalSpace B
inst_23 : ChartedSpace HB B
EM : Type u_12
inst_24 : NormedAddCommGroup EM
inst_25 : NormedSpace 𝕜 EM
HM : Type u_13
inst_26 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_27 : TopologicalSpace M
inst_28 : ChartedSpace HM M
inst_29 : FiberBundle F₁ E₁
inst_30 : VectorBundle 𝕜 F₁ E₁
inst_31 : FiberBundle F₂ E₂
inst_32 : VectorBundle 𝕜 F₂ E₂
inst_33 : FiberBundle F₃ E₃
inst_34 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst_35 : ∀ (x : B), IsTopologicalAddGroup.{u_9} (E₃ x)
inst_36 : ∀ (x : B), ContinuousSMul.{u_1, u_9} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ : MDiff (T% ψ)
hv : MDiff (T% v)
hw : MDiff (T% w)
⊢ MDiff fun (m : M) ↦
    ⟨b m,
      (((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
            ContinuousLinearMap.{u_1, u_1, u_8, u_9} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
          (a : E₂ (b m)) → E₃ (b m))
        (w m)⟩

Tactic:
fun x ↦ (hψ x).clm_bundle_apply₂ (hv x) (hw x)

Premises used: MDifferentiableAt.clm_bundle_apply₂, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
x : M
hx : x ∈ u
⊢ LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ s x_1 x

Tactic:
have := hs.linearIndependent hx
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
x : M
hx : x ∈ u
this : LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ s x_1 x
⊢ LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ s' x_1 x

Tactic:
simp_all
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
x : M
hx : x ∈ u
⊢ LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ s x_1 x))

Tactic:
have := hs.generating hx
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
x : M
hx : x ∈ u
this : LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ s x_1 x))
⊢ LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ s' x_1 x))

Tactic:
simp_all
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
i : ι
⊢ ∀ y ∈ u, ⟨y, s' i y⟩ = ⟨y, s i y⟩

Tactic:
simp +contextual [hs']
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hu'u : u' ⊆ u
x : M
hx : x ∈ u'
⊢ LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ s x_1 x

Tactic:
hs.linearIndependent (hu'u hx)

Premises used: IsLocalFrameOn.linearIndependent
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hu'u : u' ⊆ u
x : M
hx : x ∈ u'
⊢ LinearIndependent.{u_7, u_1, u_6} 𝕜 (M := V x) fun (x_1 : ι) ↦ s x_1 x

Tactic:
exact hs.linearIndependent (hu'u hx)

Premises used: IsLocalFrameOn.linearIndependent
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F (V := V) n s u
hu'u : u' ⊆ u
x : M
hx : x ∈ u'
⊢ LE.le.{u_6} (α := Submodule 𝕜 (V x)) ⊤ (Submodule.span 𝕜 (Set.range fun (x_1 : ι) ↦ s x_1 x))

Tactic:
hs.generating (hu'u hx)

Premises used: IsLocalFrameOn.generating