awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ U = ⋃ (i : (↑U : Type u_2)), u i
have h : ∀ (x : B), x ∈ U ↔ Membership.mem (γ := Set B) (⋃ (i : (↑U : Type u_2)), u i) x
Tactic: ext x
-- 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)
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
x : B
⊢ x ∈ U ↔ Membership.mem (γ := Set B) (⋃ (i : (↑U : Type u_2)), u i) x
have h : x ∈ U ↔ ∃ (i : (↑U : Type u_2)), x ∈ u i
Tactic: rw [mem_iUnion]
-- 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)
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
x : B
⊢ x ∈ U ↔ ∃ (i : (↑U : Type u_2)), x ∈ u i
have h : (∃ (i : (↑U : Type u_2)), x ∈ u i) → x ∈ U
Tactic: refine ⟨fun h => ⟨⟨x, h⟩, hux _⟩, ?_⟩
-- 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)
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
⊢ ∃ (Φ : 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.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU₀ ⋯ ⋯)
have hUu' : U = ⋃ (i : (↑U : Type u_2)), u i
Tactic: have hUu' : U = ⋃ i, u i := by
    ext x
    rw [mem_iUnion]
    refine ⟨fun h => ⟨⟨x, h⟩, hux _⟩, ?_⟩
    rintro ⟨x, hx⟩
    exact hUu x hx
-- 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)
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
⊢ IsOpen[inst] U
have rw : IsOpen[inst] (⋃ (i : (↑U : Type u_2)), u i)
Tactic: rw [hUu']
-- 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)
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
⊢ ∃ (Φ : 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.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU₀ ⋯ ⋯)
have hU' : IsOpen[inst] U
Tactic: have hU' : IsOpen U := by
    rw [hUu']
    apply isOpen_iUnion hu
-- 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)
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
⊢ ∃ (Φ : 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.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU₀ ⋯ ⋯)
have hΦ : ∀ (y : B) (hy : y ∈ U), Φ y = Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y hy)
Tactic: have hΦ : ∀ (y) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩ := fun y hy => dif_pos hy
-- 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)
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
⊢ Φ y = φ x y
have refine : Φ₀ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) y sorry) = φ x y
Tactic: refine (hΦ y (hUu x hyu)).trans ?_
-- 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)
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)
⊢ ∃ (Φ : 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.EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU₀ ⋯ ⋯)
have hΦφ : ∀ (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⟩ _
-- 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)
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
have 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)
Tactic: apply contMDiffOn_of_locally_contMDiffOn
-- 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)
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)
have 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))
Tactic: refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