mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : ∀ (F : fsu), ↑F ⊆ T1 → (⋂₀ ι F).Nonempty
⊢ X.str F = x

Tactic:
by
    obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
    have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
    have c2 : G.map X.str = X.incl x := by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
    simp [← c1, c2]

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

Goal state before:
pp: case a.tr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
exact subset_union_of_subset_right (subset_iUnion₂_of_subset m hm (subset_iUnion _ j)) _

Goal state after:
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
T : fsu
hT : ↑T ⊆ T1
⊢ ↑T ⊆ finiteInterClosure T1

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 : Set (Ultrafilter X.A)
ht : t ∈ ↑T
⊢ t ∈ finiteInterClosure T1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ Function.Bijective ⇑(iso_map C J)

Tactic:
refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : (iso_map C J) a = (iso_map C J) b
⊢ a = b

case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ ∃ a_1, (iso_map C J) a_1 = a
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
⊢ ∀ (i : ℕ), C i ∈ insert ∅ S

Tactic:
simp [hi]

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
obtain (hs | hs) := (tsupport g).eq_empty_or_nonempty
    · exact ⟨0, by simp [tsupport_eq_empty_iff.mp hs]⟩
    · obtain ⟨z, _, hmax⟩ := hg₂.exists_isMaxOn hs <| hg₁.norm.continuousOn
      refine ⟨2 * ‖g z‖, dist_le_two_norm' fun x ↦ ?_⟩
      by_cases hx : x ∈ tsupport g
      · exact isMaxOn_iff.mp hmax x hx
      · simp [image_eq_zero_of_notMem_tsupport hx]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
⊢ C(↑(Icc a c), E)

Tactic:
by
  by_cases hb : f ⊤ = g ⊥
  · let h (t : α) : E := if t ≤ b then IccExtendCM f t else IccExtendCM g t
    suffices Continuous h from ⟨fun t => h t, by fun_prop⟩
    apply Continuous.if_le (by fun_prop) (by fun_prop) continuous_id continuous_const
    rintro x rfl
    simpa [IccExtendCM, projIccCM]
  · exact .const _ (f ⊥)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : b ≤ ↑t
⊢ (f.concat g) t = g ⟨↑t, ⋯⟩

Tactic:
← concat_comp_IccInclusionRight hb

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : b ≤ ↑t
⊢ (f.concat g) t = ((f.concat g).comp IccInclusionRight) ⟨↑t, ⋯⟩
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst✝¹, inst✝] f
l : Filter F
hl_nebot : l.NeBot
⊢ ∀ [l.IsCountablyGenerated], l ≤ 𝓟 (f '' A) → ∃ a ∈ f '' A, ClusterPt a l

Tactic:
hl_count

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst✝¹, inst✝] f
l : Filter F
hl_nebot : l.NeBot
hl_count : l.IsCountablyGenerated
⊢ l ≤ 𝓟 (f '' A) → ∃ a ∈ f '' A, ClusterPt a l
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
s : Finset ι
f : ι → Set E
hf : ∀ i ∈ s, IsCountablyCompact (f i)
⊢ IsCountablyCompact (⋃ i ∈ s, f i)

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝³ : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
A : Type u_1
inst✝ : TopologicalSpace A
φ : A → ContinuousMapGeneratedBy X Z T
⊢ Continuous[inst✝, _] φ ↔ ∀ (i : ι) (f : C(X i, Z)), Continuous[inst✝, _] (precomp f ∘ φ)

Tactic:
simp only [continuous_iInf_rng, continuous_induced_rng]

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

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace ≤ t

Tactic:
intro u

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
⊢ IsOpen[t] u → IsOpen[⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace] u
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f✝ g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f : X → Y
⊢ ∀ (f' : X → Y), f =ᶠ[𝓝 x] f' → (∀ᶠ (y : X) in 𝓝 x, P y ↑f) → ∀ᶠ (y : X) in 𝓝 x, P y ↑f'

Tactic:
f'

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f✝ g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f f' : X → Y
⊢ f =ᶠ[𝓝 x] f' → (∀ᶠ (y : X) in 𝓝 x, P y ↑f) → ∀ᶠ (y : X) in 𝓝 x, P y ↑f'
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
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
y : X
hy : P y ↑f
h'y : ∀ᶠ (x : X) in 𝓝 y, g x = f x
⊢ P y ↑g

Tactic:
Germ.coe_eq.mpr h'y

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace ↑(s x i)
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, ContractibleSpace ↑r ∧ r ⊆ t

Tactic:
intro t ht

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace ↑(s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
⊢ ∃ r ∈ 𝓝 x, ContractibleSpace ↑r ∧ r ⊆ t
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:
gcongr; apply Finset.filter_subset

Goal state after:
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 : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ {
      toFun := fun t ↦
        ⟨((({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp ↑(Cube.splitAt i)).comp
                ↑(Cube.insertAt i)).curry
            t,
          ⋯⟩,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    p

Tactic:
ContinuousMap.comp_assoc,

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ {
      toFun := fun t ↦
        ⟨(({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp
                ((↑(Cube.splitAt i)).comp ↑(Cube.insertAt i))).curry
            t,
          ⋯⟩,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    p
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 : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
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
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ l < #J - 1

Tactic:
by_contra hl

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 : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
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
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hl : ¬l < #J - 1
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ (fun y ↦ ⟨ofDigits fun i ↦ bif y i then 2 else 0, ⋯⟩)
      ((fun x ↦
          match (motive := ↑cantorSet → ℕ → Bool) x with
          | ⟨x, h⟩ => (cantorToBinary x).get)
        ⟨x, hx⟩) =
    ⟨x, hx⟩

Tactic:
simp only [Fin.isValue, Subtype.mk.injEq]

Goal state after:
x : ℝ
hx : x ∈ cantorSet
⊢ (ofDigits fun i ↦ bif (cantorToBinary x).get i then 2 else 0) = x
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case refine_1
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ a ^ n ≤ 1 ^ n

Tactic:
exact ENNReal.pow_le_pow_left ha1

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ coveringNumber δ A ≤ coveringNumber ε A

Tactic:
coveringNumber

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ ⨅ C, ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover δ A C), C.encard ≤ ⨅ C, ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard
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
z : (l : ℕ) → ↥(s (n + l))
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k ↦ ↑(z k)
y : α
y_lim : Tendsto (fun k ↦ ↑(z k)) atTop (𝓝 y)
k : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(z x) ∈ ⋃ m, ⋃ (_ : m ≥ k), ↑(s m)

Tactic:
simp only [exists_prop, Set.mem_iUnion, Filter.eventually_atTop]
            exact ⟨k, fun m hm => ⟨n + m, by lia, (z m).2⟩⟩

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
h : ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists :
  ⨆ i, ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε) i), i.encard < ⊤ →
    ∃ i, (↑i).encard = ⨆ i, ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε) i), i.encard
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard

Tactic:
specialize h_exists h.lt_top

Goal state after:
case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ∃ i, (↑i).encard = ⨆ i, ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε) i), i.encard
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ y ∈ maximalSeparatedSet ε A, (x, y) ∉ {x | edist x.1 x.2 ≤ ↑ε}
C : Set X := {x} ∪ maximalSeparatedSet ε A
⊢ x ∉ maximalSeparatedSet ε A

Tactic:
simpa using h_dist x

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

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

Tactic:
rw [← ENNReal.coe_eq_zero, hf.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_eq_zero]

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : c = 0
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
simp [hc]

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:
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.Snowflaking

Goal state before:
pp: case mp
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C
⊢ ∃ C, ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C

Tactic:
use C ^ α

Goal state after:
case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C
⊢ ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C ^ α
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
f : ℕ → X
hf : ∀ (n : ℕ), f n ∈ U n
n m : ℕ
hm : m ∈ f ⁻¹' U n
⊢ m = n

Tactic:
exact hd.eq (not_disjoint_iff.2 ⟨f m, hf _, hm⟩)

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}} → s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
rintro ⟨F, ⟨hF, hs⟩, rfl⟩

Goal state after:
case mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
⊢ (fun f ↦ ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
S : Set L
x✝ : PT L
⊢ x✝ ∈ {x | x (sSup S)} ↔ x✝ ∈ sSup ((fun u ↦ {x | x u}) '' S)

Tactic:
simp [Prop.exists_iff]

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
L : Locale
x : X
S : Set (Opens X)
⊢ (x ∈ sSup S) = sSup ((fun x_1 ↦ x ∈ x_1) '' S)

Tactic:
simp [Prop.exists_iff]

Goal state after:
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f g : EsakiaHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝ }.toFun a ≤ b →
      ∃ c, a ≤ c ∧ { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝ }.toFun c = b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝,
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    g
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
⊢ L ≤ S

Tactic:
@IsScott.topology_eq α univ _ S _,

Goal state after:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
⊢ L ≤ scott α univ
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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝² : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁴ : 0 ≤ ε₂
this✝³ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝¹ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝³
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : 0 ≤ ε₁
x : X
x✝ : x ∈ s
⊢ dist x x ≤ ε₁

Tactic:
by simpa only [dist_self]

Goal state after:
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case e'_5
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
⊢ s.arrows (𝟙 ⊤)

Tactic:
obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X

Goal state after:
case e'_5.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
he : IsEmpty ↑X
⊢ s.arrows (𝟙 ⊤)

case e'_5.inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
⊢ s.arrows (𝟙 ⊤)