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
x : B
hx : x ∈ e.baseSet
simp_rw : (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x 0) = (x, 0)
simp_rw₁ : Eq (α := B × F) ((x, (continuousLinearEquivAt R (E := E) e x hx : (a : E x) → F) 0) : B × F) ((x, 0) : B × F)
⊢ (↑e : TotalSpace F E → B × F) (zeroSection F E x) = (x, 0)

Tactic:
simp_rw [zeroSection, e.apply_eq_prod_continuousLinearEquivAt R x hx 0, map_zero]

Premises used: map_zero, Bundle.zeroSection, Bundle.Trivialization.apply_eq_prod_continuousLinearEquivAt, OfNat.ofNat
-- 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
⊢ Continuous[inst_5, inst_6] (zeroSection F E)

Tactic:
continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- 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
refine : ∀ (x : B), ContinuousAt (zeroSection F E) x
⊢ Continuous[inst_5, inst_6] (zeroSection F E)

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- 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
x : B
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
⊢ ContinuousAt (Y := TotalSpace F E) (fun (x : B) ↦ TotalSpace.mk (E := E) x 0) x

Tactic:
rw [FiberBundle.continuousAt_section]

Premises used: FiberBundle.continuousAt_section
-- 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
x : B
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
⊢ 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:
apply (continuousAt_const (y := 0)).congr_of_eventuallyEq

Premises used: ContinuousAt.congr_of_eventuallyEq, continuousAt_const
-- 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
x y : B
hy : y ∈ baseSet (trivializationAt F E x)
⊢ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) y 0)).2 = 0

Tactic:
congr_arg Prod.snd <| (trivializationAt F E x).zeroSection R hy

Premises used: Bundle.zeroSection, Bundle.Trivialization.zeroSection, congr_arg, FiberBundle.trivializationAt, Prod.snd
-- 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
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
h₁ h₂ :
  ∀ (y : B) (hy : y ∈ baseSet (trivializationAt F E x)),
    ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) y 0)).2 = 0
⊢ 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:
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

Premises used: Bundle.Trivialization.open_baseSet, congr_arg, FiberBundle.trivializationAt, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt, Prod.snd
-- 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
s : Set B
⊢ ContinuousOn (zeroSection F E) s

Tactic:
(continuous_zeroSection R).continuousOn

Premises used: Continuous.continuousOn, Bundle.Trivialization.continuous_zeroSection
-- 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
x : B
⊢ ContinuousAt (zeroSection F E) x

Tactic:
(continuous_zeroSection R).continuousAt

Premises used: Bundle.Trivialization.continuous_zeroSection, Continuous.continuousAt
-- 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 : F
⊢ (↑e.symm : B × F → TotalSpace F E) (b, z) =
    TotalSpace.mk (E := E) b
      (((ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b hb) :
            ContinuousLinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
          (a : F) → E b)
        z)

Tactic:
simpa using (mk_symm _ hb _).symm

Premises used: Bundle.Trivialization.mk_symm, 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 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
h :
  ∀ (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)
⊢ 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)

Tactic:
ext v
-- 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 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
h :
  (ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b ⋯))
          (continuousLinearEquivAt R (E := E) e' b ⋯) :
        (a : F) → F)
      v =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2
⊢ 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)

Tactic:
rw [coordChangeL_apply e e' hb]

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 : 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
⊢ (ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (continuousLinearEquivAt R (E := E) e b ⋯))
          (continuousLinearEquivAt R (E := E) e' b ⋯) :
        (a : F) → F)
      v =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2

Tactic:
rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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)
⊢ Z.coordChange j k x ∘SL Z.coordChange i j x = Z.coordChange i k x

Tactic:
ext v
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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:
Z.coordChange_comp i j k x hx v

Premises used: VectorBundleCore.coordChange_comp
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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:
exact Z.coordChange_comp i j k x hx v

Premises used: VectorBundleCore.coordChange_comp
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : ι
p : B × F
⊢ p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Tactic:
Z.toFiberBundleCore.mem_trivChange_source i j p

