-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem tendsto_nhds_iff {α : Type*} {l : Filter α} {f : α → Z} {z : Z} (hz : z ∈ e.source) :
    Tendsto f l (𝓝 z) ↔
      Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (e (f x)).2) l (𝓝 (e z).2)

Proof state:
case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 (f x)).2) l (𝓝 (↑e z).2)

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

Result:
no goals

Proof state:
case pos
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
simp only [hl, and_true]

Result:
case pos
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

Proof state:
case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
rw [e.source_eq] at hl hz

Result:
case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 (f x)).2) l (𝓝 (↑e z).2)

Proof state:
case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

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

Result:
case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ ((Tendsto (fun n => ((↑e ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

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

Result:
case pos
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ Tendsto f l (𝓝 z) ↔ Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e 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]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ ((Tendsto (fun n => ((↑e ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

Proof state:
case pos
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)

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

Result:
case pos
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) =ᶠ[l] proj ∘ f

Proof state:
case pos
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : 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 ∘ f) n).1) =ᶠ[l] proj ∘ f

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

Result:
no goals