mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
simp only [opowAux2, opow_def, e₁, h, r₁, r₂, OfNat.ofNat, Zero.zero, One.one,
          repr]

Goal state after:
case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : m = 0
⊢ ω ^ type emptyRelation * ↑↑⟨1, ⋯⟩ + type emptyRelation = (type emptyRelation + ↑(0 + 1)) ^ (ω * b'.repr + ↑k)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case cons
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
n : Fin (basis_hd :: basis_tl).length
⊢ (monomialRpow (basis_hd :: basis_tl) (↑n) r).toFun = (basis_hd :: basis_tl)[n] ^ r

Tactic:
cases n using Fin.cases

Goal state after:
case cons.zero
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
⊢ (monomialRpow (basis_hd :: basis_tl) (↑0) r).toFun = (basis_hd :: basis_tl)[0] ^ r

case cons.succ
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
i✝ : Fin basis_tl.length
⊢ (monomialRpow (basis_hd :: basis_tl) (↑i✝.succ) r).toFun = (basis_hd :: basis_tl)[i✝.succ] ^ r
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
x : ℝ
hx : 0 < basis_hd x
⊢ (basis_hd ^ (exp2 - exp1) * (toFun m2 basis_tl * (toFun m1 basis_tl)⁻¹)) x =
    (fun x ↦ basis_hd x ^ exp2 * toFun m2 basis_tl x / (basis_hd x ^ exp1 * toFun m1 basis_tl x)) x

Tactic:
simp only [Pi.mul_apply, Pi.pow_apply, Pi.inv_apply, Real.rpow_sub hx]

Goal state after:
case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
x : ℝ
hx : 0 < basis_hd x
⊢ basis_hd x ^ exp2 / basis_hd x ^ exp1 * (toFun m2 basis_tl x * (toFun m1 basis_tl x)⁻¹) =
    basis_hd x ^ exp2 * toFun m2 basis_tl x / (basis_hd x ^ exp1 * toFun m1 basis_tl x)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_coef : coef = 0
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop (𝓝 0)

Tactic:
intro t
  rw [zero_coef_toFun _ (by simpa [t])]
  exact tendsto_const_nhds

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

Goal state before:
pp: case succ.inl
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step✝ :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
base : motive s t
step : s = t
⊢ dist s t ≤ 2⁻¹ ^ (n + 1)

Tactic:
simp [step]

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
⊢ Nat.pair 0 (Nat.unpair n).2 = n

Tactic:
← h,

Goal state after:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
⊢ Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 = n
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case a
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).2 < n

Tactic:
exact nat_unpair_lt_2 h

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
h : o.fundamentalSequence = Sum.inl none
⊢ o.fastGrowing = Nat.succ

Tactic:
fastGrowing_def h

Goal state after:
o : ONote
h : o.fundamentalSequence = Sum.inl none
⊢ (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl none, ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun i ↦ (f i).fastGrowing i) =
    Nat.succ
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
⊢ o.fastGrowing = fun i ↦ a.fastGrowing^[i] i

Tactic:
fastGrowing_def h

Goal state after:
o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
⊢ (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl (some a), ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun i ↦ (f i).fastGrowing i) =
    fun i ↦ a.fastGrowing^[i] i
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
⊢ o.fastGrowing = fun i ↦ (f i).fastGrowing i

Tactic:
fastGrowing_def h

Goal state after:
o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
⊢ (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inr f, ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun i ↦ (f i).fastGrowing i) =
    fun i ↦ (f i).fastGrowing i
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
⊢ n ^ p ≠ m ^ q

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
h : ∀ (m : ℕ), 0 ≠ m ^ q
⊢ 0 ^ p ≠ m ^ q

case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
hn : n ≠ 0
⊢ n ^ p ≠ m ^ q
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ b * y = x * a

Tactic:
← h,

Goal state after:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a * x = x * a
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : Even 1
⊢ False

Tactic:
exact Nat.not_even_one h

Goal state after:
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: case mpr
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := ⋯
S2 : Set (X →ₜ* Y) := ⋯
S3 : Set C(X, Y) := ⋯
S4 : Set (X → Y) := ⋯
h : Equicontinuous fun x ↦ ⇑↑x
x✝ : X → Y
⊢ x✝ ∈ DFunLike.coe '' S1 → x✝ ∈ S4

Tactic:
rintro ⟨f, hf, rfl⟩

Goal state after:
case mpr
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
f : X →* Y
hf : f ∈ S1
⊢ ⇑f ∈ S4
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 ι
inst✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous[inst✝¹, inst✝².toTopologicalSpace] (eval x ∘ F)
cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ closure[inst✝¹] s ⊆ {i | F i x ∈ Q}
⊢ CompactSpace ↑(closure[inst✝¹] s)

Tactic:
exact ArzelaAscoli.compactSpace_of_isClosedEmbedding 𝔖_compact
    (F_clemb.comp isClosed_closure.isClosedEmbedding_subtypeVal) cls_eqcont
    fun K hK x hx ↦ (cls_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, by simpa using! hQ.2⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ Submonoid.closure (s ∪ s⁻¹) ≤ (Submonoid.closure s).topologicalClosure

Tactic:
Submonoid.closure_le

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ s ∪ s⁻¹ ⊆ ↑(Submonoid.closure s).topologicalClosure
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : Valued.v x < 1
y : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn : Valued.v x ^ n < ↑((Units.map ↑MonoidWithZeroHom.ValueGroup₀.embedding) y)
m : ℕ
hm : n ≤ m
⊢ Valued.v x ^ m ≤ Valued.v x ^ n

Tactic:
exact pow_le_pow_right_of_le_one' hx.le hm

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

Goal state before:
pp: X : Compactum
x : X.A
⊢ X.str (X.incl x) = x

Tactic:
change ((β).η.app _ ≫ X.a) _ = _

Goal state after:
X : Compactum
x : X.A
⊢ (ConcreteCategory.hom (β.η.app X.A ≫ X.a)) x = x
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: 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
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
⊢ X.str ⁻¹' Q ∩ X.str ⁻¹' R ∈ C0

Tactic:
use Q ∩ R

Goal state after:
case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
C0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
C1 : ssu := ⋯
C2 : Set (Set (Ultrafilter X.A)) := ⋯
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
⊢ Q ∩ R ∈ F ∧ X.str ⁻¹' (Q ∩ R) = X.str ⁻¹' Q ∩ X.str ⁻¹' R
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: 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
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty

Tactic:
refine ⟨P, hq2, ?_⟩

Goal state after:
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
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
⊢ Function.Surjective ⇑(π_app C J)

Tactic:
by
  intro x
  obtain ⟨y, hy⟩ := x.prop
  exact ⟨⟨y, hy.1⟩, Subtype.ext hy.2⟩

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

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
exact hI

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

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
exact hI

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

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ x ∈ C

Tactic:
← h,

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ Proj J y ∈ C
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
⊢ Submodule.span ℤ (eval {fun x ↦ false} '' {nil}) = ⊤

Tactic:
Set.image_singleton,

Goal state after:
I : Type u_1
inst✝ : LinearOrder I
⊢ ℤ ∙ eval {fun x ↦ false} nil = ⊤
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
⊢ (extensionHom (X.completionHom ≫ f)).hom = f

Tactic:
ext x
  exact congr_fun (Completion.extension_comp_coe f.hom.property) x

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
by_cases hs : (tsupport f).Nonempty
  · obtain ⟨x, _, hmax⟩ := mem_compactlySupported.mp h |>.exists_isMaxOn hs <|
      (map_continuous f).norm.continuousOn
    refine ⟨x, le_antisymm (norm_coe_le_norm f x) (norm_le (norm_nonneg _) |>.mpr fun y ↦ ?_)⟩
    by_cases hy : y ∈ tsupport f
    · exact hmax hy
    · simp [image_eq_zero_of_notMem_tsupport hy]
  · suffices f = 0 by simp [this]
    rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs

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

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : tsupport g = ∅
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
exact ⟨0, by simp [tsupport_eq_empty_iff.mp hs]⟩

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst✝¹, inst✝] f
l : Filter F
hl_nebot : l.NeBot
hl_count : l.IsCountablyGenerated
hle : l ≤ 𝓟 (f '' A)
this✝ : (comap f l ⊓ 𝓟 A).NeBot
x : E
hxA : x ∈ A
hx : ClusterPt x (comap f l ⊓ 𝓟 A)
this : (𝓝 x ⊓ comap f l).NeBot
⊢ ∃ a ∈ f '' A, ClusterPt a l

Tactic:
exact ⟨f x, mem_image_of_mem f hxA, (hf.continuousAt.inf tendsto_comap).neBot⟩

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

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

Tactic:
refine ⟨L '' s, image_subset_iff.2 fun x hx ↦ hLS x <| hsK x hx, s.finite_toSet.image _,
        by rwa [sUnion_image], ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ MapsTo (⇑f) (⋃₀ (L '' ↑s)) (⋃₀ t)
Module: Mathlib.Topology.Convenient.HomSpace

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
T : Type v''
inst✝² : TopologicalSpace T
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X (Y × Z) T
⊢ ContinuousGeneratedBy X fun z ↦ g.comp { toFun := fun y ↦ (y, z), prop := ⋯ }

Tactic:
simpa only [continuousGeneratedBy_iff_uncurry,
          continuousGeneratedBy_dom_prod_iff] using! g.prop

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

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
T : Type v''
inst✝² : TopologicalSpace T
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)
⊢ ContinuousGeneratedBy X fun x ↦ (g x.2) x.1

Tactic:
simpa only [continuousGeneratedBy_iff_uncurry,
          continuousGeneratedBy_dom_prod_iff] using! g.prop

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⋂ s ∈ l, Iic (𝓟 s) = Iic l

Tactic:
Iic,

Goal state after:
α : Type u_2
l : Filter α
⊢ ⋂ s ∈ l, {x | x ≤ 𝓟 s} = {x | x ≤ l}
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
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
h : (logSizeBallSeq J hJ a c (i + 1)).finset = ∅
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius

Tactic:
simp [pairSetSeq, logSizeBallStruct.ball, h, hJ]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (fun x1 x2 ↦ x1 :: x2) <$> 𝓝 a <*> traverse 𝓝 l = List.cons <$> 𝓝 a <*> 𝓝 l

Tactic:
← nhds_list

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (fun x1 x2 ↦ x1 :: x2) <$> 𝓝 a <*> 𝓝 l = List.cons <$> 𝓝 a <*> 𝓝 l
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (∃ b ∈ s, (f i) x z ≤ (f b) x y) ∨ ∃ b ∈ s, (f i) x z ≤ (f b) y z

Tactic:
refine h.imp ?_ ?_ <;>
  intro H

Goal state after:
case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) x y
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) x y

case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) y z
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) y z
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ ↑ε
a : X
ha : a ∈ A
⊢ {a} ⊆ A

Tactic:
by simp [ha]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
a : X
ha : a ∈ A
⊢ {a} ⊆ A

Tactic:
by simp [ha]

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

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

Tactic:
simp_rw [packingNumber] at h ⊢

Goal state after:
case inr
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 }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
⊢ c ≤ (univ.pi s).einfsep

Tactic:
refine le_einfsep fun x hx y hy hxy => ?_
  rw [mem_univ_pi] at hx hy
  rcases Function.ne_iff.mp hxy with ⟨i, hi⟩
  exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.infsep = 0 ↔ s.Subsingleton

Tactic:
by
  rw [infsep_zero, einfsep_eq_top_iff, or_iff_right_iff_imp]
  exact fun H => (einfsep_pos_of_finite.ne' H).elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
⊢ Topology.IsUpperSet α

Tactic:
let := upperSet α

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
this : TopologicalSpace α := upperSet α
⊢ Topology.IsUpperSet α
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
neUc : Uᶜ.Nonempty
⊢ (Iic (sSup Uᶜ))ᶜ = U

Tactic:
rw [compl_eq_comm, le_antisymm_iff]

Goal state after:
case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
neUc : Uᶜ.Nonempty
⊢ Uᶜ ⊆ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ⊆ Uᶜ