mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ↑(MaxProducts C ho)
⊢ (↑↑l).head! = term I ho

Tactic:
rw [eq_comm, ← ord_term ho]
  have hm := l.prop.2
  have := Products.prop_of_isGood_of_contained C _ l.prop.1 hsC l.val.val.head!
    (List.head!_mem_self (List.ne_nil_of_mem hm))
  simp only [Order.lt_succ_iff] at this
  refine eq_of_le_of_not_lt this (not_lt.mpr ?_)
  have h : ord I (term I ho) ≤ ord I l.val.val.head! := by
    simp only [ord, Ordinal.typein_le_typein, not_lt]
    exact Products.rel_head!_of_mem hm
  rwa [ord_term_aux] at h

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 : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ↑(skeletonLT C n) ∩ closedCell m j = ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
refine subset_antisymm ?_ (inter_subset_inter_right _ (cellFrontier_subset_closedCell _ _))

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ↑(skeletonLT C n) ∩ closedCell m j ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j
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✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
⊢ ∑ i, 1 ≤ ∑ i, (U i ∩ f ⁻¹' {y}).encard

Tactic:
refine Fintype.sum_mono fun i ↦ Set.one_le_encard_iff_nonempty.mpr (show y ∈ f '' (U i) from ?_)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
i : Fin n
⊢ y ∈ f '' U i
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε

Tactic:
choose F hF using fun y => show ∃ z ∈ tβ, dist y z < ε₂ by simpa using htβ (mem_univ y)

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
Module: Mathlib.Topology.ContinuousMap.Sigma

Goal state before:
pp: X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h : (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g'⟩
hg : ⇑g ≍ ⇑g'
⊢ ⟨i, g⟩ = ⟨i, g'⟩

Tactic:
simpa using hg

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
i : ι
⊢ ∀ (f : C(X i, Y × Z)), Continuous[inst✝⁴ i, inst✝¹] (g ∘ ⇑f)

Tactic:
f

Goal state after:
case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
i : ι
f : C(X i, Y × Z)
⊢ Continuous[inst✝⁴ i, inst✝¹] (g ∘ ⇑f)
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
⊢ Metric.eball none 1 ⊆ s

Tactic:
by simpa [ball_infty_of_pos]

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
i : ι
⊢ ∀ (f : C(X i, Y)), IsOpen[inst✝³ i] (⇑f ⁻¹' V)

Tactic:
f

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
i : ι
f : C(X i, Y)
⊢ IsOpen[inst✝³ i] (⇑f ⁻¹' V)
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
i : ι
⊢ ∀ (f : C(X i, Y)), IsClosed[inst✝³ i] (⇑f ⁻¹' V)

Tactic:
f

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
i : ι
f : C(X i, Y)
⊢ IsClosed[inst✝³ i] (⇑f ⁻¹' V)
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
⊢ ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
iSup_le_iff

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
⊢ ∀ (i : ↥J), ⨆ t, edist (f ↑i) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
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
⊢ ∀ (i : ↥J), ⨆ t, edist (f ↑i) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
rintro ⟨s, hs⟩

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
s : T
hs : s ∈ J
⊢ ⨆ t, edist (f ↑⟨s, hs⟩) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
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
s : T
hs : s ∈ J
⊢ ⨆ t, edist (f ↑⟨s, hs⟩) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
iSup_le_iff

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
s : T
hs : s ∈ J
⊢ ∀ (i : { t // edist ⟨s, hs⟩ t ≤ c }), edist (f ↑⟨s, hs⟩) (f ↑↑i) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
⊢ Homotopic p q → Path.Homotopic (toLoop i p) (toLoop i q)

Tactic:
refine Nonempty.map fun H ↦ ⟨⟨⟨fun t ↦ ⟨homotopyTo i H t, ?_⟩, ?_⟩, ?_, ?_⟩, ?_⟩
  · rintro y ⟨i, iH⟩
    rw [homotopyTo_apply, H.eq_fst, p.2]
    all_goals apply Cube.insertAt_boundary; right; exact ⟨i, iH⟩
  · fun_prop
  iterate 2
    intro
    ext
    dsimp
    rw [homotopyTo_apply, toLoop_apply]
    swap
  · apply H.apply_zero
  · apply H.apply_one
  intro t y yH
  ext
  dsimp
  rw [homotopyTo_apply]
  apply H.eq_fst; use i
  rw [funSplitAt_symm_apply, dif_pos rfl]; exact yH

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
⊢ Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Tactic:
ih

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x ↦ ↑(eraseIdx i x)) (𝓝 ⟨l, hl⟩) (𝓝 ↑⟨l.eraseIdx ↑i, ⋯⟩)

Tactic:
simp only [Vector.eraseIdx_val]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x ↦ (↑x).eraseIdx ↑i) (𝓝 ⟨l, hl⟩) (𝓝 (l.eraseIdx ↑i))
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ packingNumber ε A = 0 ↔ A = ∅

Tactic:
simp only [packingNumber, ENat.iSup_eq_zero, encard_eq_zero]
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  by_contra!
  obtain ⟨x, hx⟩ := this
  simpa using h {x} (by simp [hx]) (by simp)

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' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ ∃ z' ∈ s (n + l + 1), edist (↑z) z' < B n / 2 ^ l

Tactic:
refine exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_

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' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ hausdorffEDist ↑(s (n + l)) ↑(s (n + l + 1)) < B n / 2 ^ l
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a b : HomotopyGroup N X x
p q : ↑(Ω^ N X x)
⊢ (homotopyGroupEquivFundamentalGroupOfUnique N).toFun (⟦p⟧ * ⟦q⟧) =
    (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦p⟧ * (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦q⟧

Tactic:
simp only [HomotopyGroup.mul_spec (i := default)]

Goal state after:
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a b : HomotopyGroup N X x
p q : ↑(Ω^ N X x)
⊢ (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦transAt default q p⟧ =
    (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦p⟧ * (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦q⟧
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ dist x y = dist (inl x) (inl y)

Tactic:
by
        rw [@Sum.dist_eq X Y]
        rfl

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = dist (inr x) (inr y)

Tactic:
by
        rw [@Sum.dist_eq X Y]
        rfl

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

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)

Tactic:
by
  refine Isometry.of_dist_eq fun a b => ?_
  refine (embeddingOfSubset_dist_le x a b).antisymm (le_of_forall_pos_le_add fun e epos => ?_)
  -- First step: find n with dist a (x n) < e
  rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with ⟨n, hn⟩
  -- Second step: use the norm control at index n to conclude
  have C : dist b (x n) - dist a (x n) = embeddingOfSubset x b n - embeddingOfSubset x a n := by
    simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
  have :=
    calc
      dist a b ≤ dist a (x n) + dist (x n) b := dist_triangle _ _ _
      _ = 2 * dist a (x n) + (dist b (x n) - dist a (x n)) := by simp [dist_comm]; ring
      _ ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| := by grw [← le_abs_self]
      _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| := by
        rw [C]
        gcongr
      _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
        gcongr
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n
      _ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring
  simpa [dist_comm] using this

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

Goal state before:
pp: case pos
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A ≠ ⊤
⊢ coveringNumber ε A ≤ packingNumber ε A

Tactic:
rw [← encard_maximalSeparatedSet h_top]
    exact isCover_maximalSeparatedSet h_top |>.coveringNumber_le_encard maximalSeparatedSet_subset

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f ≠ ∞ ↔ MemHolder r f

Tactic:
by
  rw [← eHolderNorm_lt_top, lt_top_iff_ne_top]

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞

Tactic:
by
  rw [infsep, ENNReal.toReal_eq_zero_iff]

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ Nonempty (X ≃ᵢ Y) → toGHSpace X = toGHSpace Y

Tactic:
by
    rintro ⟨e⟩
    simp only [toGHSpace]
    have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm
    have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange
    have I :
      (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) =
        (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rfl
    rw [Quotient.eq]
    exact ⟨cast I ((f.trans e).trans g)⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.einfsep = 0 ∨ s.Subsingleton ↔ s.Subsingleton

Tactic:
or_iff_right_iff_imp

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.einfsep = 0 → s.Subsingleton
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hUS : univ ∉ S
b : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
a : α
hU : ¬⋃₀ S = univ
hO : IsOpen[t] (⋃₀ S)
hs : (Ici a)ᶜ ∈ S
⊢ b ∉ (Ici a)ᶜ

Tactic:
simp_all only [compl_Ici, mem_Ici, sSup_le_iff, mem_ofPred_eq, mem_Iio, not_lt]

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
by
  by_cases hU : U = univ
  · simp only [hU, isOpen_univ, compl_Ici, true_or]
  refine ⟨?_, isTopologicalBasis_insert_univ_subbasis.isOpen⟩
  intro hO
  apply Or.inr
  convert! IsTopologicalBasis.open_eq_sUnion isTopologicalBasis_insert_univ_subbasis hO
  constructor
  · intro ⟨a, ha⟩
    use {U}
    constructor
    · apply subset_trans (singleton_subset_iff.mpr _) (subset_insert _ _)
      use a
    · rw [sUnion_singleton]
  · intro ⟨S, hS1, hS2⟩
    have hUS : univ ∉ S := by
      by_contra hUS'
      apply hU
      rw [hS2]
      exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)
    use sSup {a | (Ici a)ᶜ ∈ S}
    rw [hS2, sUnion_eq_compl_sInter_compl, compl_inj_iff]
    apply le_antisymm
    · intro b hb
      simp only [sInter_image, mem_iInter, mem_compl_iff]
      intro s hs
      obtain ⟨a, ha⟩ := (subset_insert_iff_of_notMem hUS).mp hS1 hs
      subst hS2 ha
      simp_all only [compl_Ici, mem_Ici, sSup_le_iff, mem_ofPred_eq, mem_Iio, not_lt]
    · intro b hb
      rw [mem_Ici, sSup_le_iff]
      intro c hc
      simp only [sInter_image, mem_iInter] at hb
      rw [← not_lt, ← mem_Iio, ← compl_Ici]
      exact hb _ hc

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ (U = univ ∨ ∃ a, (Iic a)ᶜ = U) → IsOpen[inst✝¹] U

Tactic:
rintro (rfl | ⟨a, rfl⟩)

Goal state after:
case mpr.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] univ

case mpr.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
a : α
⊢ IsOpen[inst✝¹] (Iic a)ᶜ
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ scottHausdorff α univ ≤ inst✝¹

Tactic:
rw [IsLower.topology_eq α]
  exact scottHausdorff_le_lower

Goal state after:
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : ↑(𝒫 s)}, U t₁ ∩ d = U t₂ ∩ d → ↑t₁ ⊆ ↑t₂
h_inj : Injective fun x ↦ U x ∩ d
⊢ 2 ^ #↑s ≤ 2 ^ #↑d

Tactic:
← mk_powerset,

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : ↑(𝒫 s)}, U t₁ ∩ d = U t₂ ∩ d → ↑t₁ ⊆ ↑t₂
h_inj : Injective fun x ↦ U x ∩ d
⊢ #↑(𝒫 s) ≤ 2 ^ #↑d
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : ↑(𝒫 s)}, U t₁ ∩ d = U t₂ ∩ d → ↑t₁ ⊆ ↑t₂
h_inj : Injective fun x ↦ U x ∩ d
⊢ #↑(𝒫 s) ≤ 2 ^ #↑d

Tactic:
← mk_powerset,

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : ↑(𝒫 s)}, U t₁ ∩ d = U t₂ ∩ d → ↑t₁ ⊆ ↑t₂
h_inj : Injective fun x ↦ U x ∩ d
⊢ #↑(𝒫 s) ≤ #↑(𝒫 d)