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)
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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
⊢ Eq (α := LinearMap.{u_1, u_1, u_4, u_3} (RingHom.id R) (E b) F) (Trivialization.linearMapAt R (E := E) e b)
    (↑(linearEquivAt R (E := E) e b hb) : E b →ₗ[R] F)

Tactic:
dif_pos hb

Premises used: Set.Mem, Bundle.Trivialization.linearMapAt, dif_pos, Bundle.Pretrivialization.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 : 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∉ e.baseSet
⊢ Eq (α := LinearMap.{u_1, u_1, u_4, u_3} (RingHom.id R) (E b) F) (Trivialization.linearMapAt R (E := E) e b) 0

Tactic:
dif_neg hb

Premises used: Set.Mem, Bundle.Trivialization.linearMapAt, dif_neg, Bundle.Pretrivialization.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 : 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
y : E b
⊢ e.symm (E := E) b ((Trivialization.linearMapAt R (E := E) e b : (a : E b) → F) y) = y

Tactic:
e.toPretrivialization.symmₗ_linearMapAt hb y

Premises used: Bundle.Trivialization.symm, dite, Bundle.Pretrivialization.symm, Bundle.Pretrivialization.symmₗ_linearMapAt, Bundle.Trivialization.toPretrivialization
-- 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
y : E b
⊢ ((Trivialization.symmₗ R (E := E) e b : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) : (a : F) → E b)
      ((Trivialization.linearMapAt R (E := E) e b : (a : E b) → F) y) =
    y

Tactic:
e.toPretrivialization.symmₗ_linearMapAt hb y

Premises used: Bundle.Pretrivialization.symmₗ_linearMapAt, Bundle.Trivialization.toPretrivialization
-- 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
y : F
⊢ (Trivialization.linearMapAt R (E := E) e b : (a : E b) → F) (e.symm (E := E) b y) = y

Tactic:
e.toPretrivialization.linearMapAt_symmₗ hb y

Premises used: Bundle.Trivialization.symm, Bundle.Pretrivialization.linearMapAt_symmₗ, dite, Bundle.Pretrivialization.symm, Bundle.Trivialization.toPretrivialization
-- 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
y : F
⊢ (Trivialization.linearMapAt R (E := E) e b : (a : E b) → F)
      (((Trivialization.symmₗ R (E := E) e b : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) : (a : F) → E b)
          y :
        E b) =
    y

Tactic:
e.toPretrivialization.linearMapAt_symmₗ hb y

Premises used: Bundle.Pretrivialization.linearMapAt_symmₗ, Bundle.Trivialization.toPretrivialization
-- 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
pos :
  ∀ (hb : b ∈ e.baseSet ∩ e'.baseSet),
    Continuous[inst_1, inst_1]
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(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) :
            F →ₗ[R] F)))
neg :
  ∀ (hb : b ∉ e.baseSet ∩ e'.baseSet),
    Continuous[inst_1, inst_1]
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(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) :
            F →ₗ[R] F)))
⊢ Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[R] F)))

Tactic:
by_cases hb : b ∈ e.baseSet ∩ 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 : 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
pos :
  Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯) : F →ₗ[R] F)))
⊢ Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[R] F)))

Tactic:
rw [dif_pos hb]

Premises used: dif_pos
-- 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]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯) : F →ₗ[R] F)))

Tactic:
(e'.continuousOn.comp_continuous ?_ ?_).snd

Premises used: ContinuousOn.comp_continuous, Continuous.snd, Bundle.Trivialization.continuousOn
-- 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
pos :
  Continuous[inst_1, inst_3] fun (x : F) ↦
    TotalSpace.mk (E := E) b
      ((((↑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
          (a : F) → E b)
        x)
pos₁ :
  ∀ (x : F),
    TotalSpace.mk (E := E) b
        ((((↑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯)) :
                LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            (a : F) → E b)
          x) ∈
      e'.source
⊢ Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯) : F →ₗ[R] F)))

Tactic:
refine (e'.continuousOn.comp_continuous ?_ ?_).snd

Premises used: ContinuousOn.comp_continuous, Continuous.snd, Bundle.Trivialization.continuousOn
-- 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.symm (linearEquivAt R (E := E) e b ⋯)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
          (a : F) → E b)
        x)

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

Premises used: Bundle.Trivialization.symm, Set.Mem, ContinuousOn.comp_continuous, Continuous.prodMk_right, Bundle.Trivialization.continuousOn_symm, dite, And.left, 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.symm (linearEquivAt R (E := E) e b ⋯)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
          (a : F) → E b)
        x)

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

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right, Bundle.Trivialization.continuousOn_symm, And.left, 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.symm (linearEquivAt R (E := E) e b ⋯)) :
                LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            (a : F) → E b)
          x) ∈
      e'.source

Tactic:
fun y => e'.mem_source.mpr hb.2

Premises used: Iff.mpr, And.right, 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.symm (linearEquivAt R (E := E) e b ⋯)) :
                LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            (a : F) → E b)
          x) ∈
      e'.source

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

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] (AddHom.toFun (LinearMap.toAddHom (↑(LinearEquiv.refl R F) : F →ₗ[R] F)))
⊢ Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[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] (AddHom.toFun (LinearMap.toAddHom (↑(LinearEquiv.refl R F) : F →ₗ[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] (AddHom.toFun (LinearMap.toAddHom (↑(LinearEquiv.refl R F) : F →ₗ[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)
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
pos :
  ∀ (hb : b ∈ e.baseSet ∩ e'.baseSet),
    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))
neg :
  ∀ (hb : b ∉ e.baseSet ∩ e'.baseSet),
    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))
⊢ 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:
by_cases hb : b ∈ e.baseSet ∩ 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 : 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
pos :
  Continuous[inst_1, inst_1]
    (LinearEquiv.invFun (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))
⊢ 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_pos hb]

Premises used: dif_pos
-- 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.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))

Tactic:
(e.continuousOn.comp_continuous ?_ ?_).snd

Premises used: ContinuousOn.comp_continuous, Continuous.snd, Bundle.Trivialization.continuousOn
-- 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
pos :
  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)
pos₁ :
  ∀ (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
⊢ Continuous[inst_1, inst_1]
    (LinearEquiv.invFun (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))

Tactic:
refine (e.continuousOn.comp_continuous ?_ ?_).snd

Premises used: ContinuousOn.comp_continuous, Continuous.snd, Bundle.Trivialization.continuousOn