awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
mpr₂ : (MDiffAt fun (x_1 : M) ↦ ⟨x_1, extend E (E := TangentSpace I) v 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)

Tactic:
rw [torsion_apply_eq_extend, h]

Premises used: CovariantDerivative.torsion_apply_eq_extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
⊢ 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:
simp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
⊢ (MDiffAt fun (x_1 : M) ↦ ⟨x_1, extend E (E := TangentSpace I) u x_1⟩) x

Tactic:
apply mdifferentiableAt_extend

Premises used: FiberBundle.mdifferentiableAt_extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
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
⊢ (MDiffAt fun (x_1 : M) ↦ ⟨x_1, extend E (E := TangentSpace I) v x_1⟩) x

Tactic:
apply mdifferentiableAt_extend

Premises used: FiberBundle.mdifferentiableAt_extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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'
b : B
v : F
⊢ (↑(openPartialHomeomorph (U := U) φ hU hφ h2φ ≫ₕ openPartialHomeomorph (U := U') φ' hU' hφ' h2φ') : B × F → B × F)
      (b, v) =
    (b, (φ' b : (a : F) → F) ((φ b : (a : F) → F) v : F))

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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'
h h₁ h₂ h₃ :
  ∀ (my_y : B × F),
    my_y ∈
        ({ 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 ↔
      my_y ∈ SProd.sprod (β := Set F) (U ∩ U') univ
⊢ ({ 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

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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'
h h₁ h₂ h₃ :
  ∀ (my_y : B × F),
    my_y ∈
        ({ 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 ↔
      my_y ∈ SProd.sprod (β := Set F) (U ∩ U') univ
⊢ ({ 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

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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 ⋯ ⋯)
⊢ ∀ (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 ⋯ ⋯)

Tactic:
rw [SetCoe.forall'] at h

Premises used: SetCoe.forall'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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))
rw : (e.restr (s p)).source = SProd.sprod (β := Set F) (u p) univ
⊢ e.source ∩ s p = SProd.sprod (β := Set F) (u p) univ

Tactic:
rw [← e.restr_source' (s _) (hs _)]

Premises used: OpenPartialHomeomorph.restr_source'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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.restr (s p)).source = SProd.sprod (β := Set F) (u p) univ

Tactic:
(heφ p).1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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.restr (s p)).source = SProd.sprod (β := Set F) (u p) univ

Tactic:
exact (heφ p).1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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

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
-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
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) ⋯ ⋯ ⋯)
hesu : ∀ (p : (↑e.source : Type (max u_2 u_3))), e.source ∩ s p = SProd.sprod (β := Set F) (u p) univ
p : (↑e.source : Type (max u_2 u_3))
⊢ (↑p : B × F) ∈ e.source ∩ s p

Tactic:
have : (p : B × F) ∈ e.source ∩ s p := ⟨p.prop, hsp p⟩