case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
rcases(𝓝 (1 : G)).exists_antitone_basis with ⟨u, hu, u_anti⟩
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), True → ∃ ia, (True ∧ True) ∧ ∀ (x : G × G), x ∈ u ia.fst ×ˢ u ia.snd → x.fst * x.snd ∈ u ib
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
have :=
  ((hu.prod_nhds hu).tendsto_iff hu).mp
    (by simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G))
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), True → ∃ ia, (True ∧ True) ∧ ∀ (x : G × G), x ∈ u ia.fst ×ˢ u ia.snd → x.fst * x.snd ∈ u ib
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
simp only [and_self_iff, mem_prod, and_imp, Prod.forall, exists_true_left, Prod.exists,
  forall_true_left] at this
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
have event_mul : ∀ n : ℕ, ∀ᶠ m in atTop, u m * u m ⊆ u n := by
  intro n
  rcases this n with ⟨j, k, -, h⟩
  refine' atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => _⟩
  rintro - ⟨a, b, ha, hb, rfl⟩
  exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)
case intro.mk.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
φ : ℕ → ℕ
hφ : ∀ ⦃m n : ℕ⦄, m < n → u (φ n) * u (φ n) ⊆ u (φ m)
φ_anti_basis : HasAntitoneBasis (𝓝 1) (u ∘ φ)
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul
no goals
case intro.mk.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
φ : ℕ → ℕ
hφ : ∀ ⦃m n : ℕ⦄, m < n → u (φ n) * u (φ n) ⊆ u (φ m)
φ_anti_basis : HasAntitoneBasis (𝓝 1) (u ∘ φ)
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
exact ⟨u ∘ φ, φ_anti_basis, fun n => hφ n.lt_succ_self⟩
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
⊢ Tendsto ?m.464910 (𝓝 (1, 1)) (𝓝 1)
simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n : ℕ
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
⊢ ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
intro n
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n : ℕ
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
rcases this n with ⟨j, k, -, h⟩
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
⊢ u m * u m ⊆ u n
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
refine' atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => _⟩
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
a b : G
ha : a ∈ u m
hb : b ∈ u m
⊢ (fun x x_1 => x * x_1) a b ∈ u n
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
⊢ u m * u m ⊆ u n
rintro - ⟨a, b, ha, hb, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
a b : G
ha : a ∈ u m
hb : b ∈ u m
⊢ (fun x x_1 => x * x_1) a b ∈ u n
exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)