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 : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
have apply : ∀ (y : B) (hy : Membership.mem (γ := Set B) univ y),
  Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩
Tactic: apply (MDifferentiableWithinAt.sum_section_of_locallyFinite ht ht').congr' (t := Set.univ)
      (fun y hy ↦ ?_) (by grind) trivial
-- 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 : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : Membership.mem (γ := Set B) univ y
⊢ Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩
have choose : ∀ (U : Set B) (hu : U ∈ 𝓝 y)
  (hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}),
  Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩
Tactic: choose U hu hfin using ht y
-- 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 : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
x : ι
hx : Membership.mem (γ := Set ι) {x : ι | t x y ≠ 0} x
⊢ Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty} x
have hx₁ : t x y ≠ 0
Tactic: rw [Set.mem_setOf] at hx ⊢
Cleared hypotheses: hx
-- 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 : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
x : ι
hx : t x y ≠ 0
⊢ ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) x ∩ U).Nonempty
have h : y ∈ (fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) x ∩ U
Tactic: use y
-- 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 : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
⊢ Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩
have this : Subset.{u_9} (α := Set ι) {x : ι | t x y ≠ 0} {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
Tactic: have : {x | t x y ≠ 0} ⊆ {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty} := by
    intro x hx
    rw [Set.mem_setOf] at hx ⊢
    use y
    simpa using ⟨hx, mem_of_mem_nhds hu⟩
-- 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 : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : Membership.mem (γ := Set B) univ y
U : Set B
hu : U ∈ 𝓝 y
hfin : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
this :
  Subset.{u_9} (α := Set ι) {x : ι | t x y ≠ 0} {i : ι | ((fun (i : ι) ↦ ({x : B | t i x ≠ 0} : Set B)) i ∩ U).Nonempty}
⊢ Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑' (i : ι), t i y⟩
have rw : Eq (α := TotalSpace F E) ⟨y, ∑ᶠ (i : ι), t i y⟩ ⟨y, ∑ᶠ (b : ι), t b y⟩
Tactic: rw [tsum_eq_finsum (hfin.subset this)]
-- 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 : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite.{u_9, u_2} (X := B) fun (i : ι) ↦ {x : B | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt (T% t) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
have ht'₁ : ∀ (i : ι), MDiffAt[univ] (T% t) x₀
Tactic: simp_rw [← mdifferentiableWithinAt_univ] at ht' ⊢
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : (MDiffAt[s] fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : (MDiffAt[s] fun (m : M) ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : MDiffAt[s] b₂ m₀
⊢ (MDiffAt[s] fun (m : M) ↦ ⟨b₂ m, (ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m)⟩) m₀
have rw : ∀
  (hv :
    (MDiffAt[s] fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀ ∧
      (MDiffAt[s] fun (x : M) ↦
          ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
                TotalSpace F₁ E₁ → B₁ × F₁)
              ⟨b₁ x, v x⟩).2)
        m₀)
  (hb₂ : MDiffAt[s] b₂ m₀),
  (MDiffAt[s] fun (x : M) ↦
        TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂) ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩)
      m₀ ∧
    (MDiffAt[s] fun (x : M) ↦
        ((↑(trivializationAt F₂ E₂
                  (TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂)
                    ⟨b₂ m₀, (ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀)⟩)) :
              TotalSpace F₂ E₂ → B₂ × F₂)
            ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩).2)
      m₀
Tactic: rw [mdifferentiableWithinAt_totalSpace] at hv ⊢
Cleared hypotheses: hv, hb₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : (MDiffAt[s] fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv :
  (MDiffAt[s] fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀ ∧
    (MDiffAt[s] fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      m₀
hb₂ : MDiffAt[s] b₂ m₀
⊢ (MDiffAt[s] fun (x : M) ↦
        TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂) ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩)
      m₀ ∧
    (MDiffAt[s] fun (x : M) ↦
        ((↑(trivializationAt F₂ E₂
                  (TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂)
                    ⟨b₂ m₀, (ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀)⟩)) :
              TotalSpace F₂ E₂ → B₂ × F₂)
            ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩).2)
      m₀
have refine : (MDiffAt[s] fun (x : M) ↦
    ((↑(trivializationAt F₂ E₂
              (TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂)
                ⟨b₂ m₀, (ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀)⟩)) :
          TotalSpace F₂ E₂ → B₂ × F₂)
        ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩).2)
  m₀
Tactic: refine ⟨hb₂, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : (MDiffAt[s] fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv :
  (MDiffAt[s] fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀ ∧
    (MDiffAt[s] fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      m₀
hb₂ : MDiffAt[s] b₂ m₀
⊢ (MDiffAt[s] fun (x : M) ↦
      ((↑(trivializationAt F₂ E₂
                (TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂)
                  ⟨b₂ m₀, (ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀)⟩)) :
            TotalSpace F₂ E₂ → B₂ × F₂)
          ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩).2)
    m₀
have apply : EventuallyEq.{u_6, u_3} (β := F₂) (𝓝[insert m₀ s] m₀)
  (fun (x : M) ↦
    ((↑(trivializationAt F₂ E₂
              (TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂)
                ⟨b₂ m₀, (ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀)⟩)) :
          TotalSpace F₂ E₂ → B₂ × F₂)
        ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩).2)
  fun (x : M) ↦
  (inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ x) (b₂ m₀) (b₂ x) (ϕ x) : (a : F₁) → F₂)
    ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
          TotalSpace F₁ E₁ → B₁ × F₁)
        ⟨b₁ x, v x⟩).2
Tactic: apply (MDifferentiableWithinAt.clm_apply hϕ hv.2).congr_of_eventuallyEq_insert
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : (MDiffAt[s] fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv :
  (MDiffAt[s] fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀ ∧
    (MDiffAt[s] fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      m₀
hb₂ : MDiffAt[s] b₂ m₀
⊢ ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
have a : Membership.mem (γ := Filter B₁) (𝓝 ((fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀))
  (Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀)))
Tactic: apply hv.1.insert.continuousWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : (MDiffAt[s] fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv :
  (MDiffAt[s] fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀ ∧
    (MDiffAt[s] fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      m₀
hb₂ : MDiffAt[s] b₂ m₀
⊢ Membership.mem (γ := Filter B₁)
    (𝓝 ((fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀))
    (Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀)))
have a : (fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) m₀ ∈
  Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
Tactic: apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds