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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst_1, inst_3] fun (x : F) ↦
    TotalSpace.mk (E := E) b
      (((LinearEquiv.toEquiv (modM := inst_7 b) (modM₂ := inst_5) (linearEquivAt R (E := E) e' b ⋯)).symm :
          (a : F) → E b)
        x)

Tactic:
e'.continuousOn_symm.comp_continuous (Continuous.prodMk_right b) fun y =>
            mk_mem_prod hb.2 (mem_univ y)

Premises used: Bundle.Trivialization.symm, Set.Mem, ContinuousOn.comp_continuous, Continuous.prodMk_right, Bundle.Trivialization.continuousOn_symm, dite, And.right, Bundle.Pretrivialization.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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst_1, inst_3] fun (x : F) ↦
    TotalSpace.mk (E := E) b
      (((LinearEquiv.toEquiv (modM := inst_7 b) (modM₂ := inst_5) (linearEquivAt R (E := E) e' b ⋯)).symm :
          (a : F) → E b)
        x)

Tactic:
exact e'.continuousOn_symm.comp_continuous (Continuous.prodMk_right b) fun y =>
            mk_mem_prod hb.2 (mem_univ y)

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right, Bundle.Trivialization.continuousOn_symm, And.right, 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ ∀ (x : F),
    TotalSpace.mk (E := E) b
        (((LinearEquiv.toEquiv (modM := inst_7 b) (modM₂ := inst_5) (linearEquivAt R (E := E) e' b ⋯)).symm :
            (a : F) → E b)
          x) ∈
      e.source

Tactic:
fun y => e.mem_source.mpr hb.1

Premises used: Iff.mpr, And.left, Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ ∀ (x : F),
    TotalSpace.mk (E := E) b
        (((LinearEquiv.toEquiv (modM := inst_7 b) (modM₂ := inst_5) (linearEquivAt R (E := E) e' b ⋯)).symm :
            (a : F) → E b)
          x) ∈
      e.source

Tactic:
exact fun y => e.mem_source.mpr hb.1

Premises used: Iff.mpr, Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∉ e.baseSet ∩ e'.baseSet
neg : Continuous[inst_1, inst_1] (LinearEquiv.invFun (LinearEquiv.refl R F))
⊢ Continuous[inst_1, inst_1]
    (LinearEquiv.invFun
      (if hb : b ∈ e.baseSet ∩ e'.baseSet then
        LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯
      else LinearEquiv.refl R F))

Tactic:
rw [dif_neg hb]

Premises used: dif_neg
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∉ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst_1, inst_1] (LinearEquiv.invFun (LinearEquiv.refl R F))

Tactic:
continuous_id

Premises used: continuous_id
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∉ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst_1, inst_1] (LinearEquiv.invFun (LinearEquiv.refl R F))

Tactic:
exact continuous_id

Premises used: continuous_id
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Eq (α := (a : F) → F) (⇑(coordChangeL R (E := E) e e' b) : (a : F) → F)
    (⇑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯) : (a : F) → F)

Tactic:
congr_arg (fun f : F ≃ₗ[R] F ↦ ⇑f) (dif_pos hb)

Premises used: dif_pos, congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Eq (α := F ≃ₗ[R] F) (↑(coordChangeL R (E := E) e e' b) : F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯)

Tactic:
LinearEquiv.coe_injective (coe_coordChangeL _ _ hb)

Premises used: Bundle.Trivialization.coe_coordChangeL, LinearEquiv.coe_injective
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
a :
  Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)
⊢ Eq (α := F ≃L[R] F) (ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) (coordChangeL R (E := E) e' e b)

Tactic:
apply ContinuousLinearEquiv.toLinearEquiv_injective

Premises used: ContinuousLinearEquiv.toLinearEquiv_injective
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
a :
  Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₁ :
  Eq (α := F ≃ₗ[R] F) (LinearEquiv.symm (↑(coordChangeL R (E := E) e e' b) : F ≃ₗ[R] F))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₂ :
  Eq (α := F ≃ₗ[R] F)
    (LinearEquiv.symm (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₃ :
  Eq (α := F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ
      LinearEquiv.symm (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯)))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₄ a₅ :
  Eq (α := F ≃ₗ[R] F) (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
⊢ Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)

Tactic:
rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).toLinearEquiv_symm,
    coe_coordChangeL' e e' hb.symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]

Premises used: ContinuousLinearEquiv.toLinearEquiv_symm, Bundle.Trivialization.coordChangeL, LinearEquiv.symm_symm, LinearEquiv.trans_symm, And.symm, Bundle.Trivialization.coe_coordChangeL'
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (coordChangeL R (E := E) e e' b : (a : F) → F) y =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).2

Tactic:
congr_fun (coe_coordChangeL e e' hb) y

Premises used: Bundle.Trivialization.symm, Bundle.Trivialization.coe_coordChangeL, dite, Bundle.Pretrivialization.symm, congr_fun
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
fst :
  ((b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).1
snd :
  (b, (coordChangeL R (E := E) e e' b : (a : F) → F) y).2 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).2
⊢ (b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))

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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
fst : ((↑e.symm : B × F → TotalSpace F E) (b, y)).proj (E := E) ∈ e'.baseSet
⊢ ((b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).1

Tactic:
rw [e.mk_symm hb.1 y, e'.coe_fst', e.proj_symm_apply' hb.1]

Premises used: Bundle.Trivialization.coe_fst', Bundle.Trivialization.mk_symm, And.left, Bundle.Trivialization.proj_symm_apply'
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
fst : b ∈ e'.baseSet
⊢ ((↑e.symm : B × F → TotalSpace F E) (b, y)).proj (E := E) ∈ e'.baseSet

Tactic:
rw [e.proj_symm_apply' hb.1]

Premises used: And.left, Bundle.Trivialization.proj_symm_apply'
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ b ∈ e'.baseSet

Tactic:
hb.2

Premises used: And.right
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ b ∈ e'.baseSet

Tactic:
exact hb.2

Premises used: And.right
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, (coordChangeL R (E := E) e e' b : (a : F) → F) y).2 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).2

Tactic:
e.coordChangeL_apply e' hb y

Premises used: Bundle.Trivialization.coordChangeL_apply
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, (coordChangeL R (E := E) e e' b : (a : F) → F) y).2 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).2

Tactic:
exact e.coordChangeL_apply e' hb y

Premises used: Bundle.Trivialization.coordChangeL_apply
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
rw :
  (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))
rw₁ rw₂ :
  (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
    (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v))
⊢ (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
    (b, (coordChangeL R (E := E) e e' b : (a : F) → F) v)

Tactic:
rw [e.mk_coordChangeL e' hb, e.mk_symm hb.1]

Premises used: Bundle.Trivialization.mk_symm, And.left, Bundle.Trivialization.mk_coordChangeL
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
rw :
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).2 =
    ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2
rw₁ rw₂ :
  ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2 =
    ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2
⊢ (coordChangeL R (E := E) e e' b : (a : F) → F) y =
    ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2

Tactic:
rw [e.coordChangeL_apply e' hb, e.mk_symm hb.1]

Premises used: Bundle.Trivialization.coordChangeL_apply, Bundle.Trivialization.mk_symm, And.left
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Eq (α := (a : F) → F) (⇑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : (a : F) → F)
    (⇑(LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯) : (a : F) → F)

Tactic:
congr_arg LinearEquiv.invFun (dif_pos hb)

Premises used: dif_pos, dite, congr_arg, LinearEquiv.invFun, Bundle.Pretrivialization.symm
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : (x : B) → Zero (E x)
x : B
⊢ (zeroSection F E x).proj (E := E) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : (x : B) → Zero (E x)
x : B
⊢ (zeroSection F E x).snd (E := E) = 0

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
inst_9 : VectorBundle R F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_10 : MemTrivializationAtlas (E := E) e
⊢ Trivialization.IsLinear R (E := E) e

Tactic:
VectorBundle.trivialization_linear' e

Premises used: VectorBundle.trivialization_linear'
-- 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
inst_9 : VectorBundle R F E
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_10 : MemTrivializationAtlas (E := E) e
inst_11 : MemTrivializationAtlas (E := E) e'
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[R] F)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL R (E := E) e e' b) : F →L[R] F)) (e.baseSet ∩ e'.baseSet)

Tactic:
VectorBundle.continuousOn_coordChange' e e'

Premises used: VectorBundle.continuousOn_coordChange'