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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
x : (↑U : Type u_2)
y : B
hyu : y ∈ u x
⊢ Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y ⋯) = φ x y

Tactic:
exact iUnionLift_mk ⟨y, hyu⟩ _

Premises used: Set.iUnionLift_mk, 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
⊢ ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y

Tactic:
have hΦφ : ∀ x : U, ∀ y ∈ u x, Φ y = φ x y := by
    intro x y hyu
    refine (hΦ y (hUu x hyu)).trans ?_
    exact iUnionLift_mk ⟨y, hyu⟩ _
-- 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
h :
  ∀ x ∈ U,
    ∃ (u : Set B),
      IsOpen[inst] u ∧
        x ∈ u ∧
          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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) (U ∩ u)
⊢ 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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) U

Tactic:
apply contMDiffOn_of_locally_contMDiffOn

Premises used: contMDiffOn_of_locally_contMDiffOn
-- 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
x : B
hx : x ∈ U
⊢ ∃ (u : Set B),
    IsOpen[inst] u ∧
      x ∈ u ∧
        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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) (U ∩ u)

Tactic:
⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩

Premises used: Subtype.mk, And.intro, Exists.intro
-- 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
x : B
hx : 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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) (U ∩ u (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx))
⊢ ∃ (u : Set B),
    IsOpen[inst] u ∧
      x ∈ u ∧
        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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) (U ∩ u)

Tactic:
refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩
-- 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
x : B
hx : x ∈ U
⊢ 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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) (U ∩ u (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx))

Tactic:
(ContMDiffOn.congr (hφ ⟨x, hx⟩) ?_).mono inter_subset_right

Premises used: Subtype.mk, ContMDiffOn.mono, ContMDiffOn.congr, Set.inter_subset_right
-- 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
x : B
hx : x ∈ U
h :
  ∀ y ∈ u (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx),
    (↑(Φ y) : F →L[𝕜] F) = (↑(φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx) y) : F →L[𝕜] F)
⊢ 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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) (U ∩ u (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx))

Tactic:
refine (ContMDiffOn.congr (hφ ⟨x, hx⟩) ?_).mono inter_subset_right

Premises used: Subtype.mk, ContMDiffOn.mono, ContMDiffOn.congr, Set.inter_subset_right
-- 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
x : B
hx : x ∈ U
y : B
hy : y ∈ u (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx)
h h₁ :
  (↑(φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx) y) : F →L[𝕜] F) =
    (↑(φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx) y) : F →L[𝕜] F)
⊢ (↑(Φ y) : F →L[𝕜] F) = (↑(φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) x hx) y) : F →L[𝕜] F)

Tactic:
rw [hΦφ ⟨x, hx⟩ y hy]

Premises used: 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
⊢ 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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) U

Tactic:
have hΦ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => (Φ y : F →L[𝕜] F)) U := by
    apply contMDiffOn_of_locally_contMDiffOn
    intro x hx
    refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩
    refine (ContMDiffOn.congr (hφ ⟨x, hx⟩) ?_).mono inter_subset_right
    intro y hy
    rw [hΦφ ⟨x, hx⟩ y hy]
-- 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)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
φ : (x : (↑U : Type u_2)) → B → F ≃L[𝕜] F
u : (x : (↑U : Type u_2)) → Set B
hu : ∀ (x : (↑U : Type u_2)), IsOpen[inst] (u x)
hUu : ∀ (x : (↑U : Type u_2)), u x ⊆ U
hux : ∀ (x : (↑U : Type u_2)), (↑x : B) ∈ u x
hφ :
  ∀ (x : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    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 : (↑U : Type u_2)),
    (e.restr (SProd.sprod (β := Set F) (u x) univ)).EqOnSource
      (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
heuφ :
  ∀ (x : (↑U : Type u_2)),
    EqOn (↑e : B × F → B × F) (fun (q : B × F) ↦ (q.1, (φ x q.1 : (a : F) → F) q.2))
      (SProd.sprod (β := Set F) (u x) univ)
huφ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
hU' : IsOpen[inst] U
Φ₀ : (↑U : Type u_2) → F ≃L[𝕜] F :=
  iUnionLift u (fun (x : (↑U : Type u_2)) ↦ φ x ∘ Subtype.val (p := fun (x_1 : B) ↦ x_1 ∈ u x)) huφ U ⋯
Φ : B → F ≃L[𝕜] F :=
  fun (y : B) ↦ if hy : y ∈ U then Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy) else ContinuousLinearEquiv.refl 𝕜 F
hΦ_1 : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
hΦφ : ∀ (x : (↑U : Type u_2)), ∀ y ∈ u x, Φ y = φ x y
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 (y : B) ↦ (↑(Φ y) : F →L[𝕜] F)) U
h :
  ∀ x ∈ U,
    ∃ (u : Set B),
      IsOpen[inst] u ∧
        x ∈ u ∧
          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 (y : B) ↦ (↑(Φ y).symm : F →L[𝕜] F)) (U ∩ u)
⊢ 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 (y : B) ↦ (↑(Φ y).symm : F →L[𝕜] F)) U

Tactic:
apply contMDiffOn_of_locally_contMDiffOn

Premises used: contMDiffOn_of_locally_contMDiffOn