awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : proj x ∈ e.baseSet
⊢ ((↑e : Z → B × F) x).1 = proj x

Tactic:
e.coe_fst (e.mem_source.2 ex)

Premises used: Iff.mpr, Bundle.Trivialization.coe_fst, Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ (proj x, ((↑e : Z → B × F) x).2) = (↑e : Z → B × F) x

Tactic:
Prod.ext (e.coe_fst ex).symm rfl

Premises used: Bundle.Trivialization.coe_fst, Prod.ext, Eq.symm, rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : proj x ∈ e.baseSet
⊢ (proj x, ((↑e : Z → B × F) x).2) = (↑e : Z → B × F) x

Tactic:
Prod.ext (e.coe_fst' ex).symm rfl

Premises used: Bundle.Trivialization.coe_fst', Prod.ext, Eq.symm, rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set (B × F)
⊢ e.source ∩ (↑e : Z → B × F) ⁻¹' (e.target ∩ s) = e.source ∩ (↑e : Z → B × F) ⁻¹' s

Tactic:
e.toOpenPartialHomeomorph.source_inter_preimage_target_inter s

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun', Bundle.Trivialization.toOpenPartialHomeomorph, OpenPartialHomeomorph.source_inter_preimage_target_inter
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : OpenPartialHomeomorph Z (B × F)
i : Set B
j : IsOpen[inst] i
k : e.source = proj ⁻¹' i
l : e.target = SProd.sprod (β := Set F) i univ
m : ∀ p ∈ e.source, ((↑e : Z → B × F) p).1 = proj p
x : Z
⊢ (↑{ toOpenPartialHomeomorph := e, baseSet := i, open_baseSet := j, source_eq := k, target_eq := l, proj_toFun := m :
            Trivialization F proj } :
        Z → B × F)
      x =
    (↑e : Z → B × F) x

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : B × F
⊢ x ∈ e.target ↔ x.1 ∈ e.baseSet

Tactic:
e.toPretrivialization.mem_target

Premises used: Bundle.Pretrivialization.mem_target, Set.Mem, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : B × F
hx : x ∈ e.target
⊢ (↑e.symm : B × F → Z) x ∈ e.source

Tactic:
e.toOpenPartialHomeomorph.map_target hx

Premises used: OpenPartialHomeomorph.map_target, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : B × F
hx : x ∈ e.target
⊢ proj ((↑e.symm : B × F → Z) x) = x.1

Tactic:
e.toPretrivialization.proj_symm_apply hx

Premises used: OpenPartialHomeomorph.toFun', Bundle.Pretrivialization.proj_symm_apply, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
b : B
x : F
hx : b ∈ e.baseSet
⊢ proj ((↑e.symm : B × F → Z) (b, x)) = b

Tactic:
e.toPretrivialization.proj_symm_apply' hx

Premises used: OpenPartialHomeomorph.toFun', Bundle.Trivialization.toPretrivialization, Bundle.Pretrivialization.proj_symm_apply'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
inst_3 : Nonempty F
⊢ SurjOn proj e.source e.baseSet

Tactic:
e.toPretrivialization.proj_surjOn_baseSet

Premises used: Bundle.Trivialization.toPretrivialization, Bundle.Pretrivialization.proj_surjOn_baseSet
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : B × F
hx : x ∈ e.target
⊢ (↑e : Z → B × F) ((↑e.symm : B × F → Z) x) = x

Tactic:
e.toOpenPartialHomeomorph.right_inv hx

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun', Bundle.Trivialization.toOpenPartialHomeomorph, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
b : B
x : F
hx : b ∈ e.baseSet
⊢ (↑e : Z → B × F) ((↑e.symm : B × F → Z) (b, x)) = (b, x)

Tactic:
e.toPretrivialization.apply_symm_apply' hx

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun', Bundle.Pretrivialization.toFun', Bundle.Pretrivialization.apply_symm_apply', Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ (↑e.symm : B × F → Z) (proj x, ((↑e : Z → B × F) x).2) = x

Tactic:
e.toPretrivialization.symm_apply_mk_proj ex

Premises used: OpenPartialHomeomorph.toFun', Bundle.Pretrivialization.symm_apply_mk_proj, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e e' : Trivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ

Tactic:
Pretrivialization.symm_trans_source_eq e.toPretrivialization e'

Premises used: Bundle.Pretrivialization.symm_trans_source_eq, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e e' : Trivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).target = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ

Tactic:
Pretrivialization.symm_trans_target_eq e.toPretrivialization e'

Premises used: Bundle.Pretrivialization.symm_trans_target_eq, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ Prod.fst ∘ (↑e : Z → B × F) =ᶠ[𝓝 x] proj

Tactic:
mem_nhds_iff.2 ⟨e.source, fun _y hy => e.coe_fst hy, e.open_source, ex⟩

Premises used: Iff.mpr, Bundle.Trivialization.coe_fst, OpenPartialHomeomorph.open_source, mem_nhds_iff, Filter.Eventually, Filter.EventuallyEq, And.intro, Exists.intro, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : proj x ∈ e.baseSet
⊢ Prod.fst ∘ (↑e : Z → B × F) =ᶠ[𝓝 x] proj

Tactic:
e.coe_fst_eventuallyEq_proj (e.mem_source.2 ex)

Premises used: Iff.mpr, Bundle.Trivialization.mem_source, Bundle.Trivialization.coe_fst_eventuallyEq_proj
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
rw : map proj (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₁ : map (Prod.fst ∘ (↑e : Z → B × F)) (𝓝 x) = 𝓝 ((↑e : Z → B × F) x).1
rw₂ : map Prod.fst (map (↑e : Z → B × F) (𝓝 x)) = 𝓝 ((↑e : Z → B × F) x).1
rw₃ :
  map Prod.fst (map (↑e.toOpenPartialHomeomorph : Z → B × F) (𝓝 x)) = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
rw₄ : map Prod.fst (𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x)) = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
rw₅ rw₆ : 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1 = 𝓝 ((↑e.toOpenPartialHomeomorph : Z → B × F) x).1
⊢ map proj (𝓝 x) = 𝓝 (proj x)

Tactic:
rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]

Premises used: Bundle.Trivialization.coe_fst, Filter.map_congr, Filter.map_map, Bundle.Trivialization.coe_coe, map_fst_nhds, OpenPartialHomeomorph.map_nhds_eq, Bundle.Trivialization.coe_fst_eventuallyEq_proj, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
hb : s ⊆ e.baseSet
⊢ proj ⁻¹' s ⊆ e.source

Tactic:
fun _p hp => e.mem_source.mpr (hb hp)

Premises used: Iff.mpr, Set.Subset, Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
hb : s ⊆ e.baseSet
⊢ (↑e : Z → B × F) '' proj ⁻¹' s = SProd.sprod (β := Set F) s univ

Tactic:
Subset.antisymm
    (image_subset_iff.mpr fun p hp =>
      ⟨(e.proj_toFun p (e.preimage_subset_source hb hp)).symm ▸ hp, trivial⟩)
    fun p hp =>
    let hp' : p ∈ e.target := e.mem_target.mpr (hb hp.1)
    ⟨e.invFun p, mem_preimage.mpr ((e.proj_symm_apply hp').symm ▸ hp.1), e.apply_symm_apply hp'⟩

Premises used: Set.Subset.antisymm, Iff.mpr, trivial, Bundle.Trivialization.apply_symm_apply, Eq.rec, And.left, And.intro, Bundle.Trivialization.proj_symm_apply, Exists.intro, Bundle.Trivialization.preimage_subset_source, Set.image_subset_iff, PartialEquiv.invFun, OpenPartialHomeomorph.toPartialEquiv, Eq.symm, Bundle.Trivialization.mem_target, Set.mem_preimage, Bundle.Trivialization.toOpenPartialHomeomorph, Bundle.Trivialization.proj_toFun
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
rw :
  ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
⊢ Tendsto f l (𝓝 z) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
rw [e.nhds_eq_comap_inf_principal hz, tendsto_inf, tendsto_comap_iff, Prod.tendsto_iff, coe_coe,
    tendsto_principal, coe_fst _ hz]

Premises used: Filter.tendsto_inf, Bundle.Trivialization.coe_fst, Prod.tendsto_iff, Filter.tendsto_comap_iff, Filter.tendsto_principal, Bundle.Trivialization.coe_coe, OpenPartialHomeomorph.nhds_eq_comap_inf_principal, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
pos :
  ∀ (hl : ∀ᶠ (x : α) in l, f x ∈ e.source),
    ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
          Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
        ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
      Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧
        Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
neg :
  ∀ (hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source),
    ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
          Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
        ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
      Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧
        Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
⊢ ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
by_cases hl : ∀ᶠ x in l, f x ∈ e.source

Premises used: PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ∀ᶠ (x : α) in l, f x ∈ e.source
pos :
  Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
      Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
⊢ ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
simp only [hl, and_true]

Premises used: and_true
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ∀ᶠ (x : α) in l, f x ∈ e.source
⊢ Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
      Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
(tendsto_congr' ?_).and Iff.rfl

Premises used: Iff.rfl, Iff.and, Filter.tendsto_congr'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ∀ᶠ (x : α) in l, f x ∈ e.source
pos : (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) =ᶠ[l] proj ∘ f
⊢ Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
      Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
refine (tendsto_congr' ?_).and Iff.rfl

Premises used: Iff.rfl, Iff.and, Filter.tendsto_congr'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ∀ᶠ (x : α) in l, f x ∈ e.source
⊢ (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) =ᶠ[l] proj ∘ f

Tactic:
hl.mono fun x ↦ e.coe_fst

Premises used: Bundle.Trivialization.coe_fst, Filter.EventuallyEq, Filter.Eventually.mono
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ∀ᶠ (x : α) in l, f x ∈ e.source
⊢ (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) =ᶠ[l] proj ∘ f

Tactic:
exact hl.mono fun x ↦ e.coe_fst

Premises used: Bundle.Trivialization.coe_fst, Filter.Eventually.mono
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
neg :
  Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)
⊢ ((Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).1) l (𝓝 (proj z)) ∧
        Tendsto (fun (n : α) ↦ (((↑e : Z → B × F) ∘ f) n).2) l (𝓝 ((↑e : Z → B × F) z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
simp only [hl, and_false, false_iff, not_and]

Premises used: false_iff, and_false, not_and
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
⊢ z ∈ proj ⁻¹' e.baseSet

Tactic:
rw [e.source_eq] at hl hz

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
hz₁ : z ∈ proj ⁻¹' e.baseSet
⊢ ¬∀ᶠ (x : α) in l, f x ∈ proj ⁻¹' e.baseSet

Tactic:
rw [e.source_eq] at hl hz

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ proj ⁻¹' e.baseSet
hl : ¬∀ᶠ (x : α) in l, f x ∈ proj ⁻¹' e.baseSet
⊢ Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
fun h _ ↦ hl <| h <| e.open_baseSet.mem_nhds hz

Premises used: Bundle.Trivialization.open_baseSet, IsOpen.mem_nhds, Not
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ proj ⁻¹' e.baseSet
hl : ¬∀ᶠ (x : α) in l, f x ∈ proj ⁻¹' e.baseSet
⊢ Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun (x : α) ↦ ((↑e : Z → B × F) (f x)).2) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
exact fun h _ ↦ hl <| h <| e.open_baseSet.mem_nhds hz
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
⊢ 𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ (↑e : Z → B × F)) (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
eq_of_forall_le_iff fun l ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
refine :
  ∀ (l : Filter Z),
    l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ (↑e : Z → B × F)) (𝓝 ((↑e : Z → B × F) z).2)
⊢ 𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ (↑e : Z → B × F)) (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
refine eq_of_forall_le_iff fun l ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
rw : l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ (↑e : Z → B × F)) l (𝓝 ((↑e : Z → B × F) z).2)
⊢ l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ (↑e : Z → B × F)) (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
rw [le_inf_iff, ← tendsto_iff_comap, ← tendsto_iff_comap]

Premises used: Filter.tendsto_iff_comap, le_inf_iff
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ (↑e : Z → B × F)) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
e.tendsto_nhds_iff hz

Premises used: Set.Mem, setOf, Bundle.Trivialization.tendsto_nhds_iff, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ (↑e : Z → B × F)) l (𝓝 ((↑e : Z → B × F) z).2)

Tactic:
exact e.tendsto_nhds_iff hz

Premises used: Bundle.Trivialization.tendsto_nhds_iff
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
hb : s ⊆ e.baseSet
p : (↑(proj ⁻¹' s) : Type u_4)
⊢ (e.preimageHomeomorph (s := s) hb : (a : (↑(proj ⁻¹' s) : Type u_4)) → (↑s : Type u_1) × F) p =
    (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑p : Z)) ⋯, ((↑e : Z → B × F) (↑p : Z)).2)

Tactic:
Prod.ext (Subtype.ext (e.proj_toFun p (e.mem_source.mpr (hb p.2)))) rfl

Premises used: Iff.mpr, Bundle.Trivialization.mem_source, Prod.ext, Subtype.val, rfl, Subtype.property, Bundle.Trivialization.proj_toFun, Subtype.ext
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
hb : s ⊆ e.baseSet
p : Prod.{u_1, u_2} (↑s : Type u_1) F
⊢ Eq.{u_4 + 1} (α := (↑(proj ⁻¹' s) : Type u_4))
    (((e.preimageHomeomorph (s := s) hb).symm : (a : (↑s : Type u_1) × F) → (↑(proj ⁻¹' s) : Type u_4)) p :
      (↑(proj ⁻¹' s) : Type u_4))
    (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ((↑e.symm : B × F → Z) ((↑p.1 : B), p.2)) ⋯ :
      { x : Z // x ∈ proj ⁻¹' s })

Tactic:
rfl

Premises used: Subtype.map, Set.MapsTo.restrict, rfl