Premises used: Set.Mem, VectorBundleCore.toFiberBundleCore, FiberBundleCore.mem_trivChange_source
-- Module: Mathlib.Topology.VectorBundle.Basic
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
i j : ι
⊢ Z.toFiberBundleCore.coordChange i j b = (⇑(Z.coordChange i j b) : (a : F) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : ι
p : Z.TotalSpace
⊢ (↑(Z.localTriv i) : TotalSpace F Z.Fiber → B × F) p =
    (p.proj (E := Z.Fiber),
      (Z.coordChange (Z.indexAt (p.proj (E := Z.Fiber))) i (p.proj (E := Z.Fiber)) : (a : F) → F)
        (p.snd (E := Z.Fiber)))

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', 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
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
i : ι
x : B
h : x ∈ (Z.localTriv i).baseSet
x_1 x_2 : Z.Fiber x
⊢ ((↑(Z.localTriv i) : TotalSpace F Z.Fiber → B × F) (TotalSpace.mk (E := Z.Fiber) x (x_1 + x_2))).2 =
    ((↑(Z.localTriv i) : TotalSpace F Z.Fiber → B × F) (TotalSpace.mk (E := Z.Fiber) x x_1)).2 +
      ((↑(Z.localTriv i) : TotalSpace F Z.Fiber → B × F) (TotalSpace.mk (E := Z.Fiber) x x_2)).2

Tactic:
simp only [map_add, localTriv_apply, mfld_simps]

Premises used: map_add, VectorBundleCore.localTriv_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 : 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 : ι
x : B
h : x ∈ (Z.localTriv i).baseSet
x_1 : R
x_2 : Z.Fiber x
⊢ ((↑(Z.localTriv i) : TotalSpace F Z.Fiber → B × F) (TotalSpace.mk (E := Z.Fiber) x (x_1 • x_2))).2 =
    x_1 • ((↑(Z.localTriv i) : TotalSpace F Z.Fiber → B × F) (TotalSpace.mk (E := Z.Fiber) x x_2)).2

Tactic:
simp only [map_smul, localTriv_apply, mfld_simps]

Premises used: VectorBundleCore.localTriv_apply, map_smul
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : ι
p : Z.TotalSpace
⊢ p ∈ (Z.localTriv i).source ↔ p.proj (E := Z.Fiber) ∈ Z.baseSet i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : ι
⊢ Z.baseSet i = (Z.localTriv i).baseSet

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : ι
p : B × F
⊢ p ∈ (Z.localTriv i).target ↔ p.1 ∈ (Z.localTriv i).baseSet

Tactic:
Z.toFiberBundleCore.mem_localTriv_target i p

Premises used: Set.Mem, FiberBundleCore.mem_localTriv_target, VectorBundleCore.toFiberBundleCore
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : ι
p : B × F
⊢ (↑(Z.localTriv i).symm : B × F → TotalSpace F Z.Fiber) p =
    TotalSpace.mk (E := Z.Fiber) p.1 ((Z.coordChange i (Z.indexAt p.1) p.1 : (a : F) → F) p.2)

Tactic:
rfl

Premises used: VectorBundleCore.Fiber, OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
v : F
⊢ (Z.localTriv i).symm (E := Z.Fiber) b v = (Z.coordChange i (Z.indexAt b) b : (a : F) → F) v

Tactic:
apply (Z.localTriv i).symm_apply hb v

Premises used: VectorBundleCore.localTriv, Bundle.Trivialization.symm_apply
-- Module: Mathlib.Topology.VectorBundle.Basic
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
hb₁ : b ∈ (Z.localTriv i).baseSet ∩ (Z.localTriv j).baseSet
⊢ 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)

Tactic:
rw [Trivialization.coordChangeL_apply', localTriv_symm_fst, localTriv_apply, coordChange_comp]

Premises used: VectorBundleCore.localTriv_symm_fst, VectorBundleCore.localTriv_apply, Bundle.Trivialization.coordChangeL_apply', VectorBundleCore.coordChange_comp
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ 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:
⟨⟨hb.1, Z.mem_baseSet_at b⟩, hb.2⟩

Premises used: Set.Mem, setOf, VectorBundleCore.mem_baseSet_at, Set.inter, And.right, And.left, And.intro
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ b ∈ (Z.localTriv i).baseSet ∩ (Z.localTriv j).baseSet

Tactic:
hb

Premises used: Set.Mem, setOf, Set.inter
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ 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:
exacts [⟨⟨hb.1, Z.mem_baseSet_at b⟩, hb.2⟩, hb]
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Z.localTriv (Z.indexAt b) = Z.localTrivAt b

Tactic:
rfl

Premises used: VectorBundleCore.localTrivAt, rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
rw : TotalSpace.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) b a) ∈ Z.baseSet (Z.indexAt b)
⊢ TotalSpace.mk (E := Z.Fiber) b a ∈ (Z.localTrivAt b).source

Tactic:
rw [localTrivAt, mem_localTriv_source]

Premises used: VectorBundleCore.localTrivAt, VectorBundleCore.mem_localTriv_source
-- Module: Mathlib.Topology.VectorBundle.Basic
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.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) b a) ∈ Z.baseSet (Z.indexAt b)

Tactic:
Z.mem_baseSet_at b

Premises used: Set.Mem, VectorBundleCore.mem_baseSet_at
-- Module: Mathlib.Topology.VectorBundle.Basic
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.proj (F := F) (E := Z.Fiber) (TotalSpace.mk (E := Z.Fiber) b a) ∈ Z.baseSet (Z.indexAt b)

Tactic:
exact Z.mem_baseSet_at b

Premises used: VectorBundleCore.mem_baseSet_at