awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)

Tactic:
⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
refine : Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
      LE.le (α := (a : X) → ℝ) 0 (⇑f : (a : X) → ℝ) ∧ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
refine ⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
⊢ Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 x : ℝ)

Tactic:
have := fk (mem_of_mem_nhds k_mem)
-- Module: Mathlib.Topology.UrysohnsLemma
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 : ℝ)
this : Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
⊢ Ne (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp [this]
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
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)
inst_7 : Pretrivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
⊢ IsLinearMap.{u_1, u_4, u_3} R (M₂ := F) fun (x : E b) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b x)).2

Tactic:
IsLinear.linear b hb

Premises used: Bundle.Pretrivialization.IsLinear.linear
-- Module: Mathlib.Topology.VectorBundle.Basic
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
refine : IsLinearMap R (e.symm (E := E) b)
⊢ LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)

Tactic:
refine IsLinearMap.mk' (e.symm b) ?_

Premises used: Bundle.Pretrivialization.symm, IsLinearMap.mk'
-- Module: Mathlib.Topology.VectorBundle.Basic
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)
neg : ∀ (hb : b ∉ e.baseSet), IsLinearMap R (e.symm (E := E) b)
⊢ IsLinearMap R (e.symm (E := E) b)

Tactic:
by_cases hb : b ∈ e.baseSet

Premises used: Bundle.Pretrivialization.baseSet
-- Module: Mathlib.Topology.VectorBundle.Basic
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)

Tactic:
(((e.linear R hb).mk' _).inverse (e.symm b) (e.symm_apply_apply_mk hb) fun v ↦
      congr_arg Prod.snd <| e.apply_mk_symm hb v).isLinear

Premises used: Bundle.Pretrivialization.apply_mk_symm, dite, congr_arg, LinearMap.isLinear, Bundle.Pretrivialization.symm, LinearMap.inverse, Bundle.Pretrivialization.symm_apply_apply_mk, IsLinearMap.mk', Prod.snd, Bundle.Pretrivialization.linear
-- Module: Mathlib.Topology.VectorBundle.Basic
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)

Tactic:
exact (((e.linear R hb).mk' _).inverse (e.symm b) (e.symm_apply_apply_mk hb) fun v ↦
      congr_arg Prod.snd <| e.apply_mk_symm hb v).isLinear

Premises used: Bundle.Pretrivialization.apply_mk_symm, congr_arg, LinearMap.isLinear, Bundle.Pretrivialization.symm, LinearMap.inverse, Bundle.Pretrivialization.symm_apply_apply_mk, IsLinearMap.mk', Prod.snd, Bundle.Pretrivialization.linear
-- Module: Mathlib.Topology.VectorBundle.Basic
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
neg : IsLinearMap.{u_1, u_3, u_4} R (M := F) (M₂ := E b) 0
⊢ IsLinearMap R (e.symm (E := E) b)

Tactic:
rw [e.coe_symm_of_notMem hb]

Premises used: Bundle.Pretrivialization.coe_symm_of_notMem
-- Module: Mathlib.Topology.VectorBundle.Basic
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.{u_1, u_3, u_4} R (M := F) (M₂ := E b) 0

Tactic:
(0 : F →ₗ[R] E b).isLinear

Premises used: LinearMap.isLinear, OfNat.ofNat
-- Module: Mathlib.Topology.VectorBundle.Basic
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.{u_1, u_3, u_4} R (M := F) (M₂ := E b) 0

Tactic:
exact (0 : F →ₗ[R] E b).isLinear

Premises used: LinearMap.isLinear, OfNat.ofNat
-- Module: Mathlib.Topology.VectorBundle.Basic
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
v : F
simp_rw simp_rw₁ : ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2 = v
⊢ (fun (y : E b) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2) (e.symm (E := E) b v) = v

Tactic:
simp_rw [e.apply_mk_symm hb v]

Premises used: Bundle.Pretrivialization.apply_mk_symm
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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
⊢ 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

Tactic:
rw [Pretrivialization.linearMapAt]

Premises used: Bundle.Pretrivialization.linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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
neg : b ∉ e.baseSet → Eq (α := (a : E b) → F) (⇑0 : (a : E b) → F) fun (y : E b) ↦ 0
⊢ 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:
split_ifs
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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:
rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
h : b ∉ e.baseSet
⊢ Eq (α := (a : E b) → F) (⇑0 : (a : E b) → F) fun (y : E b) ↦ 0

Tactic:
rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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
⊢ 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

Tactic:
simp_rw [coe_linearMapAt, if_pos hb]

Premises used: if_pos, Bundle.Pretrivialization.coe_linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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
rw 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
⊢ (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

Tactic:
rw [coe_linearMapAt]

Premises used: Bundle.Pretrivialization.coe_linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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 (α := LinearMap.{u_1, u_1, u_4, u_3} (RingHom.id R) (E b) F) (Pretrivialization.linearMapAt R (E := E) e b)
    (↑(linearEquivAt R (E := E) e b hb) : E b →ₗ[R] F)

Tactic:
dif_pos hb

Premises used: dif_pos, Bundle.Pretrivialization.linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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 (α := LinearMap.{u_1, u_1, u_4, u_3} (RingHom.id R) (E b) F) (Pretrivialization.linearMapAt R (E := E) e b) 0

Tactic:
dif_neg hb

Premises used: dif_neg, Bundle.Pretrivialization.linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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
y : E b
⊢ ((Pretrivialization.symmₗ R (E := E) e b : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) : (a : F) → E b)
      ((Pretrivialization.linearMapAt R (E := E) e b : (a : E b) → F) y) =
    y

Tactic:
simp [hb]
-- Module: Mathlib.Topology.VectorBundle.Basic
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
y : F
⊢ (Pretrivialization.linearMapAt R (E := E) e b : (a : E b) → F)
      (((Pretrivialization.symmₗ R (E := E) e b : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
            (a : F) → E b)
          y :
        E b) =
    y

Tactic:
simp [hb]
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := 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)
inst_8 : Trivialization.IsLinear R (E := E) e
b : B
hb : b ∈ e.baseSet
⊢ IsLinearMap.{u_1, u_4, u_3} R (M₂ := F) fun (y : E b) ↦ ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2

Tactic:
Trivialization.IsLinear.linear b hb

Premises used: Bundle.Trivialization.IsLinear.linear
-- Module: Mathlib.Topology.VectorBundle.Basic
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 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
b : B
y : E b
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)
inst_8 : Trivialization.IsLinear R (E := E) e
⊢ Pretrivialization.IsLinear R (E := E) e.toPretrivialization

Tactic:
{ (‹_› : e.IsLinear R) with }

Premises used: Bundle.Pretrivialization.IsLinear.mk, Bundle.Trivialization.IsLinear.linear
-- Module: Mathlib.Topology.VectorBundle.Basic
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
v : E b
⊢ (linearEquivAt R (E := E) e b hb : (a : E b) → F) v = ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b v)).2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
v : F
⊢ ((LinearEquiv.symm (linearEquivAt R (E := E) e b hb) : LinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id R) F (E b)) :
        (a : F) → E b)
      v =
    e.symm (E := E) b v

Tactic:
rfl

Premises used: Bundle.Trivialization.symm, dite, Bundle.Pretrivialization.symm, rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ (⇑(Trivialization.symmₗ R (E := E) e b) : (a : F) → E b) = e.symm (E := E) b

Tactic:
rfl

Premises used: Bundle.Trivialization.symm, dite, Bundle.Pretrivialization.symm, rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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
⊢ Eq (α := (a : E b) → F) (⇑(Trivialization.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

Tactic:
e.toPretrivialization.coe_linearMapAt b

Premises used: Set.Mem, Bundle.Trivialization.toPretrivialization, Bundle.Pretrivialization.coe_linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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
⊢ 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

Tactic:
simp_rw [coe_linearMapAt, if_pos hb]

Premises used: if_pos, Bundle.Trivialization.coe_linearMapAt
-- Module: Mathlib.Topology.VectorBundle.Basic
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
rw 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
⊢ (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

Tactic:
rw [coe_linearMapAt]

Premises used: Bundle.Trivialization.coe_linearMapAt