awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
      x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
have simp_rw : ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ →
  ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ x) a x₀
Tactic: simp_rw [contMDiffWithinAt_totalSpace, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) x₀ ↔
    ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) x₀
have simp_rw : ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) x₀ →
  ContMDiffAt IB IB (M' := B) n (fun (x : B) ↦ x) x₀
Tactic: simp_rw [contMDiffAt_totalSpace, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (TotalSpace.proj (E := E)) x
have this : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x
Tactic: have : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x := contMDiffAt_id
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
this : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x
⊢ ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (TotalSpace.proj (E := E)) x
have this₁ : ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
  ContMDiffAt (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
    (fun (x_1 : TotalSpace F E) ↦
      ((↑(trivializationAt F E ((id x).proj (E := E))) : TotalSpace F E → B × F) (id x_1)).2)
    x
Tactic: rw [contMDiffAt_totalSpace] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk (E := E) x 0) x
have rw : ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
  (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2) x
Tactic: rw [contMDiffAt_section]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
⊢ ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x_1 : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x_1 0)).2) x
have apply : EventuallyEq.{u_2, u_4} (β := 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: apply (contMDiffAt_const (c := 0)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
⊢ EventuallyEq.{u_2, u_4} (β := 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
have h : ∀ (a : B),
  Membership.mem (γ := Set B)
    {x_1 : B |
      x_1 ∈ Trivialization.baseSet (trivializationAt F E x) →
        Membership.mem (γ := Set B)
          {x_2 : B |
            (fun (x_3 : B) ↦
                Eq.{u_4 + 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
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 𝕜 hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
h :
  ∀ (a : B),
    Membership.mem (γ := Set B)
      {x_1 : B |
        x_1 ∈ Trivialization.baseSet (trivializationAt F E x) →
          Membership.mem (γ := Set B)
            {x_2 : B |
              (fun (x_3 : B) ↦
                  Eq.{u_4 + 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
⊢ EventuallyEq.{u_2, u_4} (β := 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
have h₁ : ∀ a ∈ Trivialization.baseSet (trivializationAt F E x),
  ((↑(trivializationAt F E x) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) a 0)).2 = 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 𝕜 hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
⊢ ContMDiffVectorBundle 0 F E IB
have contMDiffOn_coordChangeL : ∀ (e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)))
  [inst_19 : MemTrivializationAtlas (E := E) e] [inst_20 : MemTrivializationAtlas (E := E) e'],
  ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) 0
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
he' : MemTrivializationAtlas (E := E) e'
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) 0
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)
have contMDiffOn_coordChangeL : ContinuousOn.{u_2, u_4} (Y := F →L[𝕜] F) (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F))
  (e.baseSet ∩ e'.baseSet)
Tactic: rw [contMDiffOn_zero_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F))
    (e.baseSet ∩ e'.baseSet)
have rw : ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
  (fun (b : B) ↦ (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F))
  (e'.baseSet ∩ e.baseSet)
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F))
    (e'.baseSet ∩ e.baseSet)
have refine : ∀ (b : B) (hb : b ∈ e'.baseSet ∩ e.baseSet),
  Eq (α := F →L[𝕜] F) (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F)
    (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)
Tactic: refine (ContMDiffVectorBundle.contMDiffOn_coordChangeL e' e).congr fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ Eq (α := F →L[𝕜] F) (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F)
    (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)
have rw : Eq (α := F →L[𝕜] F) (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)
  (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)
Tactic: rw [e.symm_coordChangeL e' hb]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ e.coordChange e' (f y) (g y)) s x
have refine_1 : EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ e.coordChange e' (f y) (g y)) fun (x : M) ↦
  ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)
Tactic: refine ((hf.coordChangeL he he').clm_apply hg).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
refine_1 :
  EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ e.coordChange e' (f y) (g y)) fun (x : M) ↦
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ e.coordChange e' (f y) (g y)) s x
have refine_2 : e.coordChange e' (f x) (g x) = ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)
Tactic: refine ((hf.coordChangeL he he').clm_apply hg).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ e.coordChange e' (f y) (g y)) fun (x : M) ↦
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)
have this : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)
Tactic: have : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x) :=
     (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨he, he'⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
this : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)
⊢ EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ e.coordChange e' (f y) (g y)) fun (x : M) ↦
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)
have h : ∀ (y : M) (hy : y ∈ f ⁻¹' (e.baseSet ∩ e'.baseSet)),
  e.coordChange e' (f y) (g y) =
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F) : (a : F) → F) (g y)
Tactic: filter_upwards [hf.continuousWithinAt this] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) : B × F → B × F)
    (e.target ∩ e'.target)
have Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet)
Tactic: have Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet) := fun x hx ↦
    ⟨e.mem_target.1 hx.1, e'.mem_target.1 hx.2⟩