awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Basic
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
rw :
  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
⊢ Continuous[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(Trivialization.linearMapAt R (E := E) e b) : (a : E b) → F)

Tactic:
rw [e.coe_linearMapAt b]

Premises used: Bundle.Trivialization.coe_linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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

Tactic:
continuous_if_const _ (fun hb => ?_) fun _ => continuous_zero

Premises used: continuous_if_const, continuous_zero
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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
⊢ 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

Tactic:
refine continuous_if_const _ (fun hb => ?_) fun _ => continuous_zero

Premises used: continuous_if_const, continuous_zero
-- Module: Mathlib.Topology.VectorBundle.Basic
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[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : E b) ↦
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2

Tactic:
(e.continuousOn.comp_continuous (FiberBundle.totalSpaceMk_isInducing F E b).continuous
        fun x => e.mem_source.mpr hb).snd

Premises used: Iff.mpr, ContinuousOn.comp_continuous, Continuous.snd, Bundle.Trivialization.mem_source, Bundle.Trivialization.continuousOn, FiberBundle.totalSpaceMk_isInducing, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.VectorBundle.Basic
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[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : E b) ↦
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2

Tactic:
exact (e.continuousOn.comp_continuous (FiberBundle.totalSpaceMk_isInducing F E b).continuous
        fun x => e.mem_source.mpr hb).snd

Premises used: Iff.mpr, ContinuousOn.comp_continuous, Continuous.snd, Bundle.Trivialization.mem_source, Bundle.Trivialization.continuousOn, FiberBundle.totalSpaceMk_isInducing, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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
⊢ 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

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

Premises used: continuous_if_const, continuous_zero
-- Module: Mathlib.Topology.VectorBundle.Basic
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
y : E b
⊢ (continuousLinearMapAt R (E := E) e b : (a : E b) → F) y =
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2

Tactic:
simp [coe_linearMapAt_of_mem e hb]

Premises used: Bundle.Trivialization.coe_linearMapAt_of_mem
-- Module: Mathlib.Topology.VectorBundle.Basic
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)
neg :
  ∀ (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)

Tactic:
by_cases hb : b ∈ e.baseSet

Premises used: Bundle.Trivialization.baseSet
-- Module: Mathlib.Topology.VectorBundle.Basic
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
pos :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (TotalSpace.mk (E := E) b ∘ e.symm (E := E) b)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7 b] (e.symm (E := E) b)

Tactic:
rw [(FiberBundle.totalSpaceMk_isInducing F E b).continuous_iff]

Premises used: Topology.IsInducing.continuous_iff, FiberBundle.totalSpaceMk_isInducing
-- Module: Mathlib.Topology.VectorBundle.Basic
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_6] (TotalSpace.mk (E := E) b ∘ e.symm (E := E) b)

Tactic:
e.continuousOn_symm.comp_continuous (.prodMk_right _) fun x ↦
          mk_mem_prod hb (mem_univ x)

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right, Bundle.Trivialization.continuousOn_symm, Set.mem_univ, Set.mk_mem_prod
-- Module: Mathlib.Topology.VectorBundle.Basic
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_6] (TotalSpace.mk (E := E) b ∘ e.symm (E := E) b)

Tactic:
exact e.continuousOn_symm.comp_continuous (.prodMk_right _) fun x ↦
          mk_mem_prod hb (mem_univ x)

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right, Bundle.Trivialization.continuousOn_symm, Set.mem_univ, Set.mk_mem_prod
-- Module: Mathlib.Topology.VectorBundle.Basic
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)

Tactic:
continuous_zero.congr fun x => (e.symm_apply_of_notMem hb x).symm

Premises used: Bundle.Trivialization.symm_apply_of_notMem, Continuous.congr, continuous_zero, Eq.symm
-- Module: Mathlib.Topology.VectorBundle.Basic
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)

Tactic:
refine continuous_zero.congr fun x => (e.symm_apply_of_notMem hb x).symm

Premises used: Bundle.Trivialization.symm_apply_of_notMem, Continuous.congr, continuous_zero, Eq.symm
-- Module: Mathlib.Topology.VectorBundle.Basic
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
y : E b
⊢ ((symmL R (E := E) e b : ContinuousLinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) : (a : F) → E b)
      ((continuousLinearMapAt R (E := E) e b : (a : E b) → F) y) =
    y

Tactic:
e.symmₗ_linearMapAt hb y

Premises used: Bundle.Trivialization.symm, Bundle.Trivialization.symmₗ_linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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
y : F
⊢ (continuousLinearMapAt R (E := E) e b : (a : E b) → F)
      (((symmL R (E := E) e b : ContinuousLinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) : (a : F) → E b) y :
        E b) =
    y

Tactic:
e.linearMapAt_symmₗ hb y

Premises used: Bundle.Trivialization.symm, Bundle.Trivialization.linearMapAt_symmₗ
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Eq (α := (a : E b) → F) (⇑(continuousLinearEquivAt R (E := E) e b hb) : (a : E b) → F)
    (⇑(continuousLinearMapAt R (E := E) e b) : (a : E b) → F)

Tactic:
(e.coe_linearMapAt_of_mem hb).symm

Premises used: Bundle.Trivialization.coe_linearMapAt_of_mem, Eq.symm
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id R) (E b) F)
    (↑(continuousLinearEquivAt R (E := E) e b hb) : E b →L[R] F) (continuousLinearMapAt R (E := E) e b)

Tactic:
DFunLike.coe_injective (e.coe_linearMapAt_of_mem hb).symm

Premises used: Bundle.Trivialization.coe_linearMapAt_of_mem, DFunLike.coe_injective, Eq.symm
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Eq (α := (a : F) → E b) (⇑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b hb)) : (a : F) → E b)
    (⇑(symmL R (E := E) e b) : (a : F) → E b)

Tactic:
rfl

Premises used: Bundle.Trivialization.symm, dite, Bundle.Pretrivialization.symm, rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b))
    (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b hb)) : F →L[R] E b) (symmL R (E := E) e b)

Tactic:
rfl

Premises used: Bundle.Trivialization.symm, dite, Bundle.Pretrivialization.symm, Bundle.Trivialization.symmL, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : TotalSpace F E
hx : x ∈ e.source
⊢ (continuousLinearEquivAt R (E := E) e (x.proj (E := E)) ⋯ : (a : E x.proj) → F) (x.snd (E := E)) =
    ((↑e : TotalSpace F E → B × F) x).2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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
⊢ (↑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)

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.Basic
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

Tactic:
e.coe_fst ?_

Premises used: Bundle.Trivialization.coe_fst
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : TotalSpace.mk (E := E) b z ∈ e.source
⊢ ((↑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:
refine e.coe_fst ?_

Premises used: Bundle.Trivialization.coe_fst
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' e.baseSet) (TotalSpace.mk (E := E) b z)
⊢ TotalSpace.mk (E := E) b z ∈ e.source

Tactic:
rw [e.source_eq]

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' e.baseSet) (TotalSpace.mk (E := E) b z)

Tactic:
hb

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' e.baseSet) (TotalSpace.mk (E := E) b z)

Tactic:
exact hb
-- Module: Mathlib.Topology.VectorBundle.Basic
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)).2 =
    (b, (continuousLinearEquivAt R (E := E) e b hb : (a : E b) → F) z).2

Tactic:
simp only [continuousLinearEquivAt_apply]

Premises used: Bundle.Trivialization.continuousLinearEquivAt_apply