mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.DeriveCountable

Goal state before:
pp: p : Prop
a b b' : ℕ
h : b = b' → p
⊢ Nat.pair a b = Nat.pair a b' → p

Tactic:
simpa [Nat.pair_eq_pair, and_imp] using h

Goal state after:
Module: Mathlib.Tactic.DeriveCountable

Goal state before:
pp: p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ Nat.pair a b = Nat.pair a' b' → p

Tactic:
Nat.pair_eq_pair,

Goal state after:
p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ a = a' ∧ b = b' → p
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1

Tactic:
by
  rw [Nat.blt_eq] at hb
  rw [Nat.blt_eq, ← Nat.lt_clog_iff_pow_lt hb] at h₁
  rw [Nat.ble_eq, ← Nat.clog_le_iff_le_pow hb] at h₂
  lia

Goal state after:
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: m b : ℕ
hk₁ : m < b
hk₂ : b ^ 2 ≤ m ^ 2 + 2 * m
⊢ False

Tactic:
rw [← Nat.add_one_le_iff, ← Nat.pow_le_pow_iff_left two_ne_zero] at hk₁

Goal state after:
m b : ℕ
hk₁ : (m + 1) ^ 2 ≤ b ^ 2
hk₂ : b ^ 2 ≤ m ^ 2 + 2 * m
⊢ False
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ 0 ≤ x

Tactic:
simp only [hx_eq, invOf_eq_inv]; positivity

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ Irrational (x ^ (1 / 2))

Tactic:
apply irrational_rpow_rat_rat_of_num hx_isNNRat (y_num := 1) (y_den := 2) _ hx_coprime (by simp)
    hn1 hn2

Goal state after:
x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ IsNNRat (1 / 2) 1 2
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x

Tactic:
apply h₀; apply List.mem_of_getElem? h₂

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hy : ∃ i, xs[i]? = some y
i : ℕ
hx : xs[i]? = some x
⊢ x = y

Tactic:
obtain ⟨j, hy⟩ := hy

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
i : ℕ
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
⊢ x = y
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F

Tactic:
eq_univ_iff_forall

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing F

Tactic:
eq_univ_iff_forall

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing F
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
eq_univ_iff_forall

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f ≫ e.hom) = f ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map e.hom

Tactic:
change eta G ≫ ((forget₂ _ _).map ((_ ≫ e.inv) ≫ e.hom)) = _

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ eta G ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map
        ((((limitConeIsLimit P.diagram).liftConeMorphism
                { pt := (limitCone (diagram G)).pt,
                  π :=
                    { app := fun H ↦ (limitCone (diagram G)).π.app (preimage f H) ≫ ofFiniteGrpHom (quotientMap f H),
                      naturality := ⋯ } }).hom ≫
            e.inv) ≫
          e.hom) =
    f ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map e.hom
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
⊢ LocallyCompactSpace (PontryaginDual H)

Tactic:
let Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
⊢ LocallyCompactSpace (PontryaginDual H)
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
t : Set (ULift.{?u.17, 0} ↑(Metric.closedBall 0 1))
x✝ : IsOpen t
s : Set ↑(Metric.closedBall 0 1)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs : Subtype.val ⁻¹' r = s
hst : ULift.down ⁻¹' s = t
⊢ ∃ t,
    IsOpen t ∧
      ULift.down ⁻¹' t =
        (fun x ↦
            match x with
            | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ }) ⁻¹'
          ULift.down ⁻¹' s

Tactic:
← hrs

Goal state after:
n : ℕ
t : Set (ULift.{?u.17, 0} ↑(Metric.closedBall 0 1))
x✝ : IsOpen t
s : Set ↑(Metric.closedBall 0 1)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs : Subtype.val ⁻¹' r = s
hst : ULift.down ⁻¹' s = t
⊢ ∃ t,
    IsOpen t ∧
      ULift.down ⁻¹' t =
        (fun x ↦
            match x with
            | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ }) ⁻¹'
          ULift.down ⁻¹' Subtype.val ⁻¹' r
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case inl
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
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
h : P ∈ C0
⊢ P.Nonempty

Tactic:
exact claim2 _ h

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Tactic:
have := RelCWComplex.union' (C := C)
  rw [empty_union] at this
  exact this

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
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ C

Tactic:
simp_rw [← union]
  exact subset_union_of_subset_right (subset_iUnion₂ _ _) _

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen U → U ∈ F := by
      intro U F h1 hU
      exact isOpen_iff_ultrafilter.mp hU _ h1 _ (Ultrafilter.le_nhds_lim _)

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed (C0 C ho)

Tactic:
refine hC.inter ?_
  have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)
  exact IsClosed.preimage h (t := {false}) (isClosed_discrete _)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case inr
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
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o = ord I i
⊢ false = x i

Tactic:
· simp only [C0, Set.mem_inter_iff, Set.mem_ofPred_eq] at hx
    rw [eq_comm, ord_term ho] at hi
    rw [← hx.2, hi]

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 F : Subcomplex C
h : (fun E ↦ E.carrier) E = (fun E ↦ E.carrier) F
⊢ E = F

Tactic:
obtain ⟨E, _, _, hE⟩ := E

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
F : Subcomplex C
E : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
h : (fun E ↦ E.carrier) { carrier := E, I := I✝, closed' := closed'✝, union' := hE } = (fun E ↦ E.carrier) F
⊢ { carrier := E, I := I✝, closed' := closed'✝, union' := hE } = F
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ ∃ f', f' ≫ g = f

Tactic:
use CompHausLike.ofHom _ ⟨h, hh⟩

Goal state after:
case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := ⋯
h : Ultrafilter X → ↑Y.toTop := ⋯
hh : Continuous h
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := h, continuous_toFun := hh } ≫ g = f
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ↑(skeletonLT C n) ∩ openCell m j ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
rw [(disjoint_skeletonLT_openCell hnm).inter_eq]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ∅ ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j
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₀ : α), EquicontinuousAt (fun x ↦ ⇑↑x) x₀
⊢ IsCompact A

Tactic:
Metric.equicontinuousAt_iff_pair

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') < ε
⊢ IsCompact A
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 ⊥
⊢ (f.concat g).comp IccInclusionLeft = f

Tactic:
ext x
  simp [concat, IccExtendCM, hb, IccInclusionLeft, projIccCM, inclusion, x.2.2]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst✝] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable ↑b
⊢ A ⊆ ⋃ i, U ↑i

Tactic:
simpa using hAU

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

Goal state before:
pp: case inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
Hj : y j = 0 ∨ y j = 1
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

Tactic:
rcases Hj with Hj | Hj <;> simp only [Hj, p.coe_toContinuousMap, p.source, p.target] <;> rfl

Goal state after:
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter]
  -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
    refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
  -- In `X × Filter X`, consider the closed set `F := closure {(x, ℱ) | ℱ = pure x}`
    let F : Set (X × Filter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
  -- Since `f × id` is closed, the set `(f × id) '' F` is also closed.
    have := H.2 F isClosed_closure
  -- Let us show that `(y, 𝒰) ∈ (f × id) '' F`.
    have : (y, ↑𝒰) ∈ Prod.map f id '' F :=
  -- Note that, by the properties of the topology on `Filter X`, the function `pure : X → Filter X`
  -- tends to the point `𝒰` of `Filter X` along the filter `𝒰` on `X`. Since `f` tends to `y` along
  -- `𝒰`, we get that the function `(f, pure) : X → (Y, Filter X)` tends to `(y, 𝒰)` along
  -- `𝒰`. Furthermore, each `(f, pure)(x) = (f × id)(x, pure x)` is clearly an element of
  -- the closed set `(f × id) '' F`, thus the limit `(y, 𝒰)` also belongs to that set.
      this.mem_of_tendsto (hy.prodMk_nhds (Filter.tendsto_pure_self (𝒰 : Filter X)))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
  -- The above shows that `(y, 𝒰) = (f x, 𝒰)`, for some `x : X` such that `(x, 𝒰) ∈ F`.
    rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
  -- We already know that `f x = y`, so to finish the proof we just have to check that `𝒰` tends
  -- to `x`. So, for `U ∈ 𝓝 x` arbitrary, let's show that `U ∈ 𝒰`. Since `𝒰` is an ultrafilter,
  -- it is enough to show that `Uᶜ` is not in `𝒰`.
    refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
    rw [mem_closure_iff_nhds] at hx
  -- Indeed, if that was the case, the set `V := {𝒢 : Filter X | Uᶜ ∈ 𝒢}` would be a neighborhood
  -- of `𝒰` in `Filter X`, hence `U ×ˢ V` would be a neighborhood of `(x, 𝒰) : X × Filter X`.
  -- But recall that `(x, 𝒰) ∈ F = closure {(x, ℱ) | ℱ = pure x}`, so the neighborhood `U ×ˢ V`
  -- must contain some element of the form `(z, pure z)`. In other words, we have `z ∈ U` and
  -- `Uᶜ ∈ pure z`, which means `z ∈ Uᶜ` by the definition of pure.
  -- This is a contradiction, which completes the proof.
    rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOfPred_mem.mem_nhds hUc)) with
      ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩
    exact hz' hz

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

Goal state before:
pp: case singleton
X : Type u_1
R : Type u_2
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
Y : Type u_3
f : Y → PseudoMetric X R
s : Finset Y
x y : X
i : Y
⊢ ({i}.sup f) x y = {i}.sup' ⋯ fun i ↦ (f i) x y

Tactic:
| singleton i =>

Goal state after:
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 := 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
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
have htB : t ∈ (logSizeBallSeq J hJ a c l).ball c := by
    simp only [logSizeBallStruct.ball, Finset.mem_filter, htV, true_and]
    apply le_trans (edist_triangle _ s _)
    apply le_of_le_of_eq (add_le_add h hst)
    nth_rw 3 [← one_mul c]
    rw [← add_mul]
    congr
    rw [ENNReal.sub_add_eq_add_sub _ (ENNReal.one_ne_top),
      ENNReal.add_sub_cancel_right (ENNReal.one_ne_top)]
    rw [← Nat.cast_one]
    gcongr
    exact one_le_radius_logSizeBallSeq hJ ha l

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
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n

Tactic:
simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]

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

Goal state before:
pp: case h₂
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤ ‖embeddingOfSubset x b - embeddingOfSubset x a‖

Tactic:
exact lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n

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

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
refine (coveringNumber_le_packingNumber _ A).trans ?_

Goal state after:
case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ packingNumber (2 * ε) A ≤ externalCoveringNumber ε A
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case right
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ Subtype.val '' univ = ↑p

Tactic:
Set.image_univ,

Goal state after:
case right
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ range Subtype.val = ↑p
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ ball x r = ⇑toSnowflaking '' ball (ofSnowflaking x) (r ^ α⁻¹)

Tactic:
image_toSnowflaking_ball _ (by positivity),

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ ball x r = ball (toSnowflaking (ofSnowflaking x)) ((r ^ α⁻¹) ^ α)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure[inst✝¹] s ⊆ ↑(lowerClosure s)

Tactic:
apply closure_minimal subset_lowerClosure _

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsClosed[inst✝¹] ↑(lowerClosure s)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
x y : α
h : Inseparable x y
⊢ Ici x = Ici y

Tactic:
simpa only [inseparable_iff_closure_eq, closure_singleton] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝¹ : TopologicalSpace (α × β) := lower (α × β)
a : α
x✝ : a ∈ s
⊢ (Ici (a, ⊥))ᶜ = (Prod.fst ⁻¹' Ici a)ᶜ

Tactic:
by simp [Ici_prod_eq, prod_univ]

Goal state after: