awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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Φ_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
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 (y : B) ↦ (↑(Φ y).symm : F →L[𝕜] F)) U
p : B × F
hp : p ∈ e.source
⊢ (↑e : B × F → B × F) p = (↑(FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU' ⋯ ⋯) : B × F → B × F) p
have hp₁ : p ∈ SProd.sprod (β := Set F) U univ
Tactic: rw [hU] at hp
Cleared hypotheses: 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)
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
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 (y : B) ↦ (↑(Φ y).symm : F →L[𝕜] F)) U
p : B × F
hp : p ∈ SProd.sprod (β := Set F) U univ
⊢ (↑e : B × F → B × F) p = (↑(FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU' ⋯ ⋯) : B × F → B × F) p
have rw : (fun (q : B × F) ↦ ((q.1, (φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) p.1 sorry) q.1 : (a : F) → F) q.2) : B × F)) p =
  (↑(FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU' sorry sorry) : B × F → B × F) p
Tactic: rw [heuφ ⟨p.fst, hp.1⟩ ⟨hux _, hp.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) ⋯ ⋯ ⋯)
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
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 (y : B) ↦ (↑(Φ y).symm : F →L[𝕜] F)) U
p : B × F
hp : p ∈ SProd.sprod (β := Set F) U univ
⊢ (fun (q : B × F) ↦ ((q.1, (φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) p.1 ⋯) q.1 : (a : F) → F) q.2) : B × F)) p =
    (↑(FiberwiseLinear.openPartialHomeomorph (U := U) Φ hU' ⋯ ⋯) : B × F → B × F) p
have congrm : Eq (α := F) ((φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) p.1 sorry) p.1 : (a : F) → F) p.2 : F)
  ((Φ p.1 : (a : F) → F) p.2 : F)
Tactic: congrm (_, ?_)
-- 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Φ_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
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 (y : B) ↦ (↑(Φ y).symm : F →L[𝕜] F)) U
p : B × F
hp : p ∈ SProd.sprod (β := Set F) U univ
⊢ Eq (α := F) ((φ (Subtype.mk (p := fun (x : B) ↦ x ∈ U) p.1 ⋯) p.1 : (a : F) → F) p.2 : F)
    ((Φ p.1 : (a : F) → F) p.2 : F)
have a : p.1 ∈ u (Subtype.mk (p := fun (x : B) ↦ x ∈ U) p.1 sorry)
Tactic: rw [hΦφ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
⊢ ContMDiffOn IB (E' := (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (M' :=
    (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
have h₁ : ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
  (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
Tactic: have h₁ := contMDiffOn_coordChangeL (IB := IB) e₁' e₁ (n := n)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
⊢ ContMDiffOn IB (E' := (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (M' :=
    (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
have h₂ : ContMDiffOn.{u_1, u_8, u_9, u_2, u_4, u_4, u_4} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
  (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
Tactic: have h₂ := contMDiffOn_coordChangeL (IB := IB) e₂ e₂' (n := n)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_4, u_4, u_4} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ ContMDiffOn IB (E' := (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (M' :=
    (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
have refine_1 : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
Tactic: refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_4, u_4, u_4} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
refine_1 : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
⊢ ContMDiffOn IB (E' := (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (M' :=
    (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n
    (continuousLinearMapCoordChange (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
have refine_2 : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
Tactic: refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_4, u_4, u_4} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
have refine_1 : ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
inst_18 : FiberBundle F₁ E₁
inst_19 : VectorBundle 𝕜 F₁ E₁
inst_20 : FiberBundle F₂ E₂
inst_21 : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_22 : ContMDiffVectorBundle n F₁ E₁ IB
inst_23 : ContMDiffVectorBundle n F₂ E₂ IB
inst_24 : MemTrivializationAtlas (E := E₁) e₁
inst_25 : MemTrivializationAtlas (E := E₁) e₁'
inst_26 : MemTrivializationAtlas (E := E₂) e₂
inst_27 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_3, u_3, u_3} IB (E' := F₁ →L[𝕜] F₁) 𝓘(𝕜, F₁ →L[𝕜] F₁) (M' := F₁ →L[𝕜] F₁) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ :
  ContMDiffOn.{u_1, u_8, u_9, u_2, u_4, u_4, u_4} IB (E' := F₂ →L[𝕜] F₂) 𝓘(𝕜, F₂ →L[𝕜] F₂) (M' := F₂ →L[𝕜] F₂) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
refine_1 refine_1₁ refine_1₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
have refine_1₃ : ∀ ⦃my_y : B⦄,
  (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
Tactic: mfld_set_tac