mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
⊢ ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty

Tactic:
intro T hT

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
⊢ (⋂₀ ι T).Nonempty
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: case refine_2
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
b : ↑C
hb : ∀ (J : Finset ι), (π_app C fun x ↦ x ∈ J) b = ↑a (op J)
⊢ ∃ a_1, (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a_1 = a

pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
⊢ ∃ x, ∀ (J : Finset ι), (π_app C fun x ↦ x ∈ J) x = ↑a (op J)

Tactic:
· use b
          apply Subtype.ext
          apply funext
          intro J
          exact hb (unop J)

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
⊢ ∃ x, ∀ (J : Finset ι), (π_app C fun x ↦ x ∈ J) x = ↑a (op J)
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
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
h' : Disjoint (openCell n i) (D ∪ ⋃ n, ⋃ j, openCell n ↑j)
⊢ False

Tactic:
disjoint_of_subset_iff_left_eq_empty h

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
h' : openCell n i = ∅
⊢ False
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
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
⊢ ∀ (F : fsu), ↑F ⊆ T1 → (⋂₀ ι F).Nonempty

Tactic:
intro T hT

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
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
hT : ↑T ⊆ T1
⊢ (⋂₀ ι T).Nonempty
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
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
i : I
⊢ ord I i < o → ord I i = o → true = ↑x i

Tactic:
intro h₁

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
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
i : I
h₁ : ord I i < o
⊢ ord I i = o → true = ↑x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ ⇑((πs C o₂) ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))) =
    ⇑((πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))

Tactic:
coe_πs C o₂,

Goal state after:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (⇑((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)) ∘ ProjRestrict C fun x ↦ ord I x < o₂) =
    ⇑((πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_3.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₀ : x ∈ C0 C ho
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩

Tactic:
have hx₀' : ProjRestrict C (ord I · < o) ⟨x, hx⟩ = x := by
        simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using! C0_projOrd C hsC ho hx₀

Goal state after:
case refine_3.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₀ : x ∈ C0 C ho
hx₀' : ↑(ProjRestrict C (fun x ↦ ord I x < o) ⟨x, hx⟩) = x
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩
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) = C

Tactic:
by
  apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeletonLT C _).subset_complex)
  simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]
  exact ⟨subset_iUnion_of_subset 0 (skeletonLT C 0).base_subset,
    fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeletonLT n i)⟩

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k = ∅
⊢ dissipate C n = ∅

Tactic:
← subset_empty_iff,

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
⊢ dissipate C n ⊆ ∅
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case refine_3
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}))
⊢ ∀ (x : X), ∃ i, x ∈ f ⁻¹' mk ⁻¹' {i}

Tactic:
exact fun x ↦ ⟨mk (f x), rfl⟩

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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
⊢ False

Tactic:
apply l.prop.1

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
⊢ Products.eval C ↑l ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ map Subtype.val (𝓝 ⟨↑x, ⋯⟩)

pp: case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ ∀ᶠ (x : X) in 𝓝 ↑x, x ∈ ↑U

Tactic:
exacts [image_mem_map hn, (isOpen_of_mem_countableBasis U.2).mem_nhds x.2]

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
⊢ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑g

Tactic:
rw [eventually_nhdsSet_iff_forall] at *

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
⊢ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑g
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
⊢ { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (const M 1)) =
    ContinuousMap.id M

Tactic:
ext1; apply mul_one

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

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ cantorStep x ∈ cantorSet

Tactic:
simp only [cantorStep]
  obtain ⟨y, hy, rfl | rfl⟩ : ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x := by
    rw [cantorSet_eq_union_halves] at hx
    grind
  all_goals
    grind [cantorSet_subset_unitInterval]

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ (cantorSequence x).get (n + 1) = 3 * ((cantorSequence x).get n - 3 ^ n * ofDigitsTerm (cantorToTernary x).get n)

Tactic:
by
  simp only [cantorSequence, ofDigitsTerm, cantorToTernary, cantorToBinary, Set.mem_Icc,
    Bool.if_true_right, Bool.or_false, Stream'.get_map, Bool.cond_not, Bool.cond_decide,
    Stream'.get_succ_iterate', cantorStep]
  split_ifs <;> simp
  field

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this✝ : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
this : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) u v
⊢ s ∈ traverse 𝓝 u

