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
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] 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₀
have 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₀)
Tactic: apply and_congr_right
-- 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
hf : (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₀
have 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₀
Tactic: rw [Trivialization.mdifferentiableWithinAt_snd_comp_iff₂ IB
    (FiberBundle.mem_trivializationAt_proj_source) he hf]
-- 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
x₀ : M
he : f x₀ ∈ e.source
⊢ 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₀
have 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₀
Tactic: rw [mdifferentiableAt_totalSpace]
-- 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
x₀ : M
he : f x₀ ∈ e.source
⊢ (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₀
have 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₀)
Tactic: apply and_congr_right
-- 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
x₀ : M
he : f x₀ ∈ e.source
hf : (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₀
have 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₀
Tactic: rw [Trivialization.mdifferentiableAt_snd_comp_iff₂ IB
    (FiberBundle.mem_trivializationAt_proj_source) he hf]
-- 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
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] (T% s) b₀ ↔ (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀
have 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₀
Tactic: rw [e.mdifferentiableWithinAt_totalSpace_iff IB]
-- 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
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₀
⊢ MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) b₀
have he : ⟨b₀, s b₀⟩ ∈ e.source
Tactic: rw [e.mdifferentiableWithinAt_totalSpace_iff IB]
-- 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
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] 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₀
have 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₀
Tactic: change MDifferentiableWithinAt IB IB id u b₀ ∧ _ ↔ _
-- 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
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
have 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
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x 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 : 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
⊢ MDiff[a] (T% s) ↔ MDiff[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2
have 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
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
-- 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
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[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) x
have this : MDiffAt (T% s) x
Tactic: have := (h x hx).mdifferentiableAt <| ha.mem_nhds hx
-- 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
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[a] (T% s) x
have this : (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
-- 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
s t : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
ht : MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (s + t) x⟩) x₀
have rw : ∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀)
  (ht : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀),
  (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀
Tactic: rw [mdifferentiableWithinAt_section] at hs ht ⊢
Cleared hypotheses: hs, ht
-- 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
s t : (x : B) → E x
u : Set B
x₀ : B
hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀
have set : let e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀;
∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀)
  (ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀),
  (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀
Tactic: set e := trivializationAt F E x₀
Cleared hypotheses: hs, ht
-- 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
s t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀
have refine_1 : (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) =ᶠ[𝓝[u] x₀]
  HAdd.hAdd (α := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) fun (b : B) ↦
    ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2
Tactic: refine (hs.add ht).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 : 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
s t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
refine_1 :
  (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) =ᶠ[𝓝[u] x₀]
    HAdd.hAdd (α := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) fun (b : B) ↦
      ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀
have refine_2 : ((↑e : TotalSpace F E → B × F) ⟨x₀, (s + t) x₀⟩).2 =
  HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
    (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
Tactic: refine (hs.add ht).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 : 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
s t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) =ᶠ[𝓝[u] x₀]
    HAdd.hAdd (α := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) fun (b : B) ↦
      ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2
have refine_1 : e.baseSet ∈ 𝓝[u] x₀
Tactic: apply eventually_of_mem (U := e.baseSet)