awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
this : (↑p : B × F) ∈ e.source ∩ s p
⊢ (↑p : B × F).1 ∈ u p

Tactic:
simpa only [hesu, mem_prod, mem_univ, and_true] using this

Premises used: and_true, Set.mem_prod, Set.mem_univ
-- 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).1 ∈ u p

Tactic:
have hu' : ∀ p : e.source, (p : B × F).fst ∈ u p := by
    intro p
    have : (p : B × F) ∈ e.source ∩ s p := ⟨p.prop, hsp p⟩
    simpa only [hesu, mem_prod, mem_univ, and_true] using this
-- 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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
p : (↑e.source : Type (max u_2 u_3))
q : B × F
hq : q.1 ∈ u p
⊢ q ∈ SProd.sprod (β := Set F) (u p) univ

Tactic:
have : q ∈ u p ×ˢ (univ : Set F) := ⟨hq, trivial⟩
-- 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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
p : (↑e.source : Type (max u_2 u_3))
q : B × F
hq : q.1 ∈ u p
this : q ∈ SProd.sprod (β := Set F) (u p) univ
⊢ q ∈ e.source ∩ s p

Tactic:
rw [← hesu p] at this
-- 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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
p : (↑e.source : Type (max u_2 u_3))
q : B × F
hq : q.1 ∈ u p
this : q ∈ e.source ∩ s p
⊢ q ∈ e.source

Tactic:
this.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) ⋯ ⋯ ⋯)
hesu : ∀ (p : (↑e.source : Type (max u_2 u_3))), e.source ∩ s p = SProd.sprod (β := Set F) (u p) univ
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
p : (↑e.source : Type (max u_2 u_3))
q : B × F
hq : q.1 ∈ u p
this : q ∈ e.source ∩ s p
⊢ q ∈ e.source

Tactic:
exact this.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) ⋯ ⋯ ⋯)
hesu : ∀ (p : (↑e.source : Type (max u_2 u_3))), e.source ∩ s p = SProd.sprod (β := Set F) (u p) univ
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
⊢ ∀ (p : (↑e.source : Type (max u_2 u_3))) (q : B × F), q.1 ∈ u p → q ∈ e.source

Tactic:
have heu : ∀ p : e.source, ∀ q : B × F, q.fst ∈ u p → q ∈ e.source := by
    intro p q hq
    have : q ∈ u p ×ˢ (univ : Set F) := ⟨hq, trivial⟩
    rw [← hesu p] at this
    exact this.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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
heu : ∀ (p : (↑e.source : Type (max u_2 u_3))) (q : B × F), q.1 ∈ u p → q ∈ e.source
a : e.source ⊆ SProd.sprod (β := Set F) (Prod.fst '' e.source) univ
a₁ : SProd.sprod (β := Set F) (Prod.fst '' e.source) univ ⊆ e.source
⊢ e.source = SProd.sprod (β := Set F) (Prod.fst '' e.source) univ

Tactic:
apply HasSubset.Subset.antisymm

Premises used: HasSubset.Subset.antisymm
-- 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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
heu : ∀ (p : (↑e.source : Type (max u_2 u_3))) (q : B × F), q.1 ∈ u p → q ∈ e.source
p : B × F
hp : p ∈ e.source
⊢ p ∈ SProd.sprod (β := Set F) (Prod.fst '' e.source) univ

Tactic:
⟨⟨p, hp, rfl⟩, trivial⟩

Premises used: trivial, Set.Mem, setOf, Set.prod, And.intro, Exists.intro, 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
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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
heu : ∀ (p : (↑e.source : Type (max u_2 u_3))) (q : B × F), q.1 ∈ u p → q ∈ e.source
p : B × F
hp : p ∈ e.source
⊢ p ∈ SProd.sprod (β := Set F) (Prod.fst '' e.source) univ

Tactic:
exact ⟨⟨p, hp, rfl⟩, trivial⟩
-- 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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
heu : ∀ (p : (↑e.source : Type (max u_2 u_3))) (q : B × F), q.1 ∈ u p → q ∈ e.source
v : F
p : B × F
hp : p ∈ e.source
⊢ (p.1, v) ∈ e.source

Tactic:
heu ⟨p, hp⟩ (p.fst, v) (hu' ⟨p, hp⟩)

Premises used: Prod.mk, Prod.fst, Subtype.mk
-- 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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
heu : ∀ (p : (↑e.source : Type (max u_2 u_3))) (q : B × F), q.1 ∈ u p → q ∈ e.source
v : F
p : B × F
hp : p ∈ e.source
⊢ (p.1, v) ∈ e.source

Tactic:
exact heu ⟨p, hp⟩ (p.fst, v) (hu' ⟨p, hp⟩)

Premises used: Prod.mk, Prod.fst, Subtype.mk
-- 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
hu' : ∀ (p : (↑e.source : Type (max u_2 u_3))), (↑p : B × F).1 ∈ u p
heu : ∀ (p : (↑e.source : Type (max u_2 u_3))) (q : B × F), q.1 ∈ u p → q ∈ e.source
⊢ e.source = SProd.sprod (β := Set F) (Prod.fst '' e.source) univ

Tactic:
have he : e.source = (Prod.fst '' e.source) ×ˢ (univ : Set F) := by
    apply HasSubset.Subset.antisymm
    · intro p hp
      exact ⟨⟨p, hp, rfl⟩, trivial⟩
    · rintro ⟨x, v⟩ ⟨⟨p, hp, rfl : p.fst = x⟩, -⟩
      exact heu ⟨p, hp⟩ (p.fst, v) (hu' ⟨p, hp⟩)