awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
this : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id e.source
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e : TotalSpace F E → B × F) e.source
have this₁ : ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) e.source ∧
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
    (fun (x : TotalSpace F E) ↦ ((↑e : TotalSpace F E → B × F) (id x)).2) e.source
Tactic: rw [e.contMDiffOn_iff (mapsTo_id _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e.symm : B × F → TotalSpace F E) e.target
have rw : ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : B × F) ↦ ((↑e.symm : B × F → TotalSpace F E) x).proj (E := E))
    e.target ∧
  ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
    (fun (x : B × F) ↦ ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2) e.target
Tactic: rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.symm_mapsTo]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB (M' := B) n (fun (x : B × F) ↦ ((↑e.symm : B × F → TotalSpace F E) x).proj (E := E))
      e.target ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (M' := F) n
      (fun (x : B × F) ↦ ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2) e.target
have refine : ∀ (x : B × F) (hx : x ∈ e.target), ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2 = x.2
Tactic: refine ⟨contMDiffOn_fst.congr fun x hx ↦ e.proj_symm_apply hx,
    contMDiffOn_snd.congr fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
x : B × F
hx : x ∈ e.target
⊢ ((↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) x)).2 = x.2
have rw : x.2 = x.2
Tactic: rw [e.apply_symm_apply hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
      x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
have rw : ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ (TotalSpace.mk' (E := E) F x (s x)).proj (E := E)) a x₀ ∧
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
  ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
Tactic: rw [e.contMDiffWithinAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
rw :
  ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ (TotalSpace.mk' (E := E) F x (s x)).proj (E := E)) a x₀ ∧
      ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
        (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
      x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
have rw₁ : TotalSpace.mk' (E := E) F x₀ (s x₀) ∈ e.source
Tactic: rw [e.contMDiffWithinAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffWithinAt IB IB (M' := B) n (fun (x : B) ↦ (TotalSpace.mk' (E := E) F x (s x)).proj (E := E)) a x₀ ∧
      ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
        (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
have change : ContMDiffWithinAt IB IB n id a x₀ ∧
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk' (E := E) F x (s x))).2) a x₀ ↔
  ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x₀
Tactic: change ContMDiffWithinAt IB IB n id a x₀ ∧ _ ↔ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
hx₀ : x₀ ∈ e.baseSet
⊢ TotalSpace.mk' (E := E) F x₀ (s x₀) ∈ e.source
have rwa : (TotalSpace.mk' (E := E) F x₀ (s x₀)).proj (E := E) ∈ e.baseSet
Tactic: rwa [mem_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
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_4] a
ha' : a ⊆ e.baseSet
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a ↔
    ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a
have refine_1 : ∀ (h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a)
  (x : B) (hx : x ∈ a),
  ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
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_4] a
ha' : a ⊆ e.baseSet
refine_1 :
  ∀ (h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a)
    (x : B) (hx : x ∈ a),
    ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a ↔
    ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a
have refine_2 : ∀
  (h :
    ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n
      (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a)
  (x : B) (hx : x ∈ a),
  ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a x
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
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_4] a
ha' : a ⊆ e.baseSet
h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a
x : B
hx : x ∈ a
⊢ ContMDiffWithinAt IB 𝓘(𝕜, F) (M' := F) n
    (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) a x
have this : ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) x
Tactic: have := (h x hx).contMDiffAt <| ha.mem_nhds hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
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_4] a
ha' : a ⊆ e.baseSet
h :
  ContMDiffOn IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2)
    a
x : B
hx : x ∈ a
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) (M' := TotalSpace F E) n (fun (x : B) ↦ TotalSpace.mk' (E := E) F x (s x)) a x
have this : ContMDiffAt IB 𝓘(𝕜, F) (M' := F) n (fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) x (s x))).2) x
Tactic: have := (h x hx).contMDiffAt <| ha.mem_nhds hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst_20 : Z.IsContMDiff IB n
i i' : ι
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
            (Z.toFiberBundleCore.localTriv i') b) :
        F →L[𝕜] F))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)
have refine : ∀ (b : B) (hb : b ∈ Z.baseSet i ∩ Z.baseSet i'),
  (↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
          b) :
      F →L[𝕜] F) =
    Z.coordChange i i' b
Tactic: refine (Z.contMDiffOn_coordChange IB i i').congr fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst_20 : Z.IsContMDiff IB n
i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
⊢ (↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
          b) :
      F →L[𝕜] F) =
    Z.coordChange i i' b
have h : ∀ (v : F),
  Eq (α := F)
    (((↑(Trivialization.coordChangeL 𝕜 (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                (Z.toFiberBundleCore.localTriv i') b) :
            F →L[𝕜] F) :
          (a : F) → F)
        v :
      F)
    ((Z.coordChange i i' b : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
he : MemTrivializationAtlas (E := Trivial B F) e
he' : MemTrivializationAtlas (E := Trivial B F) e'
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)
have obtain : ∀ [he : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)],
  ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) e' b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ e'.baseSet)
Tactic: obtain rfl := Bundle.Trivial.eq_trivialization B F e
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
e' : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
he' : MemTrivializationAtlas (E := Trivial B F) e'
he : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) e' b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ e'.baseSet)
have obtain : ∀ [he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)],
  ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
Tactic: obtain rfl := Bundle.Trivial.eq_trivialization B F e'
Cleared hypotheses: e', he'