mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
J : (g'⁻¹ • V) • {x} ∈ 𝓝 x
⊢ (g'⁻¹ • V) • {x} ⊆ U • {x}

Tactic:
apply smul_subset_smul_right

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := ⋯
F : ℕ × ↑s → Set X := ⋯
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
J : (g'⁻¹ • V) • {x} ∈ 𝓝 x
⊢ g'⁻¹ • V ⊆ U
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝¹ : DivInvMonoid G
inst✝ : TopologicalSpace G
x y : G
⊢ ClusterPt x (map (fun x ↦ y ^ x) atTop) ↔ ClusterPt x (map (fun x ↦ y ^ x) atTop)

Tactic:
← Nat.map_cast_int_atTop,

Goal state after:
G : Type u_1
inst✝¹ : DivInvMonoid G
inst✝ : TopologicalSpace G
x y : G
⊢ ClusterPt x (map (fun x ↦ y ^ x) (map Nat.cast atTop)) ↔ ClusterPt x (map (fun x ↦ y ^ x) atTop)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
⊢ ProfiniteCompletion.lift (𝟙 G ≫ ProfiniteCompletion.eta G) = 𝟙 (ProfiniteCompletion.completion G)

Tactic:
apply ProfiniteCompletion.lift_unique

Goal state after:
G : GrpCat
⊢ ProfiniteCompletion.eta G ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map (ProfiniteCompletion.lift (𝟙 G ≫ ProfiniteCompletion.eta G)) =
    ProfiniteCompletion.eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (𝟙 (ProfiniteCompletion.completion G))
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: X✝ Y✝ Z✝ : GrpCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ProfiniteCompletion.lift ((f ≫ g) ≫ ProfiniteCompletion.eta Z✝) =
    ProfiniteCompletion.lift (f ≫ ProfiniteCompletion.eta Y✝) ≫
      ProfiniteCompletion.lift (g ≫ ProfiniteCompletion.eta Z✝)

Tactic:
apply ProfiniteCompletion.lift_unique

Goal state after:
X✝ Y✝ Z✝ : GrpCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ProfiniteCompletion.eta X✝ ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map (ProfiniteCompletion.lift ((f ≫ g) ≫ ProfiniteCompletion.eta Z✝)) =
    ProfiniteCompletion.eta X✝ ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map
        (ProfiniteCompletion.lift (f ≫ ProfiniteCompletion.eta Y✝) ≫
          ProfiniteCompletion.lift (g ≫ ProfiniteCompletion.eta Z✝))
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ ∑' (ab : ↑(mulFiber x)), (L (if (↑ab).1 ∈ {1} then e else 0)) (f (↑ab).2) = f x

Tactic:
tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ (L (if (↑⟨(1, x), ⋯⟩).1 ∈ {1} then e else 0)) (f (↑⟨(1, x), ⋯⟩).2) = f x
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
⊢ Tendsto f (residual α) (residual β)

Tactic:
by
  apply le_countableGenerate_iff_of_countableInterFilter.mpr
  rintro t ⟨ht, htd⟩
  exact residual_of_dense_open (ht.preimage hc) (htd.preimage ho)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
⊢ ∀ ⦃e : cell C 1⦄, e ∈ univ → Std.Symm fun x y ↦ cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y

Tactic:
by grind [symm_def]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
⊢ (∃ x, (OneSkeletonGraph C).IsLoopAt e x) ↔ (cellFrontier 1 e).Subsingleton

Tactic:
exists_isLoopAt_iff

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
⊢ (∃ x, cellFrontier 1 e = closedCell 0 x) ↔ (cellFrontier 1 e).Subsingleton
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ⋃ n, ⋃ j, openCell n ↑j ⊆ ⋃ n, ⋃ j, closedCell n ↑j

Tactic:
apply iUnion₂_mono fun n i ↦ ?_

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
⊢ openCell n ↑i ⊆ closedCell n ↑i
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ↑E ⊆ D ∪ ⋃ n, ⋃ j, closedCell n ↑j

Tactic:
· rw [← E.union]
    apply union_subset_union_right
    apply iUnion₂_mono fun n i ↦ ?_
    exact openCell_subset_closedCell (C := C) n i

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
h : i ∉ E.I n
⊢ Disjoint (openCell n i) ↑E

Tactic:
simp_rw [← union, disjoint_union_right, disjoint_iUnion_right]
  exact ⟨disjointBase n i , fun _ _ ↦ disjoint_openCell_of_ne (by lia)⟩

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : IsEmpty ((n : ℕ) × cell C n)
⊢ ∀ (b : ℕ), 0 ≤ b → IsEmpty (cell C b)

Tactic:
by simp_all

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ generatedBy X = coinduced (fun x ↦ x.fst.snd x.snd) inferInstance

Tactic:
rw [generatedBy, instTopologicalSpaceSigma, coinduced_iSup, iSup_sigma]
  rfl

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
⊢ (∀ (i : ι) (i_1 : C(X i, Y)), Continuous[TopologicalSpace.coinduced (⇑i_1) inferInstance, inst✝] g) ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)

Tactic:
exact forall_congr' (fun i ↦ forall_congr'
    (fun f ↦ (by rw [continuous_coinduced_dom]; simp [equiv, Equiv.refl])))

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
hg : Continuous[inst✝¹, inst✝] g
⊢ ContinuousGeneratedBy X g

Tactic:
by
  rw [continuousGeneratedBy_def]
  exact fun _ f ↦ hg.comp f.continuous

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 : ℕ
i : cell C n
⊢ ↑(map n i) '' (sphere 0 1 ∪ ball 0 1) = ↑(map n i) '' closedBall 0 1

Tactic:
congrm map n i '' ?_

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ sphere 0 1 ∪ ball 0 1 = closedBall 0 1
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
this : D ∪ ⋃ n, ⋃ j, openCell n j = D ∪ ⋃ m, ⋃ (_ : ↑m < ⊤), ⋃ j, closedCell m j
⊢ D ∪ ⋃ n, ⋃ j, openCell n j = C

Tactic:
by
    simpa [union] using this

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ ((1 - e (π C fun x ↦ x ∈ s) a) * c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
noncomm_ring

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) +
      -1 • (e (π C fun x ↦ x ∈ s) a * c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
⊢ Products.eval C l ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
suffices L l by assumption

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
⊢ L l
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
⊢ (∀ o' < o, P I o') → P I o

Tactic:
intro h hho C hC hsC

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndependent ℤ (eval C)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: S : Profinite
⊢ IsClosedEmbedding (ι S)

Tactic:
by
  classical
  apply Continuous.isClosedEmbedding
  · dsimp +unfoldPartialApp [ι]
    refine continuous_pi ?_
    intro C
    rw [← IsLocallyConstant.iff_continuous]
    refine ((IsLocallyConstant.tfae _).out 0 3).mpr ?_
    rintro ⟨⟩
    · refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)
      convert! C.2
      ext x
      simp
    · refine IsClopen.isOpen ?_
      convert! C.2
      ext x
      simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]
  · intro a b h
    by_contra hn
    obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn
    apply hh.2 ∘ of_decide_eq_true
    dsimp +unfoldPartialApp [ι] at h
    rw [← congr_fun h ⟨C, hC⟩]
    exact decide_eq_true hh.1

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

Goal state before:
pp: case refine_2
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
l : Products I
h : Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
hh : Products.isGood (π C fun x ↦ ord I x < o) l
this : Products.isGood (π C fun x ↦ ord I x < Order.succ o) l
⊢ Products.isGood C l

Tactic:
contained_eq_proj C (Order.succ o) hsC

Goal state after:
case refine_2
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
l : Products I
h : Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
hh : Products.isGood (π C fun x ↦ ord I x < o) l
this : Products.isGood (π C fun x ↦ ord I x < Order.succ o) l
⊢ Products.isGood (π C fun x ↦ ord I x < Order.succ o) l
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
n : ℕ
⊢ dissipate C (n + 1) ⊆ dissipate C n

pp: case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ IsCompact (dissipate C 0)

Tactic:
· exact Set.antitone_dissipate (by lia)

Goal state after:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ IsCompact (dissipate C 0)
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_2
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
U : ι → Set E
this : Countable ↑b
t : Finset ↑b
ht : A ⊆ ⋃ i ∈ t, U ↑i
hUo : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (U ↑x)
hAU : A ⊆ ⋃ x, U ↑x
hb : Countable ↑b
d : Finset { a // a ∈ b }
hd : A ⊆ ⋃ i ∈ d, U ↑i
⊢ A ⊆ ⋃ i ∈ Subtype.val '' ↑d, U i

Tactic:
· rwa [biUnion_image]

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

Goal state before:
pp: 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 ι
f : ℕ → ι
hf : A ⊆ ⋃ n, U (f n)
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, (U ∘ f) i
⊢ A ⊆ ⋃ i ∈ Finset.image f t, U i

Tactic:
by simp_all

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

Goal state before:
pp: 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 : IsEmpty ι
⊢ A ⊆ ⋃ i ∈ ∅, U i

Tactic:
by simp_all

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

Goal state before:
pp: case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
hG : Continuous G
x : X
y : Y
⊢ { toFun := G, continuous_toFun := hG }.toFun (1, x, y) = (ContinuousMap.id (X × Y)) (x, y)

Tactic:
exact Prod.ext (HSpace.hmulE.1.3 x) (HSpace.hmulE.1.3 y)

Goal state after:
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✝ i : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).radius ≤ n

Tactic:
simp only [radius_logSizeBallSeq_add_one, logSizeRadius, ha, ↓reduceDIte]
    refine Nat.find_min' _ ⟨hn, le_trans ?_ hJ_card⟩
    gcongr
    exact (Finset.filter_subset _ _).trans (finset_logSizeBallSeq_subset_logSizeBallSeq_init _ _)

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
⊢ Tendsto f (𝓝 []) (r [])

Tactic:
by rwa [nhds_nil]

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

Goal state before:
pp: case h
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
C : Set X
⊢ ⨅ (_ : IsCover δ A C), C.encard ≤ ⨅ (_ : IsCover ε A C), C.encard

Tactic:
exact iInf_const_mono (fun h_cover ↦ h_cover.mono_radius h)

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

Goal state before:
pp: case h
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
C : Set X
x✝ : C ⊆ A
⊢ ⨅ (_ : IsCover δ A C), C.encard ≤ ⨅ (_ : IsCover ε A C), C.encard

Tactic:
exact iInf_const_mono (fun h_cover ↦ h_cover.mono_radius h)

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

Goal state before:
pp: case inr.refine_1
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 }
C : { s // s ⊆ A ∧ IsSeparated (↑ε) s }
hC : (↑C).encard = ⨆ i, ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε) i), i.encard
⊢ (↑C).encard ≠ ⊤

Tactic:
rwa [hC]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := fun x ↦ ⟨⋯.choose, ⋯⟩
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ edist ↑x ↑(f x) + edist ↑(f x) ↑y ≤ 2 * ↑ε

Tactic:
by
      rw [two_mul]
      gcongr
      · exact hf' x
      · simpa [edist_comm, hxy] using hf' y

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

Goal state before:
pp: case pos.refine_2
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
hf : MemHolder r f
x₁ x₂ : X
⊢ edist (c • f x₁) (c • f x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r

Tactic:
← Pi.smul_apply,

Goal state after:
case pos.refine_2
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
hf : MemHolder r f
x₁ x₂ : X
⊢ edist ((c • f) x₁) (c • f x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set X
⊢ IsBounded (⇑ofSnowflaking ⁻¹' s) ↔ IsBounded s

Tactic:
rw [← image_toSnowflaking_eq_preimage, isBounded_image_toSnowflaking_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] s ↔ ScottContinuousOn univ fun x ↦ x ∈ s

Tactic:
scottContinuousOn_iff_continuous (fun _ _ _ ↦ by trivial)

Goal state after:
α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] s ↔ Continuous[inst✝¹, _] fun x ↦ x ∈ s
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (x, r), ⋯⟩

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_between h
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · grind [ofLex_toLex]
      · simp [Prod.Lex.lt_iff, hs, hs']

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

Goal state before:
pp: case refine_1
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ ghDist X Y

pp: case refine_2
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ ghDist X Y ≤ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y))

Tactic:
· apply le_csInf
    · refine (Set.Nonempty.prod ?_ ?_).image _ <;> exact ⟨_, rfl⟩
    · rintro b ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩
      exact B p q hp hq

Goal state after:
case refine_2
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ ghDist X Y ≤ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y))
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ Continuous fun s ↦ WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ))

Tactic:
continuous_iff_continuousAt,

Goal state after:
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ ∀ (x_1 : ↑(base ⁻¹' ↑U)),
    ContinuousAt (fun s ↦ WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ))) x_1