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
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
pos :
  ∀ (hb : b ∈ e.baseSet ∩ e'.baseSet),
    Continuous[inst_1, inst_1]
      (LinearEquiv.invFun
        (if hb : b ∈ e.baseSet ∩ e'.baseSet then
          LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯
        else LinearEquiv.refl R F))
⊢ Continuous[inst_1, inst_1]
    (LinearEquiv.invFun
      (if hb : b ∈ e.baseSet ∩ e'.baseSet then
        LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯
      else LinearEquiv.refl R F))
have neg : ∀ (hb : b ∉ e.baseSet ∩ e'.baseSet),
  Continuous[inst_1, inst_1]
    (LinearEquiv.invFun
      (if hb : b ∈ e.baseSet ∩ e'.baseSet then
        LinearEquiv.symm (linearEquivAt R (E := E) e b sorry) ≪≫ₗ linearEquivAt R (E := E) e' b sorry
      else LinearEquiv.refl R F))
Tactic: by_cases hb : b ∈ e.baseSet ∩ e'.baseSet
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst_1, inst_1]
    (LinearEquiv.invFun
      (if hb : b ∈ e.baseSet ∩ e'.baseSet then
        LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯
      else LinearEquiv.refl R F))
have pos : Continuous[inst_1, inst_1]
  (LinearEquiv.invFun (LinearEquiv.symm (linearEquivAt R (E := E) e b sorry) ≪≫ₗ linearEquivAt R (E := E) e' b sorry))
Tactic: rw [dif_pos 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst_1, inst_1]
    (LinearEquiv.invFun (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))
have pos : Continuous[inst_1, inst_3] fun (x : F) ↦
  TotalSpace.mk (E := E) b
    (((LinearEquiv.toEquiv (modM := inst_7 b) (modM₂ := inst_5) (linearEquivAt R (E := E) e' b sorry)).symm : (a : F) → E b)
      x)
Tactic: refine (e.continuousOn.comp_continuous ?_ ?_).snd
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
pos :
  Continuous[inst_1, inst_3] fun (x : F) ↦
    TotalSpace.mk (E := E) b
      (((LinearEquiv.toEquiv (modM := inst_7 b) (modM₂ := inst_5) (linearEquivAt R (E := E) e' b ⋯)).symm :
          (a : F) → E b)
        x)
⊢ Continuous[inst_1, inst_1]
    (LinearEquiv.invFun (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))
have pos₁ : ∀ (x : F),
  TotalSpace.mk (E := E) b
      (((LinearEquiv.toEquiv (modM := inst_7 b) (modM₂ := inst_5) (linearEquivAt R (E := E) e' b sorry)).symm :
          (a : F) → E b)
        x) ∈
    e.source
Tactic: refine (e.continuousOn.comp_continuous ?_ ?_).snd
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∉ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst_1, inst_1]
    (LinearEquiv.invFun
      (if hb : b ∈ e.baseSet ∩ e'.baseSet then
        LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯
      else LinearEquiv.refl R F))
have neg : Continuous[inst_1, inst_1] (LinearEquiv.invFun (LinearEquiv.refl R F))
Tactic: rw [dif_neg 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ Eq (α := F ≃L[R] F) (ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) (coordChangeL R (E := E) e' e b)
have a : Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
  (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)
Tactic: apply ContinuousLinearEquiv.toLinearEquiv_injective
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)
have a : Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
  (LinearEquiv.symm (linearEquivAt R (E := E) e' b sorry) ≪≫ₗ linearEquivAt R (E := E) e b sorry)
Tactic: rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).toLinearEquiv_symm,
    coe_coordChangeL' e e' hb.symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
a :
  Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
⊢ Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)
have a₁ : Eq (α := F ≃ₗ[R] F) (LinearEquiv.symm (↑(coordChangeL R (E := E) e e' b) : F ≃ₗ[R] F))
  (LinearEquiv.symm (linearEquivAt R (E := E) e' b sorry) ≪≫ₗ linearEquivAt R (E := E) e b sorry)
Tactic: rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).toLinearEquiv_symm,
    coe_coordChangeL' e e' hb.symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
a :
  Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₁ :
  Eq (α := F ≃ₗ[R] F) (LinearEquiv.symm (↑(coordChangeL R (E := E) e e' b) : F ≃ₗ[R] F))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
⊢ Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)
have a₂ : Eq (α := F ≃ₗ[R] F)
  (LinearEquiv.symm (LinearEquiv.symm (linearEquivAt R (E := E) e b sorry) ≪≫ₗ linearEquivAt R (E := E) e' b sorry))
  (LinearEquiv.symm (linearEquivAt R (E := E) e' b sorry) ≪≫ₗ linearEquivAt R (E := E) e b sorry)
Tactic: rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).toLinearEquiv_symm,
    coe_coordChangeL' e e' hb.symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
a :
  Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₁ :
  Eq (α := F ≃ₗ[R] F) (LinearEquiv.symm (↑(coordChangeL R (E := E) e e' b) : F ≃ₗ[R] F))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₂ :
  Eq (α := F ≃ₗ[R] F)
    (LinearEquiv.symm (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
⊢ Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)
have a₃ : Eq (α := F ≃ₗ[R] F)
  (LinearEquiv.symm (linearEquivAt R (E := E) e' b sorry) ≪≫ₗ
    LinearEquiv.symm (LinearEquiv.symm (linearEquivAt R (E := E) e b sorry)))
  (LinearEquiv.symm (linearEquivAt R (E := E) e' b sorry) ≪≫ₗ linearEquivAt R (E := E) e b sorry)
Tactic: rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).toLinearEquiv_symm,
    coe_coordChangeL' e e' hb.symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
a :
  Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₁ :
  Eq (α := F ≃ₗ[R] F) (LinearEquiv.symm (↑(coordChangeL R (E := E) e e' b) : F ≃ₗ[R] F))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₂ :
  Eq (α := F ≃ₗ[R] F)
    (LinearEquiv.symm (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
a₃ :
  Eq (α := F ≃ₗ[R] F)
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ
      LinearEquiv.symm (LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯)))
    (LinearEquiv.symm (linearEquivAt R (E := E) e' b ⋯) ≪≫ₗ linearEquivAt R (E := E) e b ⋯)
⊢ Eq (α := F ≃ₗ[R] F) (↑(ContinuousLinearEquiv.symm (coordChangeL R (E := E) e e' b)) : F ≃ₗ[R] F)
    (↑(coordChangeL R (E := E) e' e b) : F ≃ₗ[R] F)
have a₄ : Eq (α := F ≃ₗ[R] F) (LinearEquiv.symm (linearEquivAt R (E := E) e' b sorry) ≪≫ₗ linearEquivAt R (E := E) e b sorry)
  (LinearEquiv.symm (linearEquivAt R (E := E) e' b sorry) ≪≫ₗ linearEquivAt R (E := E) e b sorry)
Tactic: rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).toLinearEquiv_symm,
    coe_coordChangeL' e e' hb.symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
-- 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))
have fst : ((b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) : B × F).1 =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
fst :
  ((b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).1
⊢ (b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))
have snd : (b, (coordChangeL R (E := E) e e' b : (a : F) → F) y).2 =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ ((b, (coordChangeL R (E := E) e e' b : (a : F) → F) y) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).1
have fst : ((↑e.symm : B × F → TotalSpace F E) (b, y)).proj (E := E) ∈ e'.baseSet
Tactic: rw [e.mk_symm hb.1 y, 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ ((↑e.symm : B × F → TotalSpace F E) (b, y)).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 (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
    (b, (coordChangeL R (E := E) e e' b : (a : F) → F) v)
have rw : (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
  (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))
Tactic: rw [e.mk_coordChangeL e' 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
rw :
  (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))
⊢ (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
    (b, (coordChangeL R (E := E) e e' b : (a : F) → F) v)
have rw₁ : (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v)) =
  (↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, v))
Tactic: rw [e.mk_coordChangeL e' 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (coordChangeL R (E := E) e e' b : (a : F) → F) y =
    ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2
have rw : ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).2 =
  ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2
Tactic: rw [e.coordChangeL_apply e' 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 : Semiring R
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : AddCommMonoid F
inst_5 : Module R F
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_4} R (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
inst_9 : Trivialization.IsLinear R (E := E) e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
rw :
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y))).2 =
    ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2
⊢ (coordChangeL R (E := E) e e' b : (a : F) → F) y =
    ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2
have rw₁ : ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2 =
  ((↑e' : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y))).2
Tactic: rw [e.coordChangeL_apply e' 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 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_9 : Trivialization.IsLinear R (E := E) e
b : B
⊢ Continuous[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(Trivialization.linearMapAt R (E := E) e b) : (a : E b) → F)
have rw : Continuous[inst_7 b, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (y : E b) ↦
  if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
Tactic: rw [e.coe_linearMapAt b]