awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
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₀
⊢ 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₀

Tactic:
rw [mdifferentiableWithinAt_totalSpace]

Premises used: mdifferentiableWithinAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
h :
  (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) ↦ ((↑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) ↦ ((↑(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:
apply and_congr_right

Premises used: and_congr_right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
hf : (MDiffAt[s] fun (x : M) ↦ (f x).proj (E := E)) x₀
h h₁ :
  (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀ ↔
    (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) 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) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
rw [Trivialization.mdifferentiableWithinAt_snd_comp_iff₂ IB
    (FiberBundle.mem_trivializationAt_proj_source) he hf]

Premises used: FiberBundle.mem_trivializationAt_proj_source, Bundle.Trivialization.mdifferentiableWithinAt_snd_comp_iff₂
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
x₀ : M
he : f x₀ ∈ e.source
rw :
  (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
      (MDiffAt fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀ ↔
    (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧ (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
⊢ MDiffAt f x₀ ↔
    (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧ (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
rw [mdifferentiableAt_totalSpace]

Premises used: mdifferentiableAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
x₀ : M
he : f x₀ ∈ e.source
h :
  (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀ →
    ((MDiffAt fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀ ↔
      (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀)
⊢ (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
      (MDiffAt fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀ ↔
    (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧ (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
apply and_congr_right

Premises used: and_congr_right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
x₀ : M
he : f x₀ ∈ e.source
hf : (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀
h h₁ :
  (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀ ↔
    (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
⊢ (MDiffAt fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀ ↔
    (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
rw [Trivialization.mdifferentiableAt_snd_comp_iff₂ IB
    (FiberBundle.mem_trivializationAt_proj_source) he hf]

Premises used: FiberBundle.mem_trivializationAt_proj_source, Bundle.Trivialization.mdifferentiableAt_snd_comp_iff₂
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
rw :
  (MDiffAt[u] fun (x : B) ↦ ⟨x, s x⟩.proj (E := E)) b₀ ∧
      (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀ ↔
    (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀
he : ⟨b₀, s b₀⟩ ∈ e.source
⊢ MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀

Tactic:
rw [e.mdifferentiableWithinAt_totalSpace_iff IB]

Premises used: Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
change :
  MDiffAt[u] id b₀ ∧ (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀ ↔
    (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, s x⟩.proj (E := E)) b₀ ∧
      (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀ ↔
    (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀

Tactic:
change MDifferentiableWithinAt IB IB id u b₀ ∧ _ ↔ _

Premises used: id, MDifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ MDiffAt[u] id b₀ ∧ (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀ ↔
    (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀

Tactic:
simp [mdifferentiableWithinAt_id]

Premises used: mdifferentiableWithinAt_id
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ ⟨b₀, s b₀⟩ ∈ e.source

Tactic:
(coe_mem_source e).mpr hex₀

Premises used: Iff.mpr, Set.Mem, Bundle.Trivialization.coe_mem_source
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ ⟨b₀, s b₀⟩ ∈ e.source

Tactic:
exact (coe_mem_source e).mpr hex₀

Premises used: Iff.mpr, Bundle.Trivialization.coe_mem_source
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
s : (b : B) → E b
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ MDiffAt (T% s) b₀ ↔ (MDiffAt fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀

Tactic:
simpa [← mdifferentiableWithinAt_univ] using e.mdifferentiableWithinAt_section_iff IB s hex₀

Premises used: mdifferentiableWithinAt_univ, Bundle.Trivialization.mdifferentiableWithinAt_section_iff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
⊢ MDiff[a] (T% s) ↔ MDiff[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2

Tactic:
⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
refine_1 :
  ∀ (h : MDiff[a] (T% s)) (x : B) (hx : x ∈ a), (MDiffAt[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) x
refine_2 :
  ∀ (h : MDiff[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) (x : B) (hx : x ∈ a), MDiffAt[a] (T% s) x
⊢ MDiff[a] (T% s) ↔ MDiff[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
h : MDiff[a] (T% s)
x : B
hx : x ∈ a
⊢ MDiffAt (T% s) x

Tactic:
have := (h x hx).mdifferentiableAt <| ha.mem_nhds hx
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
h : MDiff[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2
x : B
hx : x ∈ a
⊢ (MDiffAt fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) x

Tactic:
have := (h x hx).mdifferentiableAt <| ha.mem_nhds hx
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
h : MDiff[a] (T% s)
x : B
hx : x ∈ a
this : MDiffAt (T% s) x
⊢ (MDiffAt[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) x

Tactic:
((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mp this).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, Bundle.Trivialization.mdifferentiableAt_section_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
h : MDiff[a] (T% s)
x : B
hx : x ∈ a
this : MDiffAt (T% s) x
⊢ (MDiffAt[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) x

Tactic:
exact ((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mp this).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, Bundle.Trivialization.mdifferentiableAt_section_iff, Iff.mp