mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ (if L.HasSupport ∧ ∅.Finite then ∏ᶠ (x : β), 1 else if HasProd (fun x ↦ 1) 1 L then 1 else Exists.choose ⋯) = 1

Tactic:
finprod_one,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ (if L.HasSupport ∧ ∅.Finite then 1 else if HasProd (fun x ↦ 1) 1 L then 1 else Exists.choose ⋯) = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : Fintype β
f : β → α
⊢ ∀ b ∉ univ, f b = 1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : Fintype β
f : β → α
⊢ ∀ b ∉ univ, f b = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a b' else 1) = 1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a b' else 1) = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
hb' : b' ≠ b
⊢ (if b = b' then a b' else 1) = 1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
hb' : b' ≠ b
⊢ (if b = b' then a b' else 1) = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↥s), f ↑x = ∏ x ∈ s.attach, f ↑x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↥s), f ↑x = ∏ x ∈ s.attach, f ↑x
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↥s), f ↑x = ∏ x ∈ s, f x

Tactic:
rw [← prod_attach]; exact tprod_fintype _

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

pp: case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A

Tactic:
;

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
x✝ : A
| ∑ kl ∈ antidiagonal x✝, f kl.1 * g kl.2

pp: case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A

Tactic:
;

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
x✝ : A
| ∑ kl ∈ antidiagonal x✝, f kl.1 * g kl.2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

pp: case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| SummationFilter.unconditional A

Tactic:
;

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| SummationFilter.unconditional A
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
x✝ : A
| ∑ kl ∈ antidiagonal x✝, f kl.1 * g kl.2

pp: case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| SummationFilter.unconditional A

Tactic:
;

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
x✝ : A
| ∑ kl ∈ antidiagonal x✝, f kl.1 * g kl.2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| SummationFilter.unconditional A
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Tactic:
rw [hf.tsum_mul_tsum hg hfg, ← HasAntidiagonal.sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)]

Goal state after:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ ∑' (c : (n : A) × ↥(antidiagonal n)),
      f (HasAntidiagonal.sigmaAntidiagonalEquivProd c).1 * g (HasAntidiagonal.sigmaAntidiagonalEquivProd c).2 =
    ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
x✝ : Finset ι
| ∏ b ∈ x✝, (fun x ↦ 1 + f x) b

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
x✝ : Finset ι
| ∏ b ∈ x✝, (fun x ↦ 1 + f x) b
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)

Tactic:
;

Goal state after:
⊢ ⨅ l, ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
;

Goal state after:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case zero
ι : Sort u_1
n : ℕ
hn : 0 ≠ 0
⊢ (fun x ↦ x ^ 0) = ⇑(NNReal.powOrderIso 0 hn).withTopCongr

pp: case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr

Tactic:
;

Goal state after:
case zero
ι : Sort u_1
n : ℕ
hn : 0 ≠ 0
⊢ (fun x ↦ x ^ 0) = ⇑(NNReal.powOrderIso 0 hn).withTopCongr

case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr

Tactic:
;

Goal state after:
case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
n : ℕ
f : ι → ℝ≥0
⊢ (⨆ i, (fun i ↦ ↑(f i)) i) ^ n = ⨆ i, (fun i ↦ ↑(f i)) i ^ n

Tactic:
;

Goal state after:
ι : Sort u_1
inst✝ : Nonempty ι
n : ℕ
f : ι → ℝ≥0
⊢ (⨆ i, (fun i ↦ ↑(f i)) i) ^ n = ⨆ i, (fun i ↦ ↑(f i)) i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
n : ℕ
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)) ^ n = ⨆ i, ↑(f i) ^ n

Tactic:
;

Goal state after:
ι : Sort u_1
inst✝ : Nonempty ι
n : ℕ
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)) ^ n = ⨆ i, ↑(f i) ^ n
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ n ≤ n

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ n ≤ n
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Pi.mulSingle b a b' = 1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Pi.mulSingle b a b' = 1
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
obtain ⟨t, ht_anti, htl, htW, hts⟩ :
      ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s := by
    have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
      rw [le_principal_iff] at hls
      have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
      simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using! this
    choose t htl htW hts using this
    have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
    exact ⟨fun n => ⋂ k ≤ n, t k, fun m n h =>
      biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
      (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n =>
      (prod_mono (this n) (this n)).trans (htW n), fun n => (this n).trans (hts n)⟩

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
⊢ ∃ x ∈ s, l ≤ 𝓝 x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i

Tactic:
;

Goal state after:
α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)

Tactic:
by
  simp only [nhds_of_ne_top ha, tendsto_iInf, tendsto_principal]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)

Tactic:
;

Goal state after:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
;

Goal state after:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)

Tactic:
simp_rw [Function.comp_def, h, ← comp_apply (f := g)]

Goal state after:
α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (fun x ↦ (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case bc
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ 1 < 2

Tactic:
;

Goal state after:
case bc
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ 1 < 2
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case top
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
ha : ∞ ≠ 0 ∨ b ≠ ∞
hb : ¬b = 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))

Tactic:
;

Goal state after:
case top
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
ha : ∞ ≠ 0 ∨ b ≠ ∞
hb : ¬b = 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ t'' ∈ ↑f ×ˢ ↑(pureCauchy x)

Tactic:
;

Goal state after:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ t'' ∈ ↑f ×ˢ ↑(pureCauchy x)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)

Tactic:
simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
      refine fun hcon => hbdd ↑(q - 1) ?_
      filter_upwards [hcon] with x hx using not_lt.1 hx

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist (↑x) a + edist (↑y) a < r + r

Tactic:
;

Goal state after:
β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist (↑x) a + edist (↑y) a < r + r
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case mk
α : Type u_1
inst✝ : LinearOrder α
a val✝ : α
property✝ : val✝ ∈ Ici a
⊢ projIci a ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
inst✝ : LinearOrder α
a val✝ : α
property✝ : val✝ ∈ Ici a
⊢ projIci a ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case mk
α : Type u_1
inst✝ : LinearOrder α
b val✝ : α
property✝ : val✝ ∈ Iic b
⊢ projIic b ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
inst✝ : LinearOrder α
b val✝ : α
property✝ : val✝ ∈ Iic b
⊢ projIic b ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y' y)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y' y)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: case hbc
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑K.toNNReal

Tactic:
;

Goal state after:
case hbc
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑K.toNNReal
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: case hbc
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K ≤ ↑K.toNNReal

Tactic:
;

Goal state after:
case hbc
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K ≤ ↑K.toNNReal
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ ↑r ≤ ↑(liminf u f) ↔ ↑r ≤ liminf (fun i ↦ ↑(u i)) f

Tactic:
rw [coe_le_coe, le_liminf_iff, le_liminf_iff]

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ∀ y < ↑r, ∀ᶠ (a : ι) in f, y < ↑(u a)