mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt 1 atTop fun x_1 ↦ x ^ x_1

Tactic:
simpa using mapClusterPt_self_zpow_atTop_pow x 0

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: case inl
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : IsEmpty ((n : ℕ) × cell C n)
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → IsEmpty (cell C b)

Tactic:
exact ⟨0, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
intro cond

Goal state after:
case mp
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
⊢ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
⊢ ↑F ≤ 𝓝 x → X.str F = x

Tactic:
intro cond

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
⊢ X.str F = x
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
⊢ i ∈ I n → i ∈ J n

Tactic:
hi

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
⊢ i ∈ J n
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
⊢ False

Tactic:
have h : openCell n i ⊆ D ∪ ⋃ n, ⋃ (j : J n), openCell (C := C) n j :=
    hIJ.symm ▸ subset_union_of_subset_right
      (subset_iUnion_of_subset n (subset_iUnion_of_subset ⟨i, hi⟩ (subset_refl (openCell n i)))) D

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ Submodule.span ℤ (Set.range (spanFinBasis C s)) ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s)))

Tactic:
rw [Submodule.span_le]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ Set.range (spanFinBasis C s) ⊆ ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s))))
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Tactic:
Tendsto,

Goal state after:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Filter.map ⇑(ConcreteCategory.hom f) ↑g ≤ 𝓝 ((ConcreteCategory.hom f) x)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
⊢ i ∈ ↑l → J i

Tactic:
hi

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
⊢ J i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
x✝ : List I
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) x✝ →
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) x✝).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ x✝})

Tactic:
induction l with

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
i : I
hi✝ : o ≤ ord I i
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
⊢ x (term I ho) = x i

Tactic:
hi

Goal state after:
case inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
i : I
hi✝ : o ≤ ord I i
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
⊢ x i = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : term I ho = i
⊢ x (term I ho) = x i

Tactic:
hi

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : term I ho = i
⊢ x i = x i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h.inr.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i✝ : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i✝
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j
hp : x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
x✝ : ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
k : ℕ
hkl : k < l
i : cell C k
hi : i ∈ p l ⋯ j k
hxi : x ∈ openCell k i
⊢ i ∈ I k

Tactic:
simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]

Goal state after:
case h.inr.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i✝ : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i✝
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j
hp : x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
x✝ : ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
k : ℕ
hkl : k < l
i : cell C k
hi : i ∈ p l ⋯ j k
hxi : x ∈ openCell k i
⊢ i ∈ J k ∨ ∃ a < n + 1, ∃ a_1 ∈ J a, i ∈ if h : a ≤ n then p a h a_1 k else ∅
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i✝ : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i✝
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j
hp : x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
x✝ : ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
k : ℕ
hkl : k < l
i : cell C k
hi : i ∈ p l ⋯ j k
hxi : x ∈ openCell k i
⊢ i ∈ if h : l ≤ n then p l h j k else ∅

Tactic:
simp [Nat.le_of_lt_succ hln, hi]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
i : I
⊢ i ∈ ↑l → ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)

Tactic:
hi

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
i : I
hi : i ∈ ↑l
⊢ ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: ⊢ ∀ {X Y : UniformSpaceCat} (f : X.Hom Y), { hom' := ⟨↑f.hom' ∘ ↑{ hom' := ⟨id, ⋯⟩ }.hom', ⋯⟩ } = f

Tactic:
by intros; apply Hom.ext; simp

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: ⊢ ∀ {X Y : UniformSpaceCat} (f : X.Hom Y), { hom' := ⟨↑{ hom' := ⟨id, ⋯⟩ }.hom' ∘ ↑f.hom', ⋯⟩ } = f

Tactic:
by intros; apply Hom.ext; simp

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
⊢ ↑(skeletonLT C ↑n) ∪ ⋃ j, closedCell n j = ↑(skeletonLT C (↑n + 1))

Tactic:
rw [coe_skeletonLT, coe_skeletonLT, union_assoc]
  congr
  norm_cast
  exact (biUnion_lt_succ _ _).symm

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
i : I
⊢ i ∈ ↑l.Tail → ↑x i = SwapTrue o (↑x) i

Tactic:
hi

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
i : I
hi : i ∈ ↑l.Tail
⊢ ↑x i = SwapTrue o (↑x) i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
· rw [Products.lt_iff_lex_lt, hM] at hq
    simp only [List.not_lex_nil] at hq

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ Finite (ConnectedComponents X)

Tactic:
by
    refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
    · exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)
    · exact fun i j hij ↦ (Disjoint.preimage mk (by simpa)).preimage f
    · rw [Set.iUnion_eq_univ_iff]
      exact fun x ↦ ⟨mk (f x), rfl⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : none ∈ s
⊢ 1 > 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: t : ↑I
⊢ Set.projIcc 0 1 qRight._proof_1 (2 * ↑(t, 1).1 / (1 + ↑(t, 1).2)) = Set.projIcc 0 1 ⋯ ↑t

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ (𝓝 (x, y)).HasBasis
    (fun x_1 ↦
      match (x, y) with
      | (x, y) =>
        match x_1 with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
    fun x ↦
    match x with
    | (Ux, Uy) => Ux ×ˢ Uy

Tactic:
rw [nhds_prod_eq]

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis
    (fun x_1 ↦
      match (x, y) with
      | (x, y) =>
        match x_1 with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
    fun x ↦
    match x with
    | (Ux, Uy) => Ux ×ˢ Uy
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case neg
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
⊢ a ^ (Nat.find ⋯ - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(Nat.find ⋯) - 1) * c}))

Tactic:
have : Nat.find (exists_radius_le t V ha c) - 1 < Nat.find (exists_radius_le t V ha c) := by
    simp

Goal state after:
case neg
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
this : Nat.find ⋯ - 1 < Nat.find ⋯
⊢ a ^ (Nat.find ⋯ - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(Nat.find ⋯) - 1) * c}))
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y

Tactic:
by_contra H : x ≠ y

Goal state after:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
⊢ False
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
⊢ i ∈ Finset.range #J → pairSetSeq J a c i ⊆ J ×ˢ J

Tactic:
hi

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
⊢ pairSetSeq J a c i ⊆ J ×ˢ J
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero.refine_1
⊢ 0 ≤ 1 / 4

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero.refine_2
⊢ 1 / 4 ≤ 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero.refine_3
⊢ 0 ≤ 3 / 4

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero.refine_4
⊢ 3 / 4 ≤ 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ (fun x ↦ x / 3) (3 / 4) = 1 / 4

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ (fun x ↦ (2 + x) / 3) (1 / 4) = 3 / 4

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
⊢ pure l ≤ traverse 𝓝 l

Tactic:
induction l with

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) [] v ∧ sequence v ⊆ s

Tactic:
exists []

Goal state after:
case nil
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) [] [] ∧ sequence [] ⊆ s
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ |3⁻¹| < 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) (cons <$> 𝓝 a <*> 𝓝 l)

Tactic:
Tendsto,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Filter.map (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ edist (logSizeBallSeq J hJ a c l).point t ≤ ↑(logSizeBallSeq J hJ a c l).radius * c

Tactic:
apply le_trans (edist_triangle _ s _)

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := ⋯
l : ℕ := ⋯
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ edist (logSizeBallSeq J hJ a c l).point s + edist s t ≤ ↑(logSizeBallSeq J hJ a c l).radius * c
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
⊢ i ∈ s → (∃ b ∈ s, (f i) x z ≤ (f b) x y) ∨ ∃ b ∈ s, (f i) x z ≤ (f b) y z

Tactic:
hi

Goal state after:
case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
⊢ (∃ b ∈ s, (f i) x z ≤ (f b) x y) ∨ ∃ b ∈ s, (f i) x z ≤ (f b) y z
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
l : List α
⊢ Tendsto prod (𝓝 l) (𝓝 l.prod)

Tactic:
induction l with

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A C : Set E
hC₁ : IsCover 0 A C
⊢ A.encard ≤ C.encard

Tactic:
isCover_zero

Goal state after:
E : Type u_3
inst✝ : EMetricSpace E
A C : Set E
hC₁ : A ⊆ C
⊢ A.encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ 1 ≤ 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ ↑ε
⊢ coveringNumber ε A = 1

Tactic:
refine le_antisymm ?_ ?_
  · have ⟨a, ha⟩ := h_nonempty
    calc coveringNumber ε A
      _ ≤ ({a} : Set X).encard :=
        (IsCover.singleton_of_ediam_le hA ha).coveringNumber_le_encard (by simp [ha])
      _ ≤ 1 := by simp
  · simpa [Order.one_le_iff_pos]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
⊢ ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n

Tactic:
intro n x xt0

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
⊢ ∃ y ∈ s n, edist x y ≤ 2 * B n
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: ⊢ 1 < 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: X : Set (ℕ → Bool)
h_closed : IsClosed X
h_nonempty : X.Nonempty
⊢ ∃ f, Continuous f ∧ Set.range f = X

Tactic:
obtain ⟨f, fs, frange, hf⟩ := PiNat.exists_lipschitz_retraction_of_isClosed h_closed h_nonempty

Goal state after:
X : Set (ℕ → Bool)
h_closed : IsClosed X
h_nonempty : X.Nonempty
f : (ℕ → Bool) → ℕ → Bool
fs : ∀ x ∈ X, f x = x
frange : Set.range f = X
hf : LipschitzWith 1 f
⊢ ∃ f, Continuous f ∧ Set.range f = X
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep ≠ ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ∞

Tactic:
← lt_top_iff_ne_top,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