awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : Z.Fiber b
⊢ Eq (α := F) ((Trivialization.continuousLinearMapAt R (E := Z.Fiber) (Z.localTriv i) b : (a : Z.Fiber b) → F) v : F)
    ((Z.coordChange (Z.indexAt b) i b : (a : Z.Fiber b) → F) v : F)
have h : Eq (α := F) ((Z.coordChange (Z.indexAt b) i b : (a : F) → F) v : F)
  ((Z.coordChange (Z.indexAt b) i b : (a : Z.Fiber b) → F) v : F)
Tactic: simp_all
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
⊢ Trivialization.symmL R (E := Z.Fiber) (Z.localTriv i) b = Z.coordChange i (Z.indexAt b) b
have h : ∀ (v : F),
  Eq (α := Z.Fiber b) ((Trivialization.symmL R (E := Z.Fiber) (Z.localTriv i) b : (a : F) → Z.Fiber b) v : Z.Fiber b)
    ((Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v : Z.Fiber b)
Tactic: ext1 v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : F
⊢ Eq (α := Z.Fiber b) ((Trivialization.symmL R (E := Z.Fiber) (Z.localTriv i) b : (a : F) → Z.Fiber b) v : Z.Fiber b)
    ((Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v : Z.Fiber b)
have h : cast sorry (((↑(Z.localTriv i).symm : B × F → TotalSpace F Z.Fiber) (b, v)).snd (E := Z.Fiber)) =
  (Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v
Tactic: rw [(Z.localTriv i).symmL_apply R, (Z.localTriv i).symm_apply]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (b, (a.coordChange (E := E) he he' b : (a : F) → F) v) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))
have fst : ((b, (a.coordChange (E := E) he he' b : (a : F) → F) v) : B × F).1 =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
fst :
  ((b, (a.coordChange (E := E) he he' b : (a : F) → F) v) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1
⊢ (b, (a.coordChange (E := E) he he' b : (a : F) → F) v) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))
have snd : (b, (a.coordChange (E := E) he he' b : (a : F) → F) v).2 =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((b, (a.coordChange (E := E) he he' b : (a : F) → F) v) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1
have fst : ((↑e.symm : B × F → TotalSpace F E) (b, v)).proj (E := E) ∈ e'.baseSet
Tactic: rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((↑e.symm : B × F → TotalSpace F E) (b, v)).proj (E := E) ∈ e'.baseSet
have fst : b ∈ e'.baseSet
Tactic: rw [e.proj_symm_apply' hb.1]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (hypothesis)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
⊢ ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
have this : ContinuousOn (Y := F) (fun (x : B × F) ↦ (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2)
  (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
Tactic: have : ContinuousOn (fun x : B × F ↦ a.coordChange he' he x.1 x.2)
          ((e'.baseSet ∩ e.baseSet) ×ˢ univ) :=
        isBoundedBilinearMap_apply.continuous.comp_continuousOn
          ((a.continuousOn_coordChange he' he).prodMap continuousOn_id)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this :
  ContinuousOn (Y := F) (fun (x : B × F) ↦ (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2)
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
⊢ ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
have rw : ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
  (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
Tactic: rw [e.target_inter_preimage_symm_source_eq e', inter_comm]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this :
  ContinuousOn (Y := F) (fun (x : B × F) ↦ (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2)
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
⊢ ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
have refine : EqOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
  (fun (x : B × F) ↦ (x.1, (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2))
  (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
Tactic: refine (continuousOn_fst.prodMk this).congr ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this :
  ContinuousOn (Y := F) (fun (x : B × F) ↦ (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2)
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
b : B
f : F
hb : (b, f).1 ∈ e'.baseSet ∩ e.baseSet
⊢ ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E)) (b, f) =
    (fun (x : B × F) ↦ ((x.1, (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2) : B × F)) (b, f)
have dsimp : (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
  (b, (a.coordChange (E := E) he' he b : (a : F) → F) f)
Tactic: dsimp only [Function.comp_def, Prod.map]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this :
  ContinuousOn (Y := F) (fun (x : B × F) ↦ (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2)
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
b : B
f : F
hb : (b, f).1 ∈ e'.baseSet ∩ e.baseSet
⊢ (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
    (b, (a.coordChange (E := E) he' he b : (a : F) → F) f)
have rw : (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
  (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) (b, f).1 (e'.symm (E := E) (b, f).1 f))
Tactic: rw [a.mk_coordChange _ _ hb, e'.mk_symm hb.1]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this :
  ContinuousOn (Y := F) (fun (x : B × F) ↦ (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2)
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
b : B
f : F
hb : (b, f).1 ∈ e'.baseSet ∩ e.baseSet
rw :
  (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
    (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) (b, f).1 (e'.symm (E := E) (b, f).1 f))
⊢ (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
    (b, (a.coordChange (E := E) he' he b : (a : F) → F) f)
have rw₁ : (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
  (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) ((b, f).1, f))
Tactic: rw [a.mk_coordChange _ _ hb, e'.mk_symm hb.1]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[R] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL R (E := E)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
        F →L[R] F))
    ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
      (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet)
have refine : ∀ (b : B) (hb : b ∈ e.baseSet ∩ e'.baseSet),
  (↑(Trivialization.coordChangeL R (E := E)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
      F →L[R] F) =
    a.coordChange (E := E) he he' b
Tactic: refine (a.continuousOn_coordChange he he').congr fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ (↑(Trivialization.coordChangeL R (E := E)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
      F →L[R] F) =
    a.coordChange (E := E) he he' b
have h : ∀ (v : F),
  Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (hypothesis)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
have h₁ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)
Tactic: haveI h₁ := a.linear_trivializationOfMemPretrivializationAtlas he
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (hypothesis)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
have h₂ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he')
Tactic: haveI h₂ := a.linear_trivializationOfMemPretrivializationAtlas he'
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (hypothesis)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he')
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
have h₃ : Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
Tactic: rw [trivializationOfMemPretrivializationAtlas] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (hypothesis)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he')
h₃ :
  Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
have h₄ : Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he')
Tactic: rw [trivializationOfMemPretrivializationAtlas] at h₁ h₂
Cleared hypotheses: h₁, h₂