awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h :
  Eq (α := TangentSpace I x)
    ((((cov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) (X x) :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        (Y x) :
      TangentSpace I x)
    ((((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) (X x) :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        (Y x) :
      TangentSpace I x)
⊢ HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
      (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
            (a : TangentSpace I x) → TangentSpace I x)
          (X x) :
        TangentSpace I x)
      (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
            (a : TangentSpace I x) → TangentSpace I x)
          (Y x) :
        TangentSpace I x) =
    mlieBracket I X Y x
have h₁ : HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
      (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
            (a : TangentSpace I x) → TangentSpace I x)
          (X x) :
        TangentSpace I x)
      (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
            (a : TangentSpace I x) → TangentSpace I x)
          (Y x) :
        TangentSpace I x) -
    mlieBracket I X Y x =
  (((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) (X x) :
        TangentSpace I x →L[𝕜] TangentSpace I x) :
      (a : TangentSpace I x) → TangentSpace I x)
    (Y x)
Tactic: rw [cov.torsion_apply hX hY] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x →
      MDiffAt (T% Y) x →
        HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (X x) :
              TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (Y x) :
              TangentSpace I x) =
          mlieBracket I X Y x
⊢ cov.torsion = 0
have mpr : ∀ (x : M) (u v : TangentSpace I x),
  Eq (α := TangentSpace I x)
    ((((cov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
    ((((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
Tactic: ext x u v
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x →
      MDiffAt (T% Y) x →
        HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (X x) :
              TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (Y x) :
              TangentSpace I x) =
          mlieBracket I X Y x
x : M
u v : TangentSpace I x
⊢ Eq (α := TangentSpace I x)
    ((((cov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
    ((((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
have mpr : mlieBracket I (extend E (E := TangentSpace I) u) (extend E (E := TangentSpace I) v) x -
    mlieBracket I (extend E (E := TangentSpace I) u) (extend E (E := TangentSpace I) v) x =
  (((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
        TangentSpace I x →L[𝕜] TangentSpace I x) :
      (a : TangentSpace I x) → TangentSpace I x)
    v
Tactic: rw [torsion_apply_eq_extend, h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x →
      MDiffAt (T% Y) x →
        HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (X x) :
              TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (Y x) :
              TangentSpace I x) =
          mlieBracket I X Y x
x : M
u v : TangentSpace I x
mpr :
  mlieBracket I (extend E (E := TangentSpace I) u) (extend E (E := TangentSpace I) v) x -
      mlieBracket I (extend E (E := TangentSpace I) u) (extend E (E := TangentSpace I) v) x =
    (((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
          TangentSpace I x →L[𝕜] TangentSpace I x) :
        (a : TangentSpace I x) → TangentSpace I x)
      v
⊢ Eq (α := TangentSpace I x)
    ((((cov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
    ((((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
have mpr₁ : (MDiffAt fun (x_1 : M) ↦ ⟨x_1, extend E (E := TangentSpace I) u x_1⟩) x
Tactic: rw [torsion_apply_eq_extend, h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace E
inst_8 : FiniteDimensional 𝕜 E
inst_9 : IsManifold I 2 M
cov : CovariantDerivative.{u_1, u_2, u_3, u_4, u_2, u_2} I (M := M) E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x →
      MDiffAt (T% Y) x →
        HSub.hSub (α := TangentSpace I x) (β := TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) Y x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (X x) :
              TangentSpace I x)
            (((↑cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) X x :
                  (a : TangentSpace I x) → TangentSpace I x)
                (Y x) :
              TangentSpace I x) =
          mlieBracket I X Y x
x : M
u v : TangentSpace I x
mpr :
  mlieBracket I (extend E (E := TangentSpace I) u) (extend E (E := TangentSpace I) v) x -
      mlieBracket I (extend E (E := TangentSpace I) u) (extend E (E := TangentSpace I) v) x =
    (((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
          TangentSpace I x →L[𝕜] TangentSpace I x) :
        (a : TangentSpace I x) → TangentSpace I x)
      v
mpr₁ : (MDiffAt fun (x_1 : M) ↦ ⟨x_1, extend E (E := TangentSpace I) u x_1⟩) x
⊢ Eq (α := TangentSpace I x)
    ((((cov.torsion x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
    ((((0 x : (a : TangentSpace I x) → TangentSpace I x →L[𝕜] TangentSpace I x) u :
            TangentSpace I x →L[𝕜] TangentSpace I x) :
          (a : TangentSpace I x) → TangentSpace I x)
        v :
      TangentSpace I x)
have mpr₂ : (MDiffAt fun (x_1 : M) ↦ ⟨x_1, extend E (E := TangentSpace I) v x_1⟩) x
Tactic: rw [torsion_apply_eq_extend, h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
φ φ' : B → F ≃L[𝕜] F
U U' : Set B
hU : IsOpen[inst] U
hφ : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U
h2φ : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U
hU' : IsOpen[inst] U'
hφ' : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ' x) : F →L[𝕜] F)) U'
h2φ' : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ' x).symm : F →L[𝕜] F)) U'
⊢ ({ toFun := fun (x : B × F) ↦ (x.1, (φ x.1 : (a : F) → F) x.2),
          invFun := fun (x : B × F) ↦ (x.1, ((φ x.1).symm : (a : F) → F) x.2),
          source := SProd.sprod (β := Set F) U univ, target := SProd.sprod (β := Set F) U univ, map_source' := ⋯,
          map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ : OpenPartialHomeomorph (B × F) (B × F) } ≫ₕ
        { toFun := fun (x : B × F) ↦ (x.1, (φ' x.1 : (a : F) → F) x.2),
          invFun := fun (x : B × F) ↦ (x.1, ((φ' x.1).symm : (a : F) → F) x.2),
          source := SProd.sprod (β := Set F) U' univ, target := SProd.sprod (β := Set F) U' univ, map_source' := ⋯,
          map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ : OpenPartialHomeomorph (B × F) (B × F) }).source =
    SProd.sprod (β := Set F) (U ∩ U') univ
have h : ∀ (x : B × F),
  x ∈
      ({ toFun := fun (x : B × F) ↦ (x.1, (φ x.1 : (a : F) → F) x.2),
            invFun := fun (x : B × F) ↦ (x.1, ((φ x.1).symm : (a : F) → F) x.2),
            source := SProd.sprod (β := Set F) U univ, target := SProd.sprod (β := Set F) U univ, map_source' := sorry,
            map_target' := sorry, left_inv' := sorry, right_inv' := sorry, open_source := sorry, open_target := sorry,
            continuousOn_toFun := sorry, continuousOn_invFun := sorry : OpenPartialHomeomorph (B × F) (B × F) } ≫ₕ
          { toFun := fun (x : B × F) ↦ (x.1, (φ' x.1 : (a : F) → F) x.2),
            invFun := fun (x : B × F) ↦ (x.1, ((φ' x.1).symm : (a : F) → F) x.2),
            source := SProd.sprod (β := Set F) U' univ, target := SProd.sprod (β := Set F) U' univ, map_source' := sorry,
            map_target' := sorry, left_inv' := sorry, right_inv' := sorry, open_source := sorry, open_target := sorry,
            continuousOn_toFun := sorry, continuousOn_invFun := sorry : OpenPartialHomeomorph (B × F) (B × F) }).source ↔
    x ∈ SProd.sprod (β := Set F) (U ∩ U') univ
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
φ φ' : B → F ≃L[𝕜] F
U U' : Set B
hU : IsOpen[inst] U
hφ : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) U
h2φ : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) U
hU' : IsOpen[inst] U'
hφ' : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ' x) : F →L[𝕜] F)) U'
h2φ' : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (x : B) ↦ (↑(φ' x).symm : F →L[𝕜] F)) U'
⊢ ({ toFun := fun (x : B × F) ↦ (x.1, (φ x.1 : (a : F) → F) x.2),
          invFun := fun (x : B × F) ↦ (x.1, ((φ x.1).symm : (a : F) → F) x.2),
          source := SProd.sprod (β := Set F) U univ, target := SProd.sprod (β := Set F) U univ, map_source' := ⋯,
          map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ : OpenPartialHomeomorph (B × F) (B × F) } ≫ₕ
        { toFun := fun (x : B × F) ↦ (x.1, (φ' x.1 : (a : F) → F) x.2),
          invFun := fun (x : B × F) ↦ (x.1, ((φ' x.1).symm : (a : F) → F) x.2),
          source := SProd.sprod (β := Set F) U' univ, target := SProd.sprod (β := Set F) U' univ, map_source' := ⋯,
          map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ : OpenPartialHomeomorph (B × F) (B × F) }).target =
    SProd.sprod (β := Set F) (U ∩ U') univ
have h : ∀ (x : B × F),
  x ∈
      ({ toFun := fun (x : B × F) ↦ (x.1, (φ x.1 : (a : F) → F) x.2),
            invFun := fun (x : B × F) ↦ (x.1, ((φ x.1).symm : (a : F) → F) x.2),
            source := SProd.sprod (β := Set F) U univ, target := SProd.sprod (β := Set F) U univ, map_source' := sorry,
            map_target' := sorry, left_inv' := sorry, right_inv' := sorry, open_source := sorry, open_target := sorry,
            continuousOn_toFun := sorry, continuousOn_invFun := sorry : OpenPartialHomeomorph (B × F) (B × F) } ≫ₕ
          { toFun := fun (x : B × F) ↦ (x.1, (φ' x.1 : (a : F) → F) x.2),
            invFun := fun (x : B × F) ↦ (x.1, ((φ' x.1).symm : (a : F) → F) x.2),
            source := SProd.sprod (β := Set F) U' univ, target := SProd.sprod (β := Set F) U' univ, map_source' := sorry,
            map_target' := sorry, left_inv' := sorry, right_inv' := sorry, open_source := sorry, open_target := sorry,
            continuousOn_toFun := sorry, continuousOn_invFun := sorry : OpenPartialHomeomorph (B × F) (B × F) }).target ↔
    x ∈ SProd.sprod (β := Set F) (U ∩ U') univ
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
EB : Type u_4
inst_4 : NormedAddCommGroup EB
inst_5 : NormedSpace 𝕜 EB
HB : Type u_5
inst_6 : TopologicalSpace HB
inst_7 : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
h :
  ∀ p ∈ e.source,
    ∃ (s : Set (B × F)),
      IsOpen[instTopologicalSpaceProd] s ∧
        p ∈ s ∧
          ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (hφ :
            ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
              (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
            (h2φ :
            ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
              (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
            (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
⊢ ∃ (U : Set B),
    e.source = SProd.sprod (β := Set F) U univ ∧
      ∀ x ∈ U,
        ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
          (h2φ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
          (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource
            (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
have h₁ : ∀ (x : (↑e.source : Type (max u_2 u_3))),
  ∃ (s : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] s ∧
      (↑x : B × F) ∈ s ∧
        ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (hφ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
          (h2φ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
          (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu sorry sorry)
Tactic: rw [SetCoe.forall'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
EB : Type u_4
inst_4 : NormedAddCommGroup EB
inst_5 : NormedSpace 𝕜 EB
HB : Type u_5
inst_6 : TopologicalSpace HB
inst_7 : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
s : (x : (↑e.source : Type (max u_2 u_3))) → Set (B × F)
hs : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : (↑e.source : Type (max u_2 u_3))), (↑x : B × F) ∈ s x
φ : (x : (↑e.source : Type (max u_2 u_3))) → B → F ≃L[𝕜] F
u : (x : (↑e.source : Type (max u_2 u_3))) → Set B
hu : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[inst] (u x)
hφ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x_1 : B) ↦ (↑(φ x x_1) : F →L[𝕜] F)) (u x)
h2φ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x_1 : B) ↦ (↑(φ x x_1).symm : F →L[𝕜] F)) (u x)
heφ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
p : (↑e.source : Type (max u_2 u_3))
⊢ e.source ∩ s p = SProd.sprod (β := Set F) (u p) univ
have rw : (e.restr (s p)).source = SProd.sprod (β := Set F) (u p) univ
Tactic: rw [← e.restr_source' (s _) (hs _)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
EB : Type u_4
inst_4 : NormedAddCommGroup EB
inst_5 : NormedSpace 𝕜 EB
HB : Type u_5
inst_6 : TopologicalSpace HB
inst_7 : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
s : (x : (↑e.source : Type (max u_2 u_3))) → Set (B × F)
hs : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : (↑e.source : Type (max u_2 u_3))), (↑x : B × F) ∈ s x
φ : (x : (↑e.source : Type (max u_2 u_3))) → B → F ≃L[𝕜] F
u : (x : (↑e.source : Type (max u_2 u_3))) → Set B
hu : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[inst] (u x)
hφ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x_1 : B) ↦ (↑(φ x x_1) : F →L[𝕜] F)) (u x)
h2φ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x_1 : B) ↦ (↑(φ x x_1).symm : F →L[𝕜] F)) (u x)
heφ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
⊢ ∃ (U : Set B),
    e.source = SProd.sprod (β := Set F) U univ ∧
      ∀ x ∈ U,
        ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
          (h2φ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
          (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource
            (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
have hesu : ∀ (p : (↑e.source : Type (max u_2 u_3))), e.source ∩ s p = SProd.sprod (β := Set F) (u p) univ
Tactic: have hesu : ∀ p : e.source, e.source ∩ s p = u p ×ˢ univ := by
    intro p
    rw [← e.restr_source' (s _) (hs _)]
    exact (heφ p).1