awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
refine_1 :
  ∀ y ∈ t.baseSet,
    Eq.{u_5 + 1} (α := F) ((fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) y)
      ((fun (_x : M) ↦ w) y)
refine_2 : x ∈ t.baseSet
⊢ ∃ (t_1 : Set M),
    (∀ y ∈ t_1,
        Eq.{u_5 + 1} (α := F) ((fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) y)
          ((fun (_x : M) ↦ w) y)) ∧
      IsOpen[inst_4] t_1 ∧ x ∈ t_1

Tactic:
refine ⟨t.baseSet, ?_, t.open_baseSet, ?_⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x_1 : M
σ₀ : V x_1
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x_1
w : F := ((↑t : TotalSpace F V → M × F) ⟨x_1, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x_1
x : M
hx : x ∈ t.baseSet
⊢ Eq.{u_5 + 1} (α := F) ((fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2) x)
    ((fun (_x : M) ↦ w) x)

Tactic:
simp [extend, t, hx, w]

Premises used: FiberBundle.extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
⊢ x ∈ t.baseSet

Tactic:
FiberBundle.mem_baseSet_trivializationAt' x

Premises used: FiberBundle.mem_baseSet_trivializationAt', Set.Mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
⊢ x ∈ t.baseSet

Tactic:
exact FiberBundle.mem_baseSet_trivializationAt' x

Premises used: FiberBundle.mem_baseSet_trivializationAt'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle 1 F V I
x₀ : M
σ₀ : V x₀
obtain :
  ∀ (s : Set M) (hs : s ∈ 𝓝 x₀)
    (hsσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) 1 (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) s),
    ∃ s ∈ 𝓝 x₀, MDiff[s] fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩
⊢ ∃ s ∈ 𝓝 x₀, MDiff[s] fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩

Tactic:
obtain ⟨s, hs, hsσ⟩ := exists_contMDiffOn_extend (k := 1) I F σ₀

Premises used: FiberBundle.exists_contMDiffOn_extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle 1 F V I
x₀ : M
σ₀ : V x₀
s : Set M
hs : s ∈ 𝓝 x₀
hsσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) 1 (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) s
⊢ ∃ s ∈ 𝓝 x₀, MDiff[s] fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩

Tactic:
⟨s, hs, hsσ.mdifferentiableOn one_ne_zero⟩

Premises used: And.intro, Exists.intro, one_ne_zero, ContMDiffOn.mdifferentiableOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle 1 F V I
x₀ : M
σ₀ : V x₀
s : Set M
hs : s ∈ 𝓝 x₀
hsσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) 1 (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) s
⊢ ∃ s ∈ 𝓝 x₀, MDiff[s] fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩

Tactic:
exact ⟨s, hs, hsσ.mdifferentiableOn one_ne_zero⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
x : M
σ₀ : V x
⊢ (MDiffAt fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) x

Tactic:
(contMDiffAt_extend' (k := 1) I F σ₀).mdifferentiableAt one_ne_zero

Premises used: ContMDiffAt.mdifferentiableAt, FiberBundle.contMDiffAt_extend', one_ne_zero
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
⊢ ContMDiffOn.{u_1, u_8, u_9, u_3, u_4, u_4, u_4} IB' (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B') ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f)
            b) :
        F →L[𝕜] F))
    (Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e.pullback (E := E) f) ∩
      Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e'.pullback (E := E) f))

Tactic:
((contMDiffOn_coordChangeL e e').comp f.contMDiff.contMDiffOn fun b hb => hb).congr ?_

Premises used: Set.Mem, setOf, ContMDiffMap.contMDiff, ContMDiff.contMDiffOn, Set.inter, Set.preimage, ContMDiffOn.congr, contMDiffOn_coordChangeL, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
refine :
  ∀ (y : B'),
    Membership.mem (γ := Set B') ((⇑f : (a : B') → B) ⁻¹' (e.baseSet ∩ e'.baseSet)) y →
      Eq (α := F →L[𝕜] F)
        (↑(Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f)
              (e'.pullback (E := E) f) y) :
          F →L[𝕜] F)
        (((fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) ∘ (⇑f : (a : B') → B)) y)
⊢ ContMDiffOn.{u_1, u_8, u_9, u_3, u_4, u_4, u_4} IB' (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B') ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f)
            b) :
        F →L[𝕜] F))
    (Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e.pullback (E := E) f) ∩
      Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e'.pullback (E := E) f))

Tactic:
refine ((contMDiffOn_coordChangeL e e').comp f.contMDiff.contMDiffOn fun b hb => hb).congr ?_

Premises used: ContMDiffMap.contMDiff, ContMDiff.contMDiffOn, ContMDiffOn.congr, contMDiffOn_coordChangeL, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
h :
  ∀ (v : F),
    Eq (α := F)
      (((↑(Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f)
                  (e'.pullback (E := E) f) b) :
              F →L[𝕜] F) :
            (a : F) → F)
          v :
        F)
      ((((fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) ∘ (⇑f : (a : B') → B)) b :
            (a : F) → F)
          v :
        F)
⊢ Eq (α := F →L[𝕜] F)
    (↑(Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f)
          b) :
      F →L[𝕜] F)
    (((fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) ∘ (⇑f : (a : B') → B)) b)

Tactic:
ext v
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
h :
  Eq (α := F)
    ((Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f) b :
          (a : F) → F)
        v :
      F)
    ((Trivialization.coordChangeL 𝕜 (E := E) e e' ((f : (a : B') → B) b) : (a : F) → F) v : F)
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f)
                b) :
            F →L[𝕜] F) :
          (a : F) → F)
        v :
      F)
    ((((fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) ∘ (⇑f : (a : B') → B)) b :
          (a : F) → F)
        v :
      F)

Tactic:
change ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v

Premises used: Bundle.Trivialization.pullback, Bundle.Trivialization.coordChangeL, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
h :
  ((↑(e'.pullback (E := E) f) : TotalSpace F ((⇑f : (a : B') → B) *ᵖ E) → B' × F)
        ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (e.pullback (E := E) f))) :
            B' × F → TotalSpace F ((⇑f : (a : B') → B) *ᵖ E))
          (b, v))).2 =
    ((↑e' : TotalSpace F E → B × F) ⟨(f : (a : B') → B) b, e.symm (E := E) ((f : (a : B') → B) b) v⟩).2
h₁ :
  b ∈
    Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e.pullback (E := E) f) ∩
      Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e'.pullback (E := E) f)
⊢ Eq (α := F)
    ((Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f) b :
          (a : F) → F)
        v :
      F)
    ((Trivialization.coordChangeL 𝕜 (E := E) e e' ((f : (a : B') → B) b) : (a : F) → F) v : F)

Tactic:
rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]

Premises used: Bundle.Trivialization.coordChangeL_apply, Bundle.Trivialization.pullback, Bundle.Trivialization.coordChangeL_apply'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
⊢ ((↑(e'.pullback (E := E) f) : TotalSpace F ((⇑f : (a : B') → B) *ᵖ E) → B' × F)
        ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (e.pullback (E := E) f))) :
            B' × F → TotalSpace F ((⇑f : (a : B') → B) *ᵖ E))
          (b, v))).2 =
    ((↑e' : TotalSpace F E → B × F) ⟨(f : (a : B') → B) b, e.symm (E := E) ((f : (a : B') → B) b) v⟩).2

Tactic:
rfl

Premises used: Bundle.Trivialization.symm, Set.Mem, Bundle.Pullback, Bundle.Trivialization.pullback, dite, Bundle.Pretrivialization.symm, Bundle.Pullback.lift, rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
⊢ b ∈
    Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e.pullback (E := E) f) ∩
      Trivialization.baseSet (Z := TotalSpace.{u_3, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
        (e'.pullback (E := E) f)

Tactic:
hb

Premises used: Set.Mem, setOf, Bundle.Pullback, Set.inter, Set.preimage
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback
Goal:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_5} 𝕜 (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace (TotalSpace F E)
inst_6 : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst_7 : NormedAddCommGroup EB
inst_8 : NormedSpace 𝕜 EB
HB : Type u_7
inst_9 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_10 : TopologicalSpace B
inst_11 : ChartedSpace HB B
EB' : Type u_8
inst_12 : NormedAddCommGroup EB'
inst_13 : NormedSpace 𝕜 EB'
HB' : Type u_9
inst_14 : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst_15 : TopologicalSpace B'
inst_16 : ChartedSpace HB' B'
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
⊢ ((↑(e'.pullback (E := E) f) : TotalSpace F ((⇑f : (a : B') → B) *ᵖ E) → B' × F)
        ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (e.pullback (E := E) f))) :
            B' × F → TotalSpace F ((⇑f : (a : B') → B) *ᵖ E))
          (b, v))).2 =
    ((↑e' : TotalSpace F E → B × F) ⟨(f : (a : B') → B) b, e.symm (E := E) ((f : (a : B') → B) b) v⟩).2

Tactic:
exacts [rfl, hb]

Premises used: rfl