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)
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
he : e.source = SProd.sprod (β := Set F) (Prod.fst '' e.source) univ
p : B × F
hp : p ∈ e.source
refine_1 : u (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp) ⊆ Prod.fst '' e.source
⊢ ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ Prod.fst '' e.source) (_ : p.1 ∈ u) (hφ :
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
    (h2φ :
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
    (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
have refine_2 : (e.restr (SProd.sprod (β := Set F) (u (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp)) univ)).EqOnSource
  (FiberwiseLinear.openPartialHomeomorph (U := u (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp))
    (φ (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp)) sorry sorry sorry)
Tactic: refine ⟨φ ⟨p, hp⟩, u ⟨p, hp⟩, hu ⟨p, hp⟩, ?_, hu' _, hφ ⟨p, hp⟩, h2φ ⟨p, hp⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
EB : Type u_4
inst_4 : NormedAddCommGroup EB
inst_5 : NormedSpace 𝕜 EB
HB : Type u_5
inst_6 : TopologicalSpace HB
inst_7 : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
s : (x : (↑e.source : Type (max u_2 u_3))) → Set (B × F)
hs : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : (↑e.source : Type (max u_2 u_3))), (↑x : B × F) ∈ s x
φ : (x : (↑e.source : Type (max u_2 u_3))) → B → F ≃L[𝕜] F
u : (x : (↑e.source : Type (max u_2 u_3))) → Set B
hu : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[inst] (u x)
hφ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x_1 : B) ↦ (↑(φ x x_1) : F →L[𝕜] F)) (u x)
h2φ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x_1 : B) ↦ (↑(φ x x_1).symm : F →L[𝕜] F)) (u x)
heφ :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)
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
he : e.source = SProd.sprod (β := Set F) (Prod.fst '' e.source) univ
p : B × F
hp : p ∈ e.source
⊢ (e.restr (SProd.sprod (β := Set F) (u (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp)) univ)).EqOnSource
    (FiberwiseLinear.openPartialHomeomorph (U := u (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp))
      (φ (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp)) ⋯ ⋯ ⋯)
have refine_2 : (e.restr (s (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp))).EqOnSource
  (FiberwiseLinear.openPartialHomeomorph (U := u (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp))
    (φ (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e.source) p hp)) sorry sorry sorry)
Tactic: rw [← hesu, e.restr_source_inter]
-- 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
h :
  ∀ x ∈ U,
    ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
      ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
        (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
      (h2φ :
      ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
        (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
      (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
⊢ ∃ (Φ : 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)),
  ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ U) (_ : (↑x : B) ∈ u) (hφ :
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
    (h2φ :
    ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
      (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
    (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu sorry sorry)
Tactic: rw [SetCoe.forall'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
EB : Type u_4
inst_4 : NormedAddCommGroup EB
inst_5 : NormedSpace 𝕜 EB
HB : Type u_5
inst_6 : TopologicalSpace HB
inst_7 : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
U : Set B
hU : e.source = SProd.sprod (β := Set F) U univ
h :
  ∀ (x : (↑U : Type u_2)),
    ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ U) (_ : (↑x : B) ∈ u) (hφ :
      ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
        (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
      (h2φ :
      ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
        (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
      (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
⊢ ∃ (Φ : 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 choose! : ∀ (φ : (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) sorry sorry sorry)),
  ∃ (Φ : 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₀ sorry sorry)
Tactic: choose! φ u hu hUu hux hφ h2φ heφ using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
EB : Type u_4
inst_4 : NormedAddCommGroup EB
inst_5 : NormedSpace 𝕜 EB
HB : Type u_5
inst_6 : TopologicalSpace HB
inst_7 : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
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) ⋯ ⋯ ⋯)
x : (↑U : Type u_2)
p : B × F
hp : p ∈ SProd.sprod (β := Set F) (u x) univ
⊢ (↑e : B × F → B × F) p = (fun (q : B × F) ↦ ((q.1, (φ x q.1 : (a : F) → F) q.2) : B × F)) p
have refine : p ∈ (e.restr (SProd.sprod (β := Set F) (u x) univ)).source
Tactic: refine (heφ x).2 ?_
-- 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) ⋯ ⋯ ⋯)
x : (↑U : Type u_2)
p : B × F
hp : p ∈ SProd.sprod (β := Set F) (u x) univ
⊢ p ∈ (e.restr (SProd.sprod (β := Set F) (u x) univ)).source
have rw : p ∈ (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) sorry sorry sorry).source
Tactic: rw [(heφ x).1]
-- 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) ⋯ ⋯ ⋯)
⊢ ∃ (Φ : 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 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)
Tactic: have heuφ : ∀ x : U, EqOn e (fun q => (q.1, φ x q.1 q.2)) (u x ×ˢ univ) := fun x p hp ↦ by
    refine (heφ x).2 ?_
    rw [(heφ x).1]
    exact hp
-- 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)
p p' : (↑U : Type u_2)
y : B
hyp : y ∈ u p
hyp' : y ∈ u p'
⊢ φ p y = φ p' y
have h : ∀ (v : F), Eq (α := F) ((φ p y : (a : F) → F) v : F) ((φ p' y : (a : F) → F) v : F)
Tactic: ext v
-- 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)
p p' : (↑U : Type u_2)
y : B
hyp : y ∈ u p
hyp' : y ∈ u p'
v : F
⊢ Eq (α := F) ((φ p y : (a : F) → F) v : F) ((φ p' y : (a : F) → F) v : F)
have h1 : (↑e : B × F → B × F) (y, v) = (y, (φ p y : (a : F) → F) v)
Tactic: have h1 : e (y, v) = (y, φ p y v) := heuφ _ ⟨(id hyp : (y, v).fst ∈ u p), trivial⟩
-- 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)
p p' : (↑U : Type u_2)
y : B
hyp : y ∈ u p
hyp' : y ∈ u p'
v : F
h1 : (↑e : B × F → B × F) (y, v) = (y, (φ p y : (a : F) → F) v)
⊢ Eq (α := F) ((φ p y : (a : F) → F) v : F) ((φ p' y : (a : F) → F) v : F)
have h2 : (↑e : B × F → B × F) (y, v) = (y, (φ p' y : (a : F) → F) v)
Tactic: have h2 : e (y, v) = (y, φ p' y v) := heuφ _ ⟨(id hyp' : (y, v).fst ∈ u p'), trivial⟩
-- 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)
⊢ ∃ (Φ : 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φ : ∀ (x x' : (↑U : Type u_2)), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
Tactic: have huφ : ∀ (x x' : U) (y : B), y ∈ u x → y ∈ u x' → φ x y = φ x' y := fun p p' y hyp hyp' ↦ by
    ext v
    have h1 : e (y, v) = (y, φ p y v) := heuφ _ ⟨(id hyp : (y, v).fst ∈ u p), trivial⟩
    have h2 : e (y, v) = (y, φ p' y v) := heuφ _ ⟨(id hyp' : (y, v).fst ∈ u p'), trivial⟩
    exact congr_arg Prod.snd (h1.symm.trans h2)