mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ etaFn G origin ∈ U

Tactic:
← hsv

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ etaFn G origin ∈ Subtype.val ⁻¹' s
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
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ (Subgroup.zpowers x⁻¹).topologicalClosure

Tactic:
← inv_mem_iff

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x⁻¹ ∈ (Subgroup.zpowers x⁻¹).topologicalClosure
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
⊢ 𝓝 1 ≤ Filter.map (⇑(Units.coeHom R)) (𝓝 1)

Tactic:
rw [nhds_induced, nhds_prod_eq]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
⊢ 𝓝 1 ≤
    Filter.map (⇑(Units.coeHom R))
      (Filter.comap (⇑(Units.embedProduct R)) (𝓝 ((Units.embedProduct R) 1).1 ×ˢ 𝓝 ((Units.embedProduct R) 1).2))
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous[inst✝¹, inst✝] f
ho : IsOpenMap f
s : Set β
h : BaireMeasurableSet s
⊢ BaireMeasurableSet (f ⁻¹' s)

Tactic:
rcases h with ⟨u, hu, hsu⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous[inst✝¹, inst✝] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ BaireMeasurableSet (f ⁻¹' s)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
S : Set X.A
⊢ IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
by
  rw [← isOpen_compl_iff]
  constructor
  · intro cond F h
    by_contra c
    specialize cond F c
    rw [compl_mem_iff_notMem] at cond
    contradiction
  · intro h1 F h2
    specialize h1 F
    rcases F.mem_or_compl_mem S with h | h
    exacts [absurd (h1 h) h2, h]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
⊢ Injective (openCell 0)

Tactic:
intro x y h
  rw [openCell_zero_eq_singleton, openCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
  exact injective_map_zero C 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✝ : RelCWComplex C D
⊢ D ⊆ C

Tactic:
simp_rw [← union]
  exact subset_union_left

Goal state after:
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
⊢ (ConcreteCategory.hom f) (X.str g) = (ConcreteCategory.hom f) x

Tactic:
str_eq_of_le_nhds _ x _

Goal state after:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x

X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑g ≤ 𝓝 x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
⊢ ord I i = o ↔ term I ho = i

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · subst h
    exact term_ord_aux ho
  · subst h
    exact ord_term_aux ho

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✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ⊆ ↑E

Tactic:
simp_rw [← union]
  exact subset_union_left

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 : ↑(MaxProducts C ho)
⊢ term I ho = (↑↑l).head!

Tactic:
← ord_term ho

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 : ↑(MaxProducts C ho)
⊢ ord I (↑↑l).head! = o
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅

Tactic:
← isCompactSystem_insert_empty_iff

Goal state after:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ IsCompactSystem (insert ∅ S) ↔
    ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
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 : Fin n), (U i ∩ f ⁻¹' {y}).encard

Tactic:
rw [finsum_eq_sum_of_fintype]

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, 1 ≤ ∑ i, (U i ∩ f ⁻¹' {y}).encard
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 < ε₁
εε₁ : ε₁ < ε
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε

Tactic:
let ε₂ := ε₁ / 2 / 2

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
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
obtain ⟨a, haA, hacc⟩ := h (Set.range x ∩ A) inter_subset_right <| by
        rw [eventually_iff, mem_cofinite, compl_ofPred] at hx
        exact hfin.inter_of_finite_sdiff (hx.image x |>.subset (by grind))

Goal state after:
case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ ∃ a ∈ A, MapClusterPt a cofinite x
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case pos
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hAU : A ⊆ ⋃ i, U i
h : Nonempty ι
⊢ ∃ t, A ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨f, hf⟩ := hl.indexed_countable_subcover U hUo hAU
    obtain ⟨t, ht⟩ := isCountablyCompact_iff_countable_open_cover.1 hA (U ∘ f)
      (fun n => hUo (f n)) hf
    classical
    exact ⟨t.image f, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.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
U : ↑(countableBasis X)
n : ℕ
⊢ IsCompact (Subtype.val '' (K U) n)

Tactic:
exact ((K U).isCompact _).image continuous_subtype_val

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ x ∈ f ⁻¹' s

Tactic:
rw [mem_preimage, this]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ f a ∈ s
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ ↑(#({x ∈ J | edist (Exists.choose hJ) x ≤ ↑n * c})) ≤ ↑(#J)

Tactic:
by gcongr; apply Finset.filter_subset

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

Goal state before:
pp: case mp
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∈ Cube.boundary (M ⊕ N) → y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
rintro ⟨i | i, hi⟩

Goal state after:
case mp.inl
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
i : M
hi : y (Sum.inl i) = 0 ∨ y (Sum.inl i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

case mp.inr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
i : N
hi : y (Sum.inr i) = 0 ∨ y (Sum.inr i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero
x : ℝ
hx : x ∈ cantorSet
⊢ (cantorSequence x).get 0 ∈ cantorSet

Tactic:
simpa [cantorSequence]

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

Goal state before:
pp: case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x ↦ -3⁻¹ ^ x) Filter.atTop (nhds 0)

Tactic:
rw [show 0 = -(0 : ℝ) by simp]

Goal state after:
case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x ↦ -3⁻¹ ^ x) Filter.atTop (nhds (-0))
Module: Mathlib.Topology.List

Goal state before:
pp: case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : Tendsto (fun p ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))
⊢ Tendsto (fun p ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Tactic:
exact this.comp (tendsto_id.prodMap ih)

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

Goal state before:
pp: case i
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
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
⊢ #J - 1 < #J

Tactic:
exact Nat.sub_lt (Finset.card_pos.mpr hJ) zero_lt_one

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

Goal state before:
pp: case mpr.refine_3
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
y : N → ↑I
⊢ { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯ }.toFun (1, y) = ↑a₂ y

pp: case mpr.refine_4
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 ↦
              { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑a₁ x_1

Tactic:
· exact (H.apply_one _).trans (congr_arg a₂ (eq_const_of_unique y).symm)

Goal state after:
case mpr.refine_4
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 ↦
              { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑a₁ x_1
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ hausdorffEDist s t ≤ δ

Tactic:
rw [hausdorffEDist, max_le_iff]
  rw [hausdorffEntourage, Set.mem_ofPred] at h
  conv at h => enter [2, 2, 1, 1, _]; rw [edist_comm]
  have {s t : Set α} (h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t) :
      ⨆ x ∈ s, infEDist x t ≤ δ := by
    rw [iSup₂_le_iff]
    intro x hx
    obtain ⟨y, hy, hxy⟩ := h hx
    exact iInf₂_le_of_le y hy hxy
  exact ⟨this h.1, this h.2⟩

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

pp: case neg
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:
case neg
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A = ⊤
⊢ coveringNumber ε A ≤ packingNumber ε A
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ (¬∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C) ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
simp only [not_forall, not_exists, not_lt, exists_prop, not_and]

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

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = 0 → ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
intro h x₁ x₂
    by_cases hx : x₁ = x₂
    · rw [hx]
    · rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot] at h
      rw [← edist_eq_zero, ← nonpos_iff_eq_zero]
      refine le_of_forall_gt fun b hb => ?_
      obtain ⟨C, hC, hC'⟩ := h (b / edist x₁ x₂ ^ (r : ℝ))
        (ENNReal.div_pos hb.ne.symm (ENNReal.rpow_lt_top_of_nonneg zero_le_coe
          (edist_lt_top x₁ x₂).ne).ne)
      exact lt_of_le_of_lt (hC x₁ x₂) <| ENNReal.mul_lt_of_lt_div hC'

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 Y
inst✝ : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
x✝ : MemHolder r (c • f)
h : ℝ≥0
hh : HolderWith h r (c • f)
⊢ HolderWith (h * ‖c‖₊⁻¹ * ‖c‖₊) r (c • f)

Tactic:
inv_mul_cancel_right₀ hc

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 Y
inst✝ : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
x✝ : MemHolder r (c • f)
h : ℝ≥0
hh : HolderWith h r (c • f)
⊢ HolderWith h r (c • f)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep

Tactic:
rw [not_nontrivial_iff] at hs
    exact hs.einfsep.symm ▸ WithTop.top_pos

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
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
⊢ ⟦A⟧ = toGHSpace X

Tactic:
eq_toGHSpace_iff

Goal state after:
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑A
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
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
⊢ ⟦B⟧ = toGHSpace Y

Tactic:
eq_toGHSpace_iff

Goal state after:
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑B
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ lower α = generateFrom {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
lower

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ generateFrom {s | ∃ a, (Ici a)ᶜ = s} = generateFrom {s | ∃ a, (Ici a)ᶜ = s}
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: ⊢ {∅, {True}} = {s | ∃ a, (Iic a)ᶜ = s}

Tactic:
exact le_antisymm
      (fun h hs => by
        simp only [compl_Iic, mem_ofPred_eq]
        rw [← Ioi_True, ← Ioi_False] at hs
        rcases hs with (rfl | rfl)
        · use True
        · use False)
      (by rintro _ ⟨a, rfl⟩; by_cases a <;> aesop (add simp [Ioi, lt_iff_le_not_ge]))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
T : Set α
inst✝ : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
⊢ T ↓∩ (↑(upperClosure ↑F))ᶜ = (hull T (F.inf id))ᶜ

Tactic:
rw [Set.preimage_compl, (hull_finsetInf hT)]

Goal state after: