awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
K V : Set X
hK : IsCompact K
hV : IsOpen[inst] V
hKV : K ⊆ V
U : Set X
hU1 : IsOpen[inst] U
hU2 : K ⊆ U
hU3 : closure[inst] U ⊆ V
hU4 : IsCompact (closure[inst] U)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
      IsCompact (X := X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) ∧
        tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have obtain : ∀ (f : C(X, ℝ)) (hf1 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ U)
  (hf2 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 (closure[inst] K))
  (hf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
  ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
      IsCompact (X := X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) ∧
        tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: obtain ⟨f, hf1, hf2, hf3⟩ := exists_tsupport_one_of_isOpen_isClosed hU1 hU4
    isClosed_closure (hK.closure_subset_of_isOpen hU1 hU2)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
K V : Set X
hK : IsCompact K
hV : IsOpen[inst] V
hKV : K ⊆ V
U : Set X
hU1 : IsOpen[inst] U
hU2 : K ⊆ U
hU3 : closure[inst] U ⊆ V
hU4 : IsCompact (closure[inst] U)
f : C(X, ℝ)
hf1 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ U
hf2 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 (closure[inst] K)
hf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
      IsCompact (X := X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) ∧
        tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have hfU : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ closure[inst] U
Tactic: have hfU : tsupport f ⊆ closure U := hf1.trans subset_closure
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
x : X
⊢ ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have rcases : ∀ (k : Set X) (hk : IsCompact k) (k_mem : k ∈ 𝓝 x),
  ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
⊢ ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have rcases : ∀ (f : C(X, ℝ)) (fk : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 k)
  (f_comp : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ))
  (hf : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
  ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rcases exists_continuous_one_zero_of_isCompact hk isClosed_empty (disjoint_empty k)
    with ⟨f, fk, -, f_comp, hf⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 k
f_comp : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)
hf : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have refine : Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: refine ⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 k
f_comp : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)
hf : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have this : Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 x : ℝ)
Tactic: have := fk (mem_of_mem_nhds k_mem)
-- 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
e_1 : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_3 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
⊢ LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)
have refine : IsLinearMap R (e.symm (E := E) b)
Tactic: refine IsLinearMap.mk' (e.symm b) ?_
-- 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
e_1 : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_3 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
⊢ IsLinearMap R (e.symm (E := E) b)
have pos : ∀ (hb : b ∈ e.baseSet), IsLinearMap R (e.symm (E := E) b)
Tactic: by_cases hb : b ∈ 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
e_1 : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_3 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
pos : ∀ (hb : b ∈ e.baseSet), IsLinearMap R (e.symm (E := E) b)
⊢ IsLinearMap R (e.symm (E := E) b)
have neg : ∀ (hb : b ∉ e.baseSet), IsLinearMap R (e.symm (E := E) b)
Tactic: by_cases hb : b ∈ 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
e_1 : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b_1 : B
y : E b_1
inst_3 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
hb : b ∉ e.baseSet
⊢ IsLinearMap R (e.symm (E := E) b)
have neg : IsLinearMap.{u_1, u_3, u_4} R (M := F) (M₂ := E b) 0
Tactic: rw [e.coe_symm_of_notMem 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 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
⊢ Eq (α := (a : E b) → F) (⇑(Pretrivialization.linearMapAt R (E := E) e b) : (a : E b) → F) fun (y : E b) ↦
    if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
have rw : Eq (α := (a : E b) → F)
  (⇑(if hb : b ∈ e.baseSet then (↑(linearEquivAt R (E := E) e b hb) : E b →ₗ[R] F) else 0) : (a : E b) → F)
  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 [Pretrivialization.linearMapAt]
-- 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 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
⊢ Eq (α := (a : E b) → F)
    (⇑(if hb : b ∈ e.baseSet then (↑(linearEquivAt R (E := E) e b hb) : E b →ₗ[R] F) else 0) : (a : E b) → F)
    fun (y : E b) ↦ if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
have pos : ∀ (h : b ∈ e.baseSet),
  Eq (α := (a : E b) → F) (⇑(↑(linearEquivAt R (E := E) e b h) : E b →ₗ[R] F) : (a : E b) → F) fun (y : E b) ↦
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
Tactic: split_ifs
-- 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 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
pos :
  ∀ (h : b ∈ e.baseSet),
    Eq (α := (a : E b) → F) (⇑(↑(linearEquivAt R (E := E) e b h) : E b →ₗ[R] F) : (a : E b) → F) fun (y : E b) ↦
      ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
⊢ Eq (α := (a : E b) → F)
    (⇑(if hb : b ∈ e.baseSet then (↑(linearEquivAt R (E := E) e b hb) : E b →ₗ[R] F) else 0) : (a : E b) → F)
    fun (y : E b) ↦ if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
have neg : b ∉ e.baseSet → Eq (α := (a : E b) → F) (⇑0 : (a : E b) → F) fun (y : E b) ↦ 0
Tactic: split_ifs
-- 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 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
⊢ Eq (α := (a : E b) → F) (⇑(Pretrivialization.linearMapAt R (E := E) e b) : (a : E b) → F) fun (y : E b) ↦
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
have simp_rw : Eq (α := (a : E b) → F)
  (fun (y : E b) ↦ if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0)
  fun (y : E b) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
Tactic: simp_rw [coe_linearMapAt, if_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 : AddCommMonoid F
inst_4 : Module R F
inst_5 : (x : B) → AddCommMonoid (E x)
inst_6 : (x : B) → Module.{u_1, u_4} R (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
y : E b
⊢ (Pretrivialization.linearMapAt R (E := E) e b : (a : E b) → F) y =
    if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
have rw : (fun (y : E b) ↦ if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0) y =
  if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
Tactic: rw [coe_linearMapAt]
-- 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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
⊢ Eq (α := (a : E b) → F) (⇑(Trivialization.linearMapAt R (E := E) e b) : (a : E b) → F) fun (y : E b) ↦
    ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
have simp_rw : Eq (α := (a : E b) → F)
  (fun (y : E b) ↦ if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0)
  fun (y : E b) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2
Tactic: simp_rw [coe_linearMapAt, if_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)
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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
y : E b
⊢ (Trivialization.linearMapAt R (E := E) e b : (a : E b) → F) y =
    if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
have rw : (fun (y : E b) ↦ if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0) y =
  if b ∈ e.baseSet then ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 else 0
Tactic: rw [coe_linearMapAt]
-- 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
⊢ Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[R] F)))
have pos : ∀ (hb : b ∈ e.baseSet ∩ e'.baseSet),
  Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[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
pos :
  ∀ (hb : b ∈ e.baseSet ∩ e'.baseSet),
    Continuous[inst_1, inst_1]
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(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) :
            F →ₗ[R] F)))
⊢ Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[R] F)))
have neg : ∀ (hb : b ∉ e.baseSet ∩ e'.baseSet),
  Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[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]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[R] F)))
have pos : Continuous[inst_1, inst_1]
  (AddHom.toFun
    (LinearMap.toAddHom
      (↑(LinearEquiv.symm (linearEquivAt R (E := E) e b sorry) ≪≫ₗ linearEquivAt R (E := E) e' b sorry) : F →ₗ[R] F)))
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]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯) : F →ₗ[R] F)))
have pos : Continuous[inst_1, inst_3] fun (x : F) ↦
  TotalSpace.mk (E := E) b
    ((((↑(LinearEquiv.symm (linearEquivAt R (E := E) e b sorry)) : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
          LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
        (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.symm (linearEquivAt R (E := E) e b ⋯)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
          (a : F) → E b)
        x)
⊢ Continuous[inst_1, inst_1]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearEquiv.symm (linearEquivAt R (E := E) e b ⋯) ≪≫ₗ linearEquivAt R (E := E) e' b ⋯) : F →ₗ[R] F)))
have pos₁ : ∀ (x : F),
  TotalSpace.mk (E := E) b
      ((((↑(LinearEquiv.symm (linearEquivAt R (E := E) e b sorry)) :
              LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
          (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]
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(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) :
          F →ₗ[R] F)))
have neg : Continuous[inst_1, inst_1] (AddHom.toFun (LinearMap.toAddHom (↑(LinearEquiv.refl R F) : F →ₗ[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)
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
⊢ 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 : ∀ (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