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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ -1 + ↑this.unit⁻¹ = ↑this.unit⁻¹ * -(1 + x) + ↑this.unit⁻¹ * 1

Tactic:
mul_neg,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ -1 + ↑this.unit⁻¹ = -(↑this.unit⁻¹ * (1 + x)) + ↑this.unit⁻¹ * 1
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case pos
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
x✝ : 0 < n
j : cell C n
hj : j ∈ E.I n
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

pp: case neg
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
x✝ : 0 < n
j : cell C n
hj : j ∉ E.I n
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
· exact Or.intro_right _ (h.1 n ⟨j, hj⟩)

Goal state after:
case neg
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
x✝ : 0 < n
j : cell C n
hj : j ∉ E.I n
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
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 : Finite C
h : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell C n)
⊢ _root_.Finite ((n : ℕ) × cell C n)

Tactic:
have _ := finite.finite_cell

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
h : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell C n)
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
⊢ _root_.Finite ((n : ℕ) × cell C n)
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
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ Continuous[tY, _] (⇑WithGeneratedByTopology.equiv.symm ∘ g)

Tactic:
continuous_iff (X := X)

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)
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
i : ι
⊢ Continuous[inst✝¹ i, _] ⇑WithGeneratedByTopology.equiv.symm

Tactic:
by
    rw [continuous_def]
    intro U hU
    rw [WithGeneratedByTopology.isOpen_iff] at hU
    exact hU ⟨_, continuous_id⟩

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

Goal state before:
pp: case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = true
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
· refine ⟨e (π C (· ∈ s)) a, ⟨e_mem_of_eq_true _ _ hx, ?_⟩⟩
    rw [hx] at ha
    rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg ha]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : List I
hl : List.IsChain (fun x1 x2 ↦ x1 > x2) l
hll : Products.isGood {fun x ↦ false} ⟨l, hl⟩
a✝ : List.Lex (fun x1 x2 ↦ x1 < x2) [] l
⊢ {Products.nil} ⊆ {m | m < ⟨l, hl⟩}

Tactic:
simpa only [Products.nil, Products.lt_iff_lex_lt, Set.singleton_subset_iff, Set.mem_ofPred_eq]

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

Goal state before:
pp: case refine_3
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx✝ : x ∈ C
hx : x ∈ C0 C ho ∪ C1 C ho
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx✝⟩ =
    f ⟨x, hx✝⟩

Tactic:
rcases hx with hx₀ | hx₁

Goal state after:
case refine_3.inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₀ : x ∈ C0 C ho
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩

case refine_3.inr
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₁ : x ∈ C1 C ho
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ C

Tactic:
← union_iUnion_openCell_eq_complex (C := C)

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ D ∪ ⋃ n, ⋃ j, openCell n j
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
⊢ ⋃ x, ⋃ (hx : x ∈ {x | ↑m < n}), openCell m ↑⟨x, hx⟩ = ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
iUnion_comm

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
⊢ ⋃ x, ⋃ (hx : x ∈ {x | ↑m < n}), openCell m ↑⟨x, hx⟩ = ⋃ i', ⋃ (_ : ↑m < n), openCell m i'
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)

Tactic:
← max_eq_o_cons_tail ho l hl hlh

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) ↑l
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ closure[inst✝³] (x '' Ici (k + 1)) ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}

Tactic:
refine (IsClosed.closure_subset_iff
    (isClosed_iUnion_closure_singleton_of_not_tendsto fun l φ hφ => ?_)).2 ?_

Goal state after:
case refine_1
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
l : E
φ : ℕ → ℕ
hφ : StrictMono φ
⊢ ¬Tendsto ((fun i ↦ x (i + (k + 1))) ∘ φ) atTop (𝓝 l)

case refine_2
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ x '' Ici (k + 1) ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_2
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ x '' Ici (k + 1) ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}

Tactic:
· simp only [image_eq_iUnion, mem_Ici, iUnion_ge_eq_iUnion_nat_add _ (k + 1)]
    exact iUnion_mono fun i => subset_closure

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ x1 = x2

Tactic:
apply Inseparable.eq

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable x1 x2
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑U),
    (∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X ↑U)),
    IsOpen s → IsOpen[instTopologicalSpaceSubtype] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)

Tactic:
exact fun _ hV ↦ this _ (fun a ↦
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)).isOpen_preimage _ hV)

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

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
⊢ ∀ (x : Option α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball x r)

Tactic:
by
    intro x r
    rw [h_edist]
    match x with
    | (x : α) =>
      obtain ⟨s', s'o, s's⟩ := m.topology_eq_on_restrict x r
      refine ⟨some '' s', ?_, ?_⟩
      · exact (IsOpenEmbedding.isOpen_iff_image_isOpen h).mp s'o
      ext ⟨y, yh⟩
      match y with
      | none => contradiction
      | (z : α) =>
        apply Set.ext_iff.mp at s's
        simp only [mem_preimage, Subtype.forall, Metric.mem_eball, mem_image] at s's ⊢ yh
        specialize s's z yh
        refine ⟨fun ⟨r, rh, rh'⟩ ↦ ?_, fun _ ↦ ⟨z, by tauto⟩⟩
        exact s's.1 <| h.injective rh' ▸ rh
    | none =>
      apply discreteTopology_iff_forall_isOpen.mp
      rw [ball_infty_of_pos ENNReal.zero_lt_top]
      exact Subsingleton.discreteTopology

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

Goal state before:
pp: θ : ↑I
⊢ 1 + ↑θ ≤ 2 * 1

Tactic:
mul_one,

Goal state after:
θ : ↑I
⊢ 1 + ↑θ ≤ 2
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
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
this :
  ∀ {i j : ℕ},
    i ≠ j → i < j → Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
h : j ≤ i
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

Tactic:
· exact Disjoint.symm <| this hij.symm <| (ne_iff_lt_iff_le.mpr h).mp hij.symm

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : ¬J.Nonempty
⊢ pairSetSeq J a c i ⊆ J ×ˢ J

Tactic:
simp [pairSetSeq, hJ]

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

Goal state before:
pp: case zero
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ 0 ≤ ofDigits a ∧ ofDigits a ≤ 1

Tactic:
exact ⟨ofDigits_nonneg a, ofDigits_le_one a⟩

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✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } ∈ Ω^ N X x

Tactic:
rintro y ⟨i, iH | iH⟩ <;> cases Unique.eq_default i <;> apply (congr_arg p iH).trans

Goal state after:
case inl.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 0
⊢ p 0 = x

case inr.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 1
⊢ p 1 = x
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| ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)

Tactic:
simp only [dist_eq_norm]

Goal state after:
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‖
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ ↑(2 * maxVar X Y) * dist x y

Tactic:
rintro ⟨x, y⟩ ⟨z, t⟩

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ dist (f (x, y)) (f (z, t)) ≤ ↑(2 * maxVar X Y) * dist (x, y) (z, 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_lt_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.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
by_cases hfg : MemHolder r f ∧ MemHolder r g
  · obtain ⟨hf, hg⟩ := hfg
    rw [← hf.coe_nnHolderNorm_eq_eHolderNorm, ← hg.coe_nnHolderNorm_eq_eHolderNorm,
      ← (hf.add hg).coe_nnHolderNorm_eq_eHolderNorm, ← coe_add, ENNReal.coe_le_coe]
    exact hf.nnHolderNorm_add_le hg
  · rw [Classical.not_and_iff_not_or_not, ← eHolderNorm_eq_top, ← eHolderNorm_eq_top] at hfg
    obtain (h | h) := hfg
    all_goals simp [h]

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

Goal state before:
pp: X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)

Tactic:
let s : Set γ := range Φ ∪ range Ψ

Goal state after:
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
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:
← image_toSnowflaking_eq_preimage,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set X
⊢ IsBounded (⇑toSnowflaking '' s) ↔ IsBounded s
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' eball x r ↔ { val := y } ∈ eball (toSnowflaking x) (r ^ α)

Tactic:
simp (disch := positivity) [ENNReal.rpow_lt_rpow_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsOpen[t₁] s

Tactic:
@isOpen_iff_isUpperSet α _ t₁

Goal state after:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsUpperSet s
Module: Mathlib.Topology.Order.Category.AlexDisc

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

Tactic:
by ext; apply e.apply_symm_apply

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

Goal state before:
pp: X✝ : Type u_1
inst✝ : TopologicalSpace X✝
L : Locale
X : TopCat
⊢ ∀ (s : Set (PT ↑(Opposite.unop (topToLocale.obj X)))), IsOpen s → IsOpen (localePointOfSpacePoint ↑X ⁻¹' s)

Tactic:
rintro _ ⟨u, rfl⟩; simpa using! u.2

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝¹ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 ≤ q
x✝ : α
⊢ x✝ ∈ ⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩ ↔ x✝ ∈ Ioi x

Tactic:
simp [some, Prod.Lex.lt_iff, hq.not_gt]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : ∃ a, S = (hull T a)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S

Tactic:
obtain ⟨a, ha⟩ := h
    exact ⟨(Ici a)ᶜ, isClosed_Ici.isOpen_compl, ha.symm⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝¹ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
x✝ : α
⊢ x✝ ∈ ⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩ ↔ x✝ ∈ Iio x

Tactic:
simp [some, Prod.Lex.lt_iff, hq.not_gt]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[lawson α] s ↔ IsOpen[scott α univ] s

Tactic:
exact lawsonOpen_iff_scottOpen_of_isUpperSet h

Goal state after: