mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
⊢ ⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)

Tactic:
have : l.eval (π C J) ∘ Homeomorph.setCongr (proj_eq_of_subset C J K hJK) =
      l.eval (π (π C K) J) := by
    ext; simp [Homeomorph.setCongr, Products.eval_eq]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)
⊢ ⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h
S : Profinite
⊢ Continuous (ι S)

Tactic:
dsimp +unfoldPartialApp [ι]

Goal state after:
case h
S : Profinite
⊢ Continuous fun s C ↦ decide (s ∈ ↑C)
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 : ℕ∞
h : m ≤ n
⊢ ↑(skeletonLT C m) ⊆ ↑(skeletonLT C n)

Tactic:
by
  simp_rw [coe_skeletonLT]
  apply union_subset_union_right
  intro x xmem
  simp_rw [mem_iUnion, exists_prop] at xmem ⊢
  obtain ⟨l, lltm, xmeml⟩ := xmem
  exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩

Goal state after:
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β
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (↑⟨f, hf⟩ x) (↑⟨g, hg⟩ x) ≤ ε₁

Tactic:
calc
    dist (f x) (g x) ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') :=
      dist_triangle4_right _ _ _ _
    _ ≤ ε₂ + ε₂ + ε₁ / 2 := by
      refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
      · exact (hU x').2.2 _ hx' _ (hU x').1 hf
      · exact (hU x').2.2 _ hx' _ (hU x').1 hg
      · have F_f_g : F (f x') = F (g x') :=
          (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :)
        calc
          dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) :=
            dist_triangle_right _ _ _
          _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
          _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
          _ = ε₁ / 2 := add_halves _
    _ = ε₁ := by rw [add_halves, add_halves]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t

Tactic:
rw [hT.open_eq_sUnion' hU, mapsTo_iff_image_subset, sUnion_eq_biUnion] at hfKU
      obtain ⟨t, ht, hfin, htK⟩ :=
        (hK.image (map_continuous f)).elim_finite_subcover_image (fun V hV ↦ hT.isOpen hV.1) hfKU
      refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩
      rwa [sUnion_eq_biUnion]

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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
⊢ Continuous fun fg ↦ (↑fg).1.concat (↑fg).2

Tactic:
change Continuous (S.domRestrict concat.uncurry)

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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
⊢ Continuous (S.domRestrict (Function.uncurry concat))
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_2
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
⊢ MapsTo (⇑f) (Subtype.val '' (K U) n) V

Tactic:
· rw [mapsTo_image_iff]
      exact fun y _ ↦ hUV y.2

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
i : PreconnectedSpace X
h : ∀ (x : X), (↑f).IsConstant
x x' : X
⊢ x ∈ univ

Tactic:
trivial

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
i : PreconnectedSpace X
h : ∀ (x : X), (↑f).IsConstant
x x' : X
⊢ x' ∈ univ

Tactic:
trivial

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

Goal state before:
pp: m : ℕ
⊢ preCantorSet (m + 1) ⊆ preCantorSet m

Tactic:
induction m with

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

Goal state before:
pp: case neg
x : ℝ
n : ℕ
h✝ : ¬(0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3)
⊢ 3 * (Stream'.iterate cantorStep x).get n - 2 =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (2 * (3 ^ (n + 1))⁻¹))

Tactic:
field

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ 𝓝 as = traverse 𝓝 as

Tactic:
refine nhds_mkOfNhds _ _ ?_ ?_

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

case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ ∀ (a : List α), ∀ s ∈ traverse 𝓝 a, ∀ᶠ (y : List α) in traverse 𝓝 a, s ∈ traverse 𝓝 y
Module: Mathlib.Topology.List

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

pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ ∀ (a : List α), ∀ s ∈ traverse 𝓝 a, ∀ᶠ (y : List α) in traverse 𝓝 a, s ∈ traverse 𝓝 y

Tactic:
· intro l
    induction l with
    | nil => exact le_rfl
    | cons a l ih =>
      suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
        simpa only [functor_norm] using! this
      exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ ∀ (a : List α), ∀ s ∈ traverse 𝓝 a, ∀ᶠ (y : List α) in traverse 𝓝 a, s ∈ traverse 𝓝 y
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
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ edist t s ≤ c

Tactic:
rw [edist_comm]

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
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ edist s t ≤ c
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
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
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
rw [edist_comm]

Goal state after:
case inr
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
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
⊢ edist (f ↑↑⟨⟨t, ht⟩, hst⟩) (f ↑⟨s, hs⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
⊢ ∀ (a b : PseudoMetric X R), a ≤ a ⊔ b

Tactic:
by simp [← PseudoMetric.coe_le_coe]

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
⊢ ∀ (a b : PseudoMetric X R), b ≤ a ⊔ b

Tactic:
by simp [← PseudoMetric.coe_le_coe]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Tendsto (fun p ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 ((a' :: l).insertIdx (n + 1) a))

Tactic:
have : 𝓝 a ×ˢ 𝓝 (a'::l) =
        (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1::p.2.2) := by
      simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
      simp [-Filter.map_def, Function.comp_def, functor_norm]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto (fun p ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 ((a' :: l).insertIdx (n + 1) a))
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
x✝ : α × α
| edist x✝.1 x✝.2 < δ

Tactic:
rw [edist_comm]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
x✝ : α × α
| edist x✝.2 x✝.1 < δ
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := ⋯
l : ℕ := ⋯
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
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
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f ↑⟨s, hs⟩) (f (logSizeBallSeq J hJ a c l).point) +
      edist (f (logSizeBallSeq J hJ a c l).point) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤
    (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
rw [edist_comm]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := 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
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f (logSizeBallSeq J hJ a c l).point) (f ↑⟨s, hs⟩) +
      edist (f (logSizeBallSeq J hJ a c l).point) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤
    (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 ≤ δ} (s, t).1
x✝ : α × α
| edist x✝.1 x✝.2 ≤ δ

Tactic:
rw [edist_comm]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 ≤ δ} (s, t).1
x✝ : α × α
| edist x✝.2 x✝.1 ≤ δ
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' := ⋯ }
⊢ ∃ x, Tendsto s atTop (𝓝 x)

Tactic:
use t

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := ⋯
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 α := ⋯
t : Closeds α := ⋯
⊢ Tendsto s atTop (𝓝 t)
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:
← eHolderNorm_ne_top,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = ∞ ↔ ¬eHolderNorm r f ≠ ∞
Module: Mathlib.Topology.MetricSpace.Infsep

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

Tactic:
by
  simp_rw [← lt_top_iff_ne_top, einfsep_lt_top]

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⨅ d, uncurry edist ↑d

Tactic:
simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

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
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
⊢ edist x₁ x₂ ^ ↑r ≠ ∞

Tactic:
simp [(edist_lt_top x₁ x₂).ne]

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

Goal state before:
pp: case e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ edist x y = edist y x

Tactic:
rw [edist_comm]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
rw [edist_comm]

Goal state after:
case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y
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
⊢ MemHolder r (c • f) ↔ MemHolder r f

Tactic:
refine ⟨fun ⟨h, hh⟩ => ⟨h * ‖c‖₊⁻¹, ?_⟩, .smul⟩
  rw [← HolderWith.smul_iff _ hc, inv_mul_cancel_right₀ hc]
  exact hh

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

Goal state before:
pp: α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
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)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
have := fun i => exists_pos_lt_subset_ball (hr i) (hvc i) (hcv i)

Goal state after:
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
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)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r' ∈ Ioo 0 (r i), v i ⊆ ball (c i) r'
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h : DiscreteTopology X
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)

pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h : ¬DiscreteTopology X
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
· refine ⟨fun n ↦ {Infinite.natEmbedding X n}, fun _ ↦ singleton_nonempty _,
      fun _ ↦ isOpen_discrete _, fun _ _ h ↦ ?_⟩
    simpa using h

Goal state after:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h : ¬DiscreteTopology X
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case h.right
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ U = ⋃₀ {U}

Tactic:
sUnion_singleton

Goal state after:
case h.right
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ U = U
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⟩)
    · exact isOpen_univ
    · exact isClosed_Iic.isOpen_compl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
x✝² x✝¹ : α
x✝ : x✝² ≤ x✝¹
⊢ {x✝², x✝¹} ∈ univ

Tactic:
trivial

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

Goal state before:
pp: α β : AlexDisc
e : ↑α.toTopCat ≃ₜ ↑β.toTopCat
⊢ ConcreteCategory.ofHom ↑e.symm ≫ ConcreteCategory.ofHom ↑e = 𝟙 β

Tactic:
ext; apply e.apply_symm_apply

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

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ c.ι.app (op (unop U)) = c.ι.app U

Tactic:
simp only [eqToHom_trans_assoc,
        eqToHom_refl, Category.id_comp, op_unop]

Goal state after: