awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
⊢ Continuous[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : E b) ↦
    if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
have refine : ∀ (hb : b ∈ e.baseSet),
  Continuous[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : E b) ↦
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
Tactic: refine continuous_if_const _ (fun hb => ?_) fun _ => continuous_zero
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
⊢ Continuous[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : E b) ↦
    if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
have refine : ∀ (hb : b ∈ e.baseSet),
  Continuous[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : E b) ↦
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
Tactic: classical
      refine continuous_if_const _ (fun hb => ?_) fun _ => continuous_zero
      exact (e.continuousOn.comp_continuous (FiberBundle.totalSpaceMk_isInducing F E b).continuous
        fun x => e.mem_source.mpr hb).snd
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7 b] (e.symm (E := E) b)
have pos : ∀ (hb : b ∈ e.baseSet), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7 b] (e.symm (E := E) b)
Tactic: by_cases hb : b ∈ e.baseSet
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
pos :
  ∀ (hb : b ∈ e.baseSet), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7 b] (e.symm (E := E) b)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7 b] (e.symm (E := E) b)
have neg : ∀ (hb : b ∉ e.baseSet), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7 b] (e.symm (E := E) b)
Tactic: by_cases hb : b ∈ e.baseSet
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7 b] (e.symm (E := E) b)
have pos : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (TotalSpace.mk (E := E) b ∘ e.symm (E := E) b)
Tactic: rw [(FiberBundle.totalSpaceMk_isInducing F E b).continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
z : E b
⊢ (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b z) =
    (b, (continuousLinearEquivAt R (E := E) e b hb : (a : E b) → F) z)
have fst : ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b z)).1 =
  ((b, (continuousLinearEquivAt R (E := E) e b hb : (a : E b) → F) z) : B × F).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
z : E b
fst :
  ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b z)).1 =
    ((b, (continuousLinearEquivAt R (E := E) e b hb : (a : E b) → F) z) : B × F).1
⊢ (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b z) =
    (b, (continuousLinearEquivAt R (E := E) e b hb : (a : E b) → F) z)
have snd : ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b z)).2 =
  (b, (continuousLinearEquivAt R (E := E) e b hb : (a : E b) → F) z).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
z : E b
⊢ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b z)).1 =
    ((b, (continuousLinearEquivAt R (E := E) e b hb : (a : E b) → F) z) : B × F).1
have fst : TotalSpace.mk (E := E) b z ∈ e.source
Tactic: refine e.coe_fst ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
z : E b
⊢ TotalSpace.mk (E := E) b z ∈ e.source
have fst : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' e.baseSet) (TotalSpace.mk (E := E) b z)
Tactic: rw [e.source_eq]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
x : B
hx : x ∈ e.baseSet
⊢ (↑e : TotalSpace F E → B × F) (zeroSection F E x) = (x, 0)
have simp_rw : (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x 0) = (x, 0)
Tactic: simp_rw [zeroSection, e.apply_eq_prod_continuousLinearEquivAt R x hx 0, map_zero]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
x : B
hx : x ∈ e.baseSet
simp_rw : (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x 0) = (x, 0)
⊢ (↑e : TotalSpace F E → B × F) (zeroSection F E x) = (x, 0)
have simp_rw₁ : Eq (α := B × F) ((x, (continuousLinearEquivAt R (E := E) e x hx : (a : E x) → F) 0) : B × F) ((x, 0) : B × F)
Tactic: simp_rw [zeroSection, e.apply_eq_prod_continuousLinearEquivAt R x hx 0, map_zero]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
inst_9 : VectorBundle R F E
⊢ Continuous[inst_5, inst_6] (zeroSection F E)
have refine : ∀ (x : B), ContinuousAt (zeroSection F E) x
Tactic: refine continuous_iff_continuousAt.2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
inst_9 : VectorBundle R F E
x : B
⊢ ContinuousAt (Y := TotalSpace F E) (fun (x : B) ↦ TotalSpace.mk (E := E) x 0) x
have rw : ContinuousAt.{u_2, u_3} (Y := F)
  (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2) x
Tactic: rw [FiberBundle.continuousAt_section]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
inst_9 : VectorBundle R F E
x : B
⊢ ContinuousAt.{u_2, u_3} (Y := F)
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2) x
have apply : Filter.EventuallyEq.{u_2, u_3} (β := F) (𝓝 x)
  (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2)
  fun (x : B) ↦ 0
Tactic: apply (continuousAt_const (y := 0)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
inst_9 : VectorBundle R F E
x : B
⊢ Filter.EventuallyEq.{u_2, u_3} (β := F) (𝓝 x)
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2)
    fun (x : B) ↦ 0
have h : ∀ (a : B),
  Membership.mem (γ := Set B)
    {x_1 : B |
      x_1 ∈ baseSet (trivializationAt F E x) →
        Membership.mem (γ := Set B)
          {x_2 : B |
            (fun (x_3 : B) ↦
                Eq.{u_3 + 1} (α := F)
                  ((fun (x_4 : B) ↦
                      ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_4 0)).2)
                    x_3)
                  ((fun (x : B) ↦ (0 : F)) x_3))
              x_2}
          x_1}
    a
Tactic: filter_upwards [(trivializationAt F E x).open_baseSet.mem_nhds
    (mem_baseSet_trivializationAt F E x)] with y hy
    using congr_arg Prod.snd <| (trivializationAt F E x).zeroSection R hy
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
inst_9 : VectorBundle R F E
x : B
h :
  ∀ (a : B),
    Membership.mem (γ := Set B)
      {x_1 : B |
        x_1 ∈ baseSet (trivializationAt F E x) →
          Membership.mem (γ := Set B)
            {x_2 : B |
              (fun (x_3 : B) ↦
                  Eq.{u_3 + 1} (α := F)
                    ((fun (x_4 : B) ↦
                        ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_4 0)).2)
                      x_3)
                    ((fun (x : B) ↦ (0 : F)) x_3))
                x_2}
            x_1}
      a
⊢ Filter.EventuallyEq.{u_2, u_3} (β := F) (𝓝 x)
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2)
    fun (x : B) ↦ 0
have h₁ : ∀ a ∈ baseSet (trivializationAt F E x),
  ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) a 0)).2 = 0
Tactic: filter_upwards [(trivializationAt F E x).open_baseSet.mem_nhds
    (mem_baseSet_trivializationAt F E x)] with y hy
    using congr_arg Prod.snd <| (trivializationAt F E x).zeroSection R hy
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
inst_10 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Eq (α := F ≃L[R] F)
    (ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b ⋯))
      (continuousLinearEquivAt R (E := E) e' b ⋯))
    (coordChangeL R (E := E) e e' b)
have h : ∀ (v : F),
  Eq (α := F)
    ((ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b sorry))
            (continuousLinearEquivAt R (E := E) e' b sorry) :
          (a : F) → F)
        v :
      F)
    ((coordChangeL R (E := E) e e' b : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
inst_10 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ Eq (α := F)
    ((ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b ⋯))
            (continuousLinearEquivAt R (E := E) e' b ⋯) :
          (a : F) → F)
        v :
      F)
    ((coordChangeL R (E := E) e e' b : (a : F) → F) v : F)
have h : (ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b sorry))
        (continuousLinearEquivAt R (E := E) e' b sorry) :
      (a : F) → F)
    v =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2
Tactic: rw [coordChangeL_apply e e' hb]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k
⊢ Z.coordChange j k x ∘SL Z.coordChange i j x = Z.coordChange i k x
have h : ∀ (v : F),
  Eq (α := F) ((Z.coordChange j k x ∘SL Z.coordChange i j x : (a : F) → F) v : F)
    ((Z.coordChange i k x : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet ∧ b ∈ (Z.localTriv j).baseSet
v : F
⊢ Eq (α := F) ((Trivialization.coordChangeL R (E := Z.Fiber) (Z.localTriv i) (Z.localTriv j) b : (a : F) → F) v : F)
    ((Z.coordChange i j b : (a : F) → F) v : F)
have a : TotalSpace.proj (F := F) (E := Z.Fiber)
    (TotalSpace.mk (E := Z.Fiber) (b, v).1 ((Z.coordChange i (Z.indexAt (b, v).1) (b, v).1 : (a : F) → F) (b, v).2)) ∈
  Z.baseSet i ∩
      Z.baseSet
        (Z.indexAt
          (TotalSpace.proj (F := F) (E := Z.Fiber)
            (TotalSpace.mk (E := Z.Fiber) (b, v).1
              ((Z.coordChange i (Z.indexAt (b, v).1) (b, v).1 : (a : F) → F) (b, v).2)))) ∩
    Z.baseSet j
Tactic: rw [Trivialization.coordChangeL_apply', localTriv_symm_fst, localTriv_apply, coordChange_comp]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet ∧ b ∈ (Z.localTriv j).baseSet
v : F
a :
  TotalSpace.proj (F := F) (E := Z.Fiber)
      (TotalSpace.mk (E := Z.Fiber) (b, v).1 ((Z.coordChange i (Z.indexAt (b, v).1) (b, v).1 : (a : F) → F) (b, v).2)) ∈
    Z.baseSet i ∩
        Z.baseSet
          (Z.indexAt
            (TotalSpace.proj (F := F) (E := Z.Fiber)
              (TotalSpace.mk (E := Z.Fiber) (b, v).1
                ((Z.coordChange i (Z.indexAt (b, v).1) (b, v).1 : (a : F) → F) (b, v).2)))) ∩
      Z.baseSet j
⊢ Eq (α := F) ((Trivialization.coordChangeL R (E := Z.Fiber) (Z.localTriv i) (Z.localTriv j) b : (a : F) → F) v : F)
    ((Z.coordChange i j b : (a : F) → F) v : F)
have hb₁ : b ∈ (Z.localTriv i).baseSet ∩ (Z.localTriv j).baseSet
Tactic: rw [Trivialization.coordChangeL_apply', localTriv_symm_fst, localTriv_apply, coordChange_comp]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
⊢ TotalSpace.mk (E := Z.Fiber) b a ∈ (Z.localTrivAt b).source
have rw : TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) b a) ∈ Z.baseSet (Z.indexAt b)
Tactic: rw [localTrivAt, mem_localTriv_source]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
i_1 j i i' : ι
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[R] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
            (Z.toFiberBundleCore.localTriv i') b) :
        F →L[R] F))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)
have refine : ∀ (b : B) (hb : b ∈ Z.baseSet i ∩ Z.baseSet i'),
  (↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
          b) :
      F →L[R] F) =
    Z.coordChange i i' b
Tactic: refine (Z.continuousOn_coordChange i i').congr fun b hb => ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b_1 : B
a : F
i_1 j i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
⊢ (↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
          b) :
      F →L[R] F) =
    Z.coordChange i i' b
have h : ∀ (v : F),
  Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                (Z.toFiberBundleCore.localTriv i') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((Z.coordChange i i' b : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
⊢ Trivialization.continuousLinearMapAt R (E := Z.Fiber) (Z.localTriv i) b = Z.coordChange (Z.indexAt b) i b
have h : ∀ (v : Z.Fiber b),
  Eq (α := F) ((Trivialization.continuousLinearMapAt R (E := Z.Fiber) (Z.localTriv i) b : (a : Z.Fiber b) → F) v : F)
    ((Z.coordChange (Z.indexAt b) i b : (a : Z.Fiber b) → F) v : F)
Tactic: ext1 v