awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) x
have rw : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k
  (fun (x_1 : M) ↦ ((↑(trivializationAt F V x) : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) x
Tactic: rw [contMDiffAt_section]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
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
⊢ ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2)
    x
have this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
Tactic: have : CMDiffAt k (fun (_x : M) ↦ w) x := contMDiffAt_const
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
⊢ ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2)
    x
have refine : EventuallyEq.{u_4, u_5} (β := F) (𝓝 x)
  (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) fun (_x : M) ↦ w
Tactic: refine this.congr_of_eventuallyEq ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
⊢ EventuallyEq.{u_4, u_5} (β := F) (𝓝 x)
    (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) fun (_x : M) ↦ w
have apply : ∃ (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: apply eventually_nhds_iff.mpr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
⊢ ∃ (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
have 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)
Tactic: refine ⟨t.baseSet, ?_, t.open_baseSet, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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)
⊢ ∃ (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
have refine_2 : x ∈ t.baseSet
Tactic: refine ⟨t.baseSet, ?_, t.open_baseSet, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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 ∈ 𝓝 x₀, MDiff[s] fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩
have 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'⟩
Tactic: obtain ⟨s, hs, hsσ⟩ := exists_contMDiffOn_extend (k := 1) I F σ₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Pullback (goal)
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))
have 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)
Tactic: refine ((contMDiffOn_coordChangeL e e').comp f.contMDiff.contMDiffOn fun b hb => hb).congr ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Pullback (goal)
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)
⊢ 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)
have 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)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Pullback (goal)
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
⊢ 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)
have 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)
Tactic: change ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Pullback (goal)
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
⊢ 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)
have 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
Tactic: rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Pullback (goal)
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
⊢ 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)
have 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)
Tactic: rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
h : IsContMDiffRiemannianBundle IB n F E
h' : n' ≤ n
⊢ IsContMDiffRiemannianBundle IB n' F E
have rcases : ∀ (g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ)
  (g_smooth :
    ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
      TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) n fun (b : B) ↦ ⟨b, g b⟩)
  (hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w),
  IsContMDiffRiemannianBundle IB n' F E
Tactic: rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
inst_12 : IsContMDiffRiemannianBundle IB 3 F E
⊢ LE.le (α := ℕ∞ω) 2 3
have norm_cast : LE.le (α := ℕ) 2 3
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
⊢ IsContMDiffRiemannianBundle IB n F₁ (Trivial B F₁)
have refine : ∀ (x : B),
  ContMDiffAt IB (E' := Prod.{u_1, u_6} EB (F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_6, u_6} (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (b : B) ↦ Trivial B F₁ b →L[ℝ] Trivial B F₁ b →L[ℝ] ℝ) n
    (fun (b : B) ↦ ⟨b, (fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) b⟩) x
Tactic: refine ⟨fun x ↦ innerSL ℝ, fun x ↦ ?_, fun x v w ↦ rfl⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
F₁ : Type u_6
inst_12 : NormedAddCommGroup F₁
inst_13 : InnerProductSpace ℝ F₁
x : B
⊢ ContMDiffAt IB (E' := Prod.{u_1, u_6} EB (F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_6, u_6} (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (b : B) ↦ Trivial B F₁ b →L[ℝ] Trivial B F₁ b →L[ℝ] ℝ) n
    (fun (b : B) ↦ ⟨b, (fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) b⟩) x
have simp : ContMDiffAt.{0, u_1, u_2, u_3, u_6, u_6, u_6} IB (E' := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) 𝓘(ℝ, F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (M' :=
  F₁ →L[ℝ] F₁ →L[ℝ] ℝ) n
  (fun (x_1 : B) ↦
    ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) x) :
          (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
            B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
        ⟨x_1, innerSL ℝ⟩).2)
  x
Tactic: simp only [contMDiffAt_section]