Tactic:
← hvs

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this✝ : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
this : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) u v
⊢ sequence v ∈ traverse 𝓝 u
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
h : j ≠ i
⊢ Function.uncurry (fun x_1 y ↦ Function.uncurry (fun x_2 y ↦ (H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (t, y)) =
    x

Tactic:
apply boundary

Goal state after:
case refine_3.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
h : j ≠ i
⊢ (Prod.map id ⇑(Cube.splitAt i) (t, y)).2.2 ∈ Cube.boundary { j // ¬j = i }
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ (((toLoop i q) (x✝ i)) fun j ↦ x✝ ↑j) = ↑q x✝

Tactic:
apply congr_arg q

Goal state after:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑(Cube.insertAt i) (x✝ i, fun j ↦ x✝ ↑j) = x✝
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: 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
⊢ diam (range inl) + dist (inl default) (inr default) + diam (range inr) =
    diam univ + (dist default default + 1 + dist default default) + diam univ

Tactic:
rw [isometry_inl.diam_range, isometry_inr.diam_range]
      rfl

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

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

Tactic:
· exact (coveringNumber_eq_one_of_ediam_le h_nonempty hA).le

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
c : Y
⊢ eHolderNorm r (Function.const X c) = 0

Tactic:
rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r (Function.const X c)), ↑i < b
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
hX : IsEmpty X
⊢ eHolderNorm r f = 0

Tactic:
rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r f), ↑i < b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y

Tactic:
simp_rw [le_iInf_iff]

Goal state after:
α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ ∀ i ∈ s, x ≠ i → (insert x s).einfsep ≤ edist x i
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔ ∀ x ∈ s.offDiag, x✝ ≤ uncurry edist x

Tactic:
mem_offDiag,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔
    ∀ (x : α × α), x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2 → x✝ ≤ uncurry edist x
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Fintype ↑s
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔ ∀ b ∈ s.offDiag, x✝ ≤ uncurry edist b

Tactic:
mem_offDiag,

Goal state after:
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Fintype ↑s
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x✝ ≤ uncurry edist b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔ ∀ b ∈ s.offDiag, x✝ ≤ uncurry edist b

Tactic:
mem_offDiag,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x✝ ≤ uncurry edist b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔ ∀ i ∈ s.offDiag, x✝ ≤ uncurry dist i

Tactic:
mem_offDiag,

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔
    ∀ (i : α × α), i.1 ∈ s ∧ i.2 ∈ s ∧ i.1 ≠ i.2 → x✝ ≤ uncurry dist i
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔ ∀ b ∈ s.offDiag, x✝ ≤ uncurry dist b

Tactic:
mem_offDiag,

Goal state after:
case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x✝ ≤ uncurry dist b
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite
us : s ⊆ ⋃ i, ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
by
  rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with
    ⟨v, hsv, hvc, hcv⟩
  have := fun i => exists_lt_subset_ball (hvc i) (hcv i)
  choose r' hlt hsub using this
  exact ⟨r', hsv.trans <| iUnion_mono <| hsub, hlt⟩

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

Goal state before:
pp: X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
⊢ ⟦p⟧ = toGHSpace X ↔ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p

Tactic:
simp only [toGHSpace, Quotient.eq]
  refine ⟨fun h => ?_, ?_⟩
  · rcases Setoid.symm h with ⟨e⟩
    have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.trans e
    use fun x => f x, isometry_subtype_coe.comp f.isometry
    rw [range_comp', f.range_eq_univ, Set.image_univ, Subtype.range_coe]
  · rintro ⟨Ψ, ⟨isomΨ, rangeΨ⟩⟩
    have f :=
      ((kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm.trans
          isomΨ.isometryEquivOnRange).symm
    have E : (range Ψ ≃ᵢ NonemptyCompacts.kuratowskiEmbedding X)
        = (p ≃ᵢ range (kuratowskiEmbedding X)) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rw [rangeΨ]; rfl
    exact ⟨cast E f⟩

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔ ∀ b ∈ s.offDiag, x✝ ≤ uncurry dist b

Tactic:
mem_offDiag,

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x✝ ≤ uncurry dist b