awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : 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 : (b : B) → E b
u : Set B
b₀ : B
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, s x⟩.proj (E := E)) b₀ ∧
      (MDiffAt[u] fun (x : B) ↦
          ((↑(trivializationAt F E (⟨b₀, s b₀⟩.proj (E := E))) : TotalSpace F E → B × F) ⟨x, s x⟩).2)
        b₀ ↔
    (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E b₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) b₀
have change : MDiffAt[u] id b₀ ∧
    (MDiffAt[u] fun (x : B) ↦
        ((↑(trivializationAt F E (⟨b₀, s b₀⟩.proj (E := E))) : TotalSpace F E → B × F) ⟨x, s x⟩).2)
      b₀ ↔
  (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E b₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) b₀
Tactic: change MDifferentiableWithinAt _ _ id _ _ ∧ _ ↔ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
Goal:
𝕜 : 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
⊢ MDiffAt (TotalSpace.proj (E := E)) x
have this : MDiffAt id x
Tactic: have : MDifferentiableAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) id x := mdifferentiableAt_id
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
Goal:
𝕜 : 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 : MDiffAt id x
⊢ MDiffAt (TotalSpace.proj (E := E)) x
have this₁ : (MDiffAt fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
  (MDiffAt 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 [mdifferentiableAt_totalSpace] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : 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
⊢ (MDiffAt fun (x : B) ↦ ⟨x, 0⟩) x
have rw : (MDiffAt fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2) x
Tactic: rw [mdifferentiableAt_section]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : 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
⊢ (MDiffAt fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2) x
have apply : EventuallyEq.{u_2, u_4} (β := F) (𝓝 x) (fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2)
  fun (x : B) ↦ 0
Tactic: apply (mdifferentiableAt_const (c := 0)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : 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 (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 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 (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 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.MDifferentiable (goal)
Goal:
𝕜 : 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 (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2) x_3)
                    ((fun (x : B) ↦ (0 : F)) x_3))
                x_2}
            x_1}
      a
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝 x) (fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2)
    fun (x : B) ↦ 0
have h₁ : ∀ a ∈ Trivialization.baseSet (trivializationAt F E x),
  ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨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.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ (MDiffAt[s] fun (y : M) ↦ e.coordChange e' (f y) (g y)) 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.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g 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)
⊢ (MDiffAt[s] fun (y : M) ↦ e.coordChange e' (f y) (g y)) 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.MDifferentiable (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g 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.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g 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.MDifferentiable (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : f x₀ ∈ e.source
he' : f x₀ ∈ e'.source
⊢ (MDiffAt[s] fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) x₀
have he₁ : (f x₀).proj (E := E) ∈ e.baseSet
Tactic: rw [Trivialization.mem_source] at he he'
Cleared hypotheses: he, he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : f x₀ ∈ e.source
he' : f x₀ ∈ e'.source
he₁ : (f x₀).proj (E := E) ∈ e.baseSet
⊢ (MDiffAt[s] fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) x₀
have he'₁ : (f x₀).proj (E := E) ∈ e'.baseSet
Tactic: rw [Trivialization.mem_source] at he he'
Cleared hypotheses: he, he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : (f x₀).proj (E := E) ∈ e.baseSet
he' : (f x₀).proj (E := E) ∈ e'.baseSet
⊢ (MDiffAt[s] fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) x₀
have refine : EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x₀) (fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) fun (y : M) ↦
  e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2
Tactic: refine (hf.coordChange he'f he he').congr_of_eventuallyEq ?_ (by simp [he])
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : (f x₀).proj (E := E) ∈ e.baseSet
he' : (f x₀).proj (E := E) ∈ e'.baseSet
⊢ EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x₀) (fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) fun (y : M) ↦
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2
have h : ∀ (y : M) (hy : y ∈ TotalSpace.proj (E := E) ∘ f ⁻¹' e.baseSet),
  ((↑e' : TotalSpace F E → B × F) (f y)).2 =
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2
Tactic: filter_upwards [hf.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
f : M → TotalSpace F E
s : Set M
x₀ : M
he : f x₀ ∈ e.source
⊢ MDiffAt[s] f x₀ ↔
    (MDiffAt[s] fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
      (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
have rw : (MDiffAt[s] fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
    (MDiffAt[s] fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀ ↔
  (MDiffAt[s] fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
    (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
Tactic: rw [mdifferentiableWithinAt_totalSpace]