awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
B : Type u_3
inst_1 : TopologicalSpace B
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_1, u_7} 𝕜 (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₁ x)
inst_13 : FiberBundle F₁ E₁
inst_14 : (x : B) → TopologicalSpace (E₂ x)
inst_15 : FiberBundle F₂ E₂
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_16 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
have mfld_set_tac₃ : ∀ ⦃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
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
B : Type u_3
inst_1 : TopologicalSpace B
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_1, u_7} 𝕜 (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₁ x)
inst_13 : FiberBundle F₁ E₁
inst_14 : (x : B) → TopologicalSpace (E₂ x)
inst_15 : FiberBundle F₂ E₂
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_16 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_17 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_18 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_19 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
x : B
L : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
h₁ :
  TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L) ∈
    e₁.baseSet
h₂ :
  TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L) ∈
    e₂.baseSet
⊢ ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
      (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
      (ContinuousAlternatingMap.compContinuousLinearMap.{u_1, u_4, u_5, u_6, u_2} (M := F₁)
        (ContinuousLinearMap.compContinuousAlternatingMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
          (L.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) e₁ x)))
        (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)) =
    L
have H : ∀ (v : ι → E₁ x),
  Eq.{u_7 + 1} (α := E₂ x)
    (((ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
              (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
              (ContinuousAlternatingMap.compContinuousLinearMap.{u_1, u_4, u_5, u_6, u_2} (M := F₁)
                (ContinuousLinearMap.compContinuousAlternatingMap
                  (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
                  (L.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) e₁ x)))
                (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)) :
            ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) :
          (a : ι → E₁ x) → E₂ x)
        v :
      E₂ x)
    ((L : (a : ι → E₁ x) → E₂ x) v : E₂ x)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
B : Type u_3
inst_1 : TopologicalSpace B
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_1, u_7} 𝕜 (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₁ x)
inst_13 : FiberBundle F₁ E₁
inst_14 : (x : B) → TopologicalSpace (E₂ x)
inst_15 : FiberBundle F₂ E₂
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_16 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_17 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_18 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_19 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
x : B
f : F₁ [⋀^ι]→L[𝕜] F₂
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
⊢ ContinuousLinearMap.compContinuousAlternatingMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
      (ContinuousAlternatingMap.compContinuousLinearMap
        (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
          (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
          (f.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)))
        (Trivialization.symmL 𝕜 (E := E₁) e₁ x)) =
    f
have H : ∀ (v : ι → F₁),
  Eq.{u_6 + 1} (α := F₂)
    ((ContinuousLinearMap.compContinuousAlternatingMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
            (ContinuousAlternatingMap.compContinuousLinearMap
              (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
                (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
                (f.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)))
              (Trivialization.symmL 𝕜 (E := E₁) e₁ x)) :
          (a : ι → F₁) → F₂)
        v :
      F₂)
    ((f : (a : ι → F₁) → F₂) v : F₂)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
B : Type u_3
inst_1 : TopologicalSpace B
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_1, u_7} 𝕜 (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₁ x)
inst_13 : FiberBundle F₁ E₁
inst_14 : (x : B) → TopologicalSpace (E₂ x)
inst_15 : FiberBundle F₂ E₂
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_16 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_17 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_18 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_19 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
inst_20 : ∀ (x : B), ContinuousAdd.{u_7} (E₂ x)
inst_21 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x : B
h :
  x ∈
    baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂)
c : 𝕜
L : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
⊢ ((↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
          (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
        (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
          (c • L))).2 =
    HSMul.hSMul (β := F₁ [⋀^ι]→L[𝕜] F₂) c
      ((↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
            (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
          (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L)).2
have H : ∀ (x_1 : ι → F₁),
  Eq.{u_6 + 1} (α := F₂)
    ((((↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
                (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
              (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                (c • L))).2 :
          (a : ι → F₁) → F₂)
        x_1 :
      F₂)
    ((HSMul.hSMul (β := F₁ [⋀^ι]→L[𝕜] F₂) c
            ((↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
                  (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                  L)).2 :
          (a : ι → F₁) → F₂)
        x_1 :
      F₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
B : Type u_3
inst_1 : TopologicalSpace B
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_1, u_7} 𝕜 (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₁ x)
inst_13 : FiberBundle F₁ E₁
inst_14 : (x : B) → TopologicalSpace (E₂ x)
inst_15 : FiberBundle F₂ E₂
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_16 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_17 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_18 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_19 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ [⋀^ι]→L[𝕜] F₂
v : ι → F₁
⊢ Eq.{u_6 + 1} (α := F₂)
    ((((continuousAlternatingMapCoordChange 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂' b :
                (a : F₁ [⋀^ι]→L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂)
              L :
            F₁ [⋀^ι]→L[𝕜] F₂) :
          (a : ι → F₁) → F₂)
        v :
      F₂)
    ((((↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁' e₂') :
                (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
              (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) b
                (Pretrivialization.symm (E := fun (x : B) ↦
                  ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                  (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂ :
                    Pretrivialization (B := B) (F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
                      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.proj (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
                  b L))).2 :
          (a : ι → F₁) → F₂)
        v :
      F₂)
have hb₁ : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet
Tactic: simp only [mem_inter_iff] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace 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_1, u_7} 𝕜 (E₂ x)
b : B
⊢ IsInducing (X := ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι) (Y := B × F₁ [⋀^ι]→L[𝕜] F₂)
    (Function.comp (β :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
        (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
      (TotalSpace.mk (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) b))
have simp : IsInducing (Y := F₁ [⋀^ι]→L[𝕜] F₂) fun (x' : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι) ↦
  ContinuousLinearMap.compContinuousAlternatingMap
    (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ b) b)
    (x'.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) (trivializationAt F₁ E₁ b) b))
Tactic: simp only [Function.comp_def, continuousAlternatingMap_apply, isInducing_const_prod]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace 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_1, u_7} 𝕜 (E₂ x)
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_1, u_1, u_7, u_6} (RingHom.id 𝕜) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
⊢ IsInducing (Y := F₁ [⋀^ι]→L[𝕜] F₂) fun (x' : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι) ↦
    ContinuousLinearMap.compContinuousAlternatingMap
      (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ b) b)
      (x'.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) (trivializationAt F₁ E₁ b) b))
have h : ∀ (x : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι),
  Eq (α := F₁ [⋀^ι]→L[𝕜] F₂)
    (ContinuousLinearMap.compContinuousAlternatingMap
      (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ b) b)
      (x.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) (trivializationAt F₁ E₁ b) b)))
    ((ContinuousLinearEquiv.toHomeomorph (L₁.continuousAlternatingMapCongr L₂) :
        (a : E₁ b [⋀^ι]→L[𝕜] E₂ b) → F₁ [⋀^ι]→L[𝕜] F₂)
      x)
Tactic: convert! (L₁.continuousAlternatingMapCongr L₂).toHomeomorph.isInducing
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace 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_1, u_7} 𝕜 (E₂ x)
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_1, u_1, u_7, u_6} (RingHom.id 𝕜) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
x : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι
⊢ Eq (α := F₁ [⋀^ι]→L[𝕜] F₂)
    (ContinuousLinearMap.compContinuousAlternatingMap
      (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ b) b)
      (x.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) (trivializationAt F₁ E₁ b) b)))
    ((ContinuousLinearEquiv.toHomeomorph (L₁.continuousAlternatingMapCongr L₂) :
        (a : E₁ b [⋀^ι]→L[𝕜] E₂ b) → F₁ [⋀^ι]→L[𝕜] F₂)
      x)
have h : ∀ (f : ι → F₁),
  Eq.{u_6 + 1} (α := F₂)
    ((ContinuousLinearMap.compContinuousAlternatingMap
            (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ b) b)
            (x.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) (trivializationAt F₁ E₁ b) b)) :
          (a : ι → F₁) → F₂)
        f :
      F₂)
    ((((ContinuousLinearEquiv.toHomeomorph (L₁.continuousAlternatingMapCongr L₂) :
                (a : E₁ b [⋀^ι]→L[𝕜] E₂ b) → F₁ [⋀^ι]→L[𝕜] F₂)
              x :
            F₁ [⋀^ι]→L[𝕜] F₂) :
          (a : ι → F₁) → F₂)
        f :
      F₂)
Tactic: ext f
-- 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 : (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₂'
⊢ 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))
have 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₂)
Tactic: have h₁ := (compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)).continuous
-- 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 : (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₂)
⊢ 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))
have 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₂)
Tactic: have h₂ := (ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)).continuous