mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case neg.e_a
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ PiNat.firstDiff ↑(Seq.cons x s) ↑(Seq.cons x t) = PiNat.firstDiff ↑s ↑t + 1

Tactic:
simp only [val_cons, PiNat.firstDiff, ne_eq, Classical.dite_not, Subtype.coe_ne_coe.mpr h,
    not_false_eq_true, ↓reduceDIte, val_eq_get]

Goal state after:
case neg.e_a
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ (if h : some x :: ↑s = some x :: ↑t then 0 else Nat.find ⋯) = Nat.find ⋯ + 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
hF : ContractingWith 2⁻¹ F
⊢ ∃ f, Function.IsFixedPt F f

Tactic:
let f := hF.fixedPoint _

Goal state after:
α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
hF : ContractingWith 2⁻¹ F
f : β →ᵤ Stream'.Seq α := ContractingWith.fixedPoint F hF
⊢ ∃ f, Function.IsFixedPt F f
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
⊢ (op nil).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' nil.tail))
      (match nil.head with
      | none =>
        match (op nil).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
generalize op nil = t
    cases t <;> simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
m1 m2 : UnitMonomial
h_lt : m1 < m2
h_basis : WellFormedBasis []
h1 : List.length m1 = [].length
h2 : List.length m2 = [].length
⊢ m1.toFun [] =o[atTop] m2.toFun []

Tactic:
simp only [List.length_nil, List.length_eq_zero_iff] at h1 h2
    simp [h1, h2] at h_lt

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
⊢ ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.nil ∧
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ exp_1 coef_1 tl_1,
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp_1 coef_1 tl_1 ∧
        coef_1.Approximates ∧
          Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp_1 ∧
            motive
              (mk tl_1 (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp_1 * coef_1.toFun))

Tactic:
obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
    refine .inr ⟨exp, coef, tl, ?_⟩
    simp only [mk_replaceFun, mk_seq, h_coef, mk_toFun, true_and]
    simp only [mk_toFun] at h_eq
    refine ⟨h_maj.of_eventuallyEq h_eq.symm, mk tl (g - basis_hd ^ exp * coef.toFun), _, rfl,
      h_tl, ?_⟩
    grw [mk_toFun, h_eq]

Goal state after:
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
⊢ ↑n = n

Tactic:
cast_id

Goal state after:
n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
⊢ n = n
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y} ⊆ Set.range toContinuousMap

Tactic:
rintro f ⟨h1, hmul⟩

Goal state after:
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f : C(A, B)
h1 : f 1 = 1
hmul : ∀ (x y : A), f (x * y) = f x * f y
⊢ f ∈ Set.range toContinuousMap
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
x : G
x✝¹ : x ∈ Set.univ
y : G
x✝ : y ∈ Set.univ
hxy : x ≠ y
V : OpenSubgroup G
dxy : Disjoint (x • ↑V) (y • ↑V)
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨_, _, V.isOpen.smul x, (V.isClosed.smul x).isOpen_compl, mem_own_leftCoset ..,
      dxy.subset_compl_left <| mem_own_leftCoset .., by simp, disjoint_compl_right⟩

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: case zero
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ IsClosed sᵈ[0]

Tactic:
simpa only [iteratedDerivedSet_zero]

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✝¹ : 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), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
j

Goal state after:
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
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
f : (m : ℕ) → Finset (cell C m)
u : cell C 0
hu : u ∈ f 0
hun1 : ↑(map 1 e) (-1) = ↑(map 0 u) ![]
v : cell C 0
hv : v ∈ f 0
hv1 : ↑(map 1 e) 1 = ↑(map 0 v) ![]
⊢ ∃ x y, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y

Tactic:
use u, v

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
f : (m : ℕ) → Finset (cell C m)
u : cell C 0
hu : u ∈ f 0
hun1 : ↑(map 1 e) (-1) = ↑(map 0 u) ![]
v : cell C 0
hv : v ∈ f 0
hv1 : ↑(map 1 e) 1 = ↑(map 0 v) ![]
⊢ cellFrontier 1 e = closedCell 0 u ∪ closedCell 0 v
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
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
⊢ (Ultrafilter.map Ultrafilter.lim FF).lim ∈ U

Tactic:
rwa [← c1]

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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
⊢ ∀ (j : cell C n), IsClosed[t] (A ∩ closedCell n j)

Tactic:
j

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
j : cell C n
⊢ IsClosed[t] (A ∩ closedCell n j)
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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : 0 < n
⊢ ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
j

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : 0 < n
j : cell C n
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
x✝ : { l // Products.isGood ∅ l }
l : Products I
hl : Products.isGood ∅ l
⊢ Products.eval ∅ l ∈ Submodule.span ℤ (Products.eval ∅ '' {m | m < l})

Tactic:
rw [subsingleton_iff.mp inferInstance (Products.eval ∅ l) 0]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
x✝ : { l // Products.isGood ∅ l }
l : Products I
hl : Products.isGood ∅ l
⊢ 0 ∈ Submodule.span ℤ (Products.eval ∅ '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x w✝ : I → Bool
left✝ : w✝ ∈ C
h : Proj (fun x ↦ ord I x < o) w✝ = x
⊢ ∀ (i : I), x i = true → ord I i < o

Tactic:
j

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x w✝ : I → Bool
left✝ : w✝ ∈ C
h : Proj (fun x ↦ ord I x < o) w✝ = x
j : I
⊢ x j = true → ord I j < o
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h.inr.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i✝ : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i✝
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j
hp : x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
x✝ : ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell i i_1
k : ℕ
hkl : k < l
i : cell C k
hi : i ∈ p l ⋯ j k
hxi : x ∈ openCell k i
⊢ i ∈ J k ∨ ∃ a < n + 1, ∃ a_1 ∈ J a, i ∈ if h : a ≤ n then p a h a_1 k else ∅

Tactic:
exact .inr ⟨l, hln, j, hj, by simp [Nat.le_of_lt_succ hln, hi]⟩

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x ↦ ord I x < o₁) l
hl' : eval (π C fun x ↦ ord I x < o₂) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o₂) '' {m | m < l})
⊢ eval (π C fun x ↦ ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o₁) '' {m | m < l})

Tactic:
eval_πs_image' C h (prop_of_isGood C _ hl),

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x ↦ ord I x < o₁) l
hl' :
  eval (π C fun x ↦ ord I x < o₂) l ∈ Submodule.span ℤ (⇑(πs' C h) '' eval (π C fun x ↦ ord I x < o₁) '' {m | m < l})
⊢ eval (π C fun x ↦ ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o₁) '' {m | m < l})
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h
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
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
⊢ ∀ (j : cell C n), Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
j

Goal state after:
case h
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
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
j : cell C n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell 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
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ∅ ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
exact empty_subset _

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmemcell : x ∈ openCell n j
xmemD : x ∈ interior D
⊢ False

Tactic:
suffices x ∈ (skeletonLT C 0 : Set X) ∩ openCell n j by
    rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmemcell : x ∈ openCell n j
xmemD : x ∈ interior D
⊢ x ∈ ↑(skeletonLT C 0) ∩ openCell n j
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ ContinuousAt (fun p ↦ p.2.insertIdx n p.1) (a, l)

Tactic:
rw [ContinuousAt, nhds_prod_eq]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ Tendsto (fun p ↦ p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a, l).2.insertIdx n (a, l).1))
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ ContinuousAt (fun p ↦ insertIdx p.1 i p.2) (a, l)

Tactic:
rw [ContinuousAt, nhds_prod_eq]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : hausdorffEDist s t < δ
⊢ (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ}

Tactic:
rw [hausdorffEDist, max_lt_iff] at h
  rw [hausdorffEntourage, Set.mem_ofPred]
  conv => enter [2, 2, 1, 1, _]; rw [edist_comm]
  have {s t : Set α} (h : ⨆ x ∈ s, infEDist x t < δ) :
      s ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} t := by
    intro x hx
    simpa only [infEDist, iInf_lt_iff, exists_prop] using! (le_iSup₂ x hx).trans_lt h
  exact ⟨this h.1, this h.2⟩

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

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

Tactic:
conv_rhs => rw [← one_pow n]

Goal state after:
case refine_1
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ a ^ n ≤ 1 ^ n
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 {x | edist x.2 x.1 ≤ δ} (s✝, t✝).1
s t : Set α
h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t
x : α
hx : x ∈ s
⊢ infEDist x t ≤ δ

Tactic:
obtain ⟨y, hy, hxy⟩ := h hx

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 {x | edist x.2 x.1 ≤ δ} (s✝, t✝).1
s t : Set α
h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : (x, y) ∈ {p | edist p.1 p.2 ≤ δ}
⊢ infEDist x t ≤ δ
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
⊢ ⟦transAt i f g⟧ = ⟦transAt j f g⟧

Tactic:
← fromLoop_trans_toLoop

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
⊢ ⟦fromLoop i (Path.trans (toLoop i f) (toLoop i g))⟧ = ⟦fromLoop j (Path.trans (toLoop j f) (toLoop j g))⟧
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
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 ↦ x1 * x2) ⟦p⟧ ⟦q⟧ = ⟦transAt (Classical.arbitrary N) q p⟧

Tactic:
← fromLoop_trans_toLoop

Goal state after:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 ↦ x1 * x2) ⟦p⟧ ⟦q⟧ =
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
h_sep : IsSeparated (↑ε) C
h : packingNumber ε A ≠ ⊤
⊢ C.encard ≤ (maximalSeparatedSet ε A).encard

Tactic:
rw [encard_maximalSeparatedSet h]
  exact le_iSup_of_le C <| le_iSup_of_le h_subset <| le_iSup_of_le h_sep (by simp)

Goal state after:
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:
refine ⟨fun h => ?_,
    fun hf => let ⟨C, hC⟩ := hf; iInf_lt_top.2 ⟨C, iInf_lt_top.2 ⟨hC, coe_lt_top⟩⟩⟩
  simp_rw [eHolderNorm, iInf_lt_top] at h
  let ⟨C, hC, _⟩ := h
  exact ⟨C, hC⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Finset α
⊢ (↑s).einfsep = s.offDiag.inf (uncurry edist)

Tactic:
by
  simp_rw [einfsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

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

Goal state before:
pp: case neg
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
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Tactic:
← ENNReal.div_le_iff h₁ h₂

Goal state after:
case neg
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
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (insert x s).einfsep = min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep

Tactic:
refine le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) ?_

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep ≤ (insert x s).einfsep
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ dist (ofSnowflaking x) (ofSnowflaking y) = dist x y ^ α⁻¹

Tactic:
by
  cases x; cases y
  simp [Real.rpow_rpow_inv dist_nonneg hα₀.ne']

Goal state after:
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 _
    rw [isClosed_iff_isLower]
    exact LowerSet.lower (lowerClosure s)

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ ⋂₀ (compl '' S) ⊆ Ici (sSup {a | (Ici a)ᶜ ∈ S})

Tactic:
intro b hb
      rw [mem_Ici, sSup_le_iff]
      intro c hc
      simp only [sInter_image, mem_iInter] at hb
      rw [← not_lt, ← mem_Iio, ← compl_Ici]
      exact hb _ hc

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst✝⁴, inst✝²] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsOpen[inst✝⁴] (f ⁻¹' u)
⊢ False

Tactic:
rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)] at hu

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst✝⁴, inst✝²] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
⊢ False
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
⊢ IsClosed[instTopologicalSpaceSubtype] S ↔ ∃ a, S = hull T a

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff hT, compl_inj_iff]

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
K : Compacts α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
⊢ ⋯.functor.Initial

Tactic:
rw [Monotone.initial_functor_iff]

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
K : Compacts α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
⊢ ∀ (j₁ : ↑K.openNhds), ∃ j₂, K.openRcNhdsToOpenNhds j₂ ≤ j₁
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
⊢ ⋯.functor.Initial

Tactic:
rw [Monotone.initial_functor_iff]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
⊢ ∀ (j₁ : ↑K.compactNhds), ∃ j₂, K.openRcNhdsToCompactNhds j₂ ≤ j₁