Theorem: Function.tendsto_zero_of_summable (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
hf : Summable f
⊢ Tendsto f cofinite (nhds 0)
Tactic:
obtain ⟨a, ha⟩ := hf
State after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : HasSum f a
⊢ Tendsto f cofinite (nhds 0)

State before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : HasSum f a
⊢ Tendsto f cofinite (nhds 0)
Tactic:
rw [HasSum, tendsto_atTop_nhds] at ha
State after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ Tendsto f cofinite (nhds 0)

State before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ Tendsto f cofinite (nhds 0)
Tactic:
rw [tendsto_nhds]
State after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ ∀ (s : Set α), IsOpen s → 0 ∈ s → f ⁻¹' s ∈ cofinite

State before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ ∀ (s : Set α), IsOpen s → 0 ∈ s → f ⁻¹' s ∈ cofinite
Tactic:
intro U₀ hU₀ memU₀
State after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ f ⁻¹' U₀ ∈ cofinite

State before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
suffices hU₁ : ∃ U₁ : Set α, IsOpen U₁ ∧ (0 : α) ∈ U₁ ∧ U₁ - U₁ ≤ U₀ by
  obtain ⟨U₁, hU₁, memU₁, addU₁_subset⟩ := hU₁
  obtain ⟨S, hS⟩ :=
    ha ((fun x => x - a) ⁻¹' U₁) (by simp only [memU₁, Set.mem_preimage, sub_self])
      (IsOpen.preimage (continuous_sub_right a) hU₁)
  apply S.finite_toSet.subset
  intro i hi
  by_contra his
  apply hi
  apply addU₁_subset
  use (insert i S).sum f - a,
    hS (insert i S) (subset_insert i S),
    S.sum f - a,
    hS S le_rfl
  simp only [sum_insert his, sub_sub_sub_cancel_right, add_sub_cancel_right]
State after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
hU₁ : ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
obtain ⟨U₁, hU₁, memU₁, addU₁_subset⟩ := hU₁
State after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
⊢ f ⁻¹' U₀ ∈ cofinite

State before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
obtain ⟨S, hS⟩ :=
  ha ((fun x => x - a) ⁻¹' U₁) (by simp only [memU₁, Set.mem_preimage, sub_self])
    (IsOpen.preimage (continuous_sub_right a) hU₁)
State after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ f ⁻¹' U₀ ∈ cofinite

State before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
apply S.finite_toSet.subset
State after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ (f ⁻¹' U₀)ᶜ ⊆ ↑S

State before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ (f ⁻¹' U₀)ᶜ ⊆ ↑S
Tactic:
intro i hi
State after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
⊢ i ∈ ↑S

State before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
⊢ i ∈ ↑S
Tactic:
by_contra his
State after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ False
Tactic:
apply hi
State after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ i ∈ f ⁻¹' U₀

State before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ i ∈ f ⁻¹' U₀
Tactic:
apply addU₁_subset
State after:
case intro.intro.intro.intro.a
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ f i ∈ U₁ - U₁

State before:
case intro.intro.intro.intro.a
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ f i ∈ U₁ - U₁
Tactic:
use (insert i S).sum f - a,
  hS (insert i S) (subset_insert i S),
  S.sum f - a,
  hS S le_rfl
State after:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ (fun x x_1 => x - x_1) ((insert i S).sum f - a) (S.sum f - a) = f i

State before:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ (fun x x_1 => x - x_1) ((insert i S).sum f - a) (S.sum f - a) = f i
Tactic:
simp only [sum_insert his, sub_sub_sub_cancel_right, add_sub_cancel_right]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
⊢ a ∈ (fun x => x - a) ⁻¹' U₁
Tactic:
simp only [memU₁, Set.mem_preimage, sub_self]
State after:
no goals

State before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
suffices h_open : IsOpen ((fun xy : α × α => xy.fst - xy.snd) ⁻¹' U₀) by
  rw [isOpen_prod_iff] at h_open
  obtain ⟨u, v, hu, hv, mem_u, mem_v, H⟩ :=
    h_open 0 0 (by simp only [Set.mem_preimage, sub_self, memU₀])
  use u ∩ v, IsOpen.inter hu hv, ⟨mem_u, mem_v⟩
  apply subset_trans _ (Set.image_subset_iff.mpr H)
  rw [image_prod]
  rintro z ⟨x, hx, y, hy, rfl⟩
  exact ⟨x, mem_of_mem_inter_left hx, y, mem_of_mem_inter_right hy, rfl⟩
State after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ IsOpen ((fun xy => xy.1 - xy.2) ⁻¹' U₀)

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open : IsOpen ((fun xy => xy.1 - xy.2) ⁻¹' U₀)
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
rw [isOpen_prod_iff] at h_open
State after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
obtain ⟨u, v, hu, hv, mem_u, mem_v, H⟩ :=
  h_open 0 0 (by simp only [Set.mem_preimage, sub_self, memU₀])
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
use u ∩ v, IsOpen.inter hu hv, ⟨mem_u, mem_v⟩
State after:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ≤ U₀

State before:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ≤ U₀
Tactic:
apply subset_trans _ (Set.image_subset_iff.mpr H)
State after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ (fun xy => xy.1 - xy.2) '' u ×ˢ v

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ (fun xy => xy.1 - xy.2) '' u ×ˢ v
Tactic:
rw [image_prod]
State after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ image2 HSub.hSub u v

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ image2 HSub.hSub u v
Tactic:
rintro z ⟨x, hx, y, hy, rfl⟩
State after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
x : α
hx : x ∈ u ∩ v
y : α
hy : y ∈ u ∩ v
⊢ (fun x x_1 => x - x_1) x y ∈ image2 HSub.hSub u v

State before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
x : α
hx : x ∈ u ∩ v
y : α
hy : y ∈ u ∩ v
⊢ (fun x x_1 => x - x_1) x y ∈ image2 HSub.hSub u v
Tactic:
exact ⟨x, mem_of_mem_inter_left hx, y, mem_of_mem_inter_right hy, rfl⟩
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ (0, 0) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀
Tactic:
simp only [Set.mem_preimage, sub_self, memU₀]
State after:
no goals

State before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ IsOpen ((fun xy => xy.1 - xy.2) ⁻¹' U₀)
Tactic:
exact IsOpen.preimage continuous_sub hU₀
State after:
no goals