mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ V_ o → y.rank < o

Tactic:
mem_vonNeumann'

Goal state after:
case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ ∀ ⦃y : ZFSet.{u_1}⦄, (∃ a < o, y ⊆ V_ a) → y.rank < o
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ V_ o

Tactic:
mem_vonNeumann'

Goal state after:
case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ ∃ a < o, y ⊆ V_ a
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (sum fun i ↦ (V_ ↑i).card) ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)

Tactic:
refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le

Goal state after:
case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ ℵ₀ ≤ #↑(Set.Iio o)

case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u, u + 1} #↑(Set.Iio o) ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
⊢ WellFormedBasis (left ++ f :: right)

Tactic:
apply compare_left_aux (h.of_sublist (by simp)) at hf_comp_left

Goal state after:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
hf_comp_left : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ WellFormedBasis (left ++ f :: right)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates

Goal state before:
pp: n : ℕ
⊢ AllZero (List.replicate n 0)

Tactic:
induction n <;> grind [AllZero, sign]

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

Goal state before:
pp: basis : Basis
⊢ toLogFun [] basis = 0

Tactic:
ext x
  simp [toLogFun]

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

Goal state before:
pp: m : UnitMonomial
⊢ m.toLogFun [] = 0

Tactic:
ext x
  simp [toLogFun]

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

Goal state before:
pp: exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ toLogFun (exp :: tl) (basis_hd :: basis_tl) = exp • log ∘ basis_hd + tl.toLogFun basis_tl

Tactic:
ext x
  simp [toLogFun]

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

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
hd : ℝ × MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ motive (Seq.cons hd tl, f)

Tactic:
apply cons

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

Goal state before:
pp: case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h_firstIsPos : 0 < exps_hd ∨ exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
obtain h | h := h_firstIsPos

Goal state after:
case cons.cons.inl
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : 0 < exps_hd
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case h_coef.step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ (exp, coef).2.Sorted ∧ motive tl

Tactic:
grind [h_step exp coef tl h]

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

Goal state before:
pp: case step.right
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ motive tl

Tactic:
grind [h_step exp coef tl h]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Sorted
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
simpa using h

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

Goal state before:
pp: a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬IsSquare a

Tactic:
by
  rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    ← Int.isSquare_natCast_iff (n := Rat.den _), Rat.den_div_eq_of_coprime]
  · simp [hd]
  · contrapose! hnd
    simp_all
  · simpa

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

Goal state before:
pp: case none
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = none
⊢ none.getD x ∈ ys ↔ x ∈ xs

Tactic:
dsimp [Option.getD]

Goal state after:
case none
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = none
⊢ x ∈ ys ↔ x ∈ xs
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
⊢ Dense ↑(Submonoid.closure s) ↔ Dense ↑(Subgroup.closure s)

Tactic:
by
  simp only [dense_iff_closure_eq, closure_submonoidClosure_eq_closure_subgroupClosure]

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 : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
m : ℕ
j : cell C m
h : ¬m < n
⊢ False

Tactic:
exact (hn m (not_lt.1 h)).false j

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: case refine_1
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a b : (fun X ↦ ↑X.toTop) (indexCone hC).pt
h :
  (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a =
    (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) b
⊢ a = b

Tactic:
refine eq_of_forall_π_app_eq a b (fun J ↦ ?_)

Goal state after:
case refine_1
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a b : (fun X ↦ ↑X.toTop) (indexCone hC).pt
h :
  (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a =
    (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) b
J : Finset ι
⊢ (π_app C fun x ↦ x ∈ J) a = (π_app C fun x ↦ x ∈ J) b
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
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ (1 - e (π C fun x ↦ x ∈ s) b) x = 1

Tactic:
rw [LocallyConstant.sub_apply, e, LocallyConstant.coe_mk, LocallyConstant.coe_mk, if_neg hh]

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ LocallyConstant.toFun 1 x - 0 = 1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π (π C K) J
⊢ x ∈ π C J

pp: case refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π C J
⊢ x ∈ π (π C K) J

Tactic:
· obtain ⟨y, ⟨z, hz, rfl⟩, rfl⟩ := h
    refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩
    rw [proj_comp_of_subset J K h]

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π C J
⊢ x ∈ π (π C K) J
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
y : I → Bool
hy : y ∈ C
⊢ (precomp Subtype.val) y = fun i ↦ ↑⟨Proj J y, ⋯⟩ ↑i

Tactic:
ext ⟨i, hi⟩

Goal state after:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
y : I → Bool
hy : y ∈ C
i : I
hi : J i
⊢ (precomp Subtype.val) y ⟨i, hi⟩ = ↑⟨Proj J y, ⋯⟩ ↑⟨i, hi⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (iso_map C J) ⟨fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false, ⋯⟩ = a

Tactic:
ext i
      exact dif_pos i.prop

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
⊢ ∀ {X Y : (Finset I)ᵒᵖ} (f : X ⟶ Y),
    (spanFunctor hC).map f ≫
        (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop Y)) ⋯).hom =
      (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop X)) ⋯).hom ≫
        (indexFunctor hC).map f

Tactic:
rintro ⟨s⟩ ⟨t⟩ ⟨⟨⟨f⟩⟩⟩

Goal state after:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ⊆ unop (op s)
⊢ (spanFunctor hC).map (op { down := { down := f } }) ≫
      (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop (op t))) ⋯).hom =
    (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop (op s))) ⋯).hom ≫
      (indexFunctor hC).map (op { down := { down := f } })
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (eval C l) x = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Tactic:
change LocallyConstant.evalMonoidHom x (l.eval C) = _

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (LocallyConstant.evalMonoidHom x) (eval C l) = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_I
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I✝¹ : (n : ℕ) → Set (cell C n)
closed'✝¹ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
F : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] F
hF : D ∪ ⋃ n, ⋃ j, openCell n ↑j = F
h :
  (fun E ↦ E.carrier) { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    (fun E ↦ E.carrier) { carrier := F, I := I✝, closed' := closed'✝, union' := hF }
⊢ E = F

Tactic:
simpa using h

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

Goal state before:
pp: case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true})

Tactic:
refine IsClopen.isOpen ?_

Goal state after:
case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsClopen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true})
Module: Mathlib.Topology.Category.UniformSpace

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

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

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)
⊢ ∃ a ∈ f '' A, ClusterPt a l

Tactic:
have : NeBot (l.comap f ⊓ 𝓟 A) :=
    comap_inf_principal_neBot_of_image_mem hl_nebot (le_principal_iff.mp hle)

Goal state after:
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
⊢ ∃ a ∈ f '' A, ClusterPt a l
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ (K_1 : Set X), (∃ i y, Subtype.val '' (K i) y = K_1) → IsCompact K_1

Tactic:
rintro K ⟨U, n, rfl⟩

Goal state after:
case h.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
U : ↑(countableBasis X)
n : ℕ
⊢ IsCompact (Subtype.val '' (K U) n)
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ ∀ t₁ ∈ range (Iic ∘ 𝓟), ∀ t₂ ∈ range (Iic ∘ 𝓟), ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range (Iic ∘ 𝓟), x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl
      exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: ⊢ Continuous toENNReal

Tactic:
by
  refine OrderTopology.continuous_iff.mpr fun a ↦ ⟨?_, ?_⟩
  · simpa using isOpen_Ioi
  · simpa using isOpen_Iio

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

Goal state before:
pp: case inr
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
· use j; rwa [funSplitAt_symm_apply, dif_neg j.prop, Subtype.coe_eta]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s := by
      induction hu generalizing s with
      | nil =>
        exists []
        simp only [List.forall₂_nil_left_iff]
        exact ⟨trivial, hus⟩
      | cons ht _ ih =>
        rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
        rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
        exact
          ⟨u::v, List.Forall₂.cons hu hv,
            Subset.trans (Set.seq_mono (Set.image_mono hut) hvss) hus⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝² : AddCommMonoid R
inst✝¹ : LinearOrder R
inst✝ : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : d x y < 0
⊢ d x y + d y x < 0 + 0

Tactic:
refine add_lt_add H (d.symm x y ▸ H)

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
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ (genLoopEquivOfUnique (Fin 1)) (transAt default q p) ≈
    ((genLoopEquivOfUnique (Fin 1)) q).trans ((genLoopEquivOfUnique (Fin 1)) p)

Tactic:
genLoopEquivOfUnique_transAt

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ Path.trans ((genLoopEquivOfUnique (Fin 1)) q) ((genLoopEquivOfUnique (Fin 1)) p) ≈
    ((genLoopEquivOfUnique (Fin 1)) q).trans ((genLoopEquivOfUnique (Fin 1)) p)
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
⊢ ∃ f, Continuous f ∧ Function.Surjective f

Tactic:
let : TopologicalSpace.SeparableSpace X :=
    TopologicalSpace.SecondCountableTopology.to_separableSpace

Goal state after:
X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
⊢ ∃ f, Continuous f ∧ Function.Surjective f
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case mpr.inl
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : IsEmpty X
⊢ eHolderNorm r f = 0

pp: case mpr.inr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ eHolderNorm r f = 0

Tactic:
· exact eHolderNorm_of_isEmpty

Goal state after:
case mpr.inr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ eHolderNorm r f = 0
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h✝ : DiscreteTopology X
x✝¹ x✝ : ℕ
h : x✝¹ ≠ x✝
⊢ (Disjoint on fun n ↦ {(Infinite.natEmbedding X) n}) x✝¹ x✝

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
⊢ ∃ U, (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
suffices ∃ U : ℕ → Set X, (∀ n, (U n).Nonempty) ∧ (∀ n, IsOpen (U n)) ∧
      Pairwise (Disjoint on U) by
    rcases this with ⟨U, hne, ho, hd⟩
    refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩
    · refine fun n ↦ infinite_iUnion fun i j hij ↦ ?_
      suffices n.pair i = n.pair j by simpa
      apply hd.eq
      simpa [hij, onFun] using (hne _).ne_empty
    · refine fun n n' hne ↦ disjoint_iUnion_left.2 fun m ↦ disjoint_iUnion_right.2 fun m' ↦ hd ?_
      simp [hne]
  by_cases h : DiscreteTopology X
  · refine ⟨fun n ↦ {Infinite.natEmbedding X n}, fun _ ↦ singleton_nonempty _,
      fun _ ↦ isOpen_discrete _, fun _ _ h ↦ ?_⟩
    simpa using h
  · simp only [discreteTopology_iff_nhds_ne, not_forall, ← ne_eq, ← neBot_iff] at h
    rcases h with ⟨x, hx⟩
    suffices ∃ U : ℕ → Set X, (∀ n, (U n).Nonempty ∧ IsOpen (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧
        Pairwise (Disjoint on U) by
      rcases this with ⟨U, hU, hd⟩
      exact ⟨U, fun n ↦ (hU n).1, fun n ↦ (hU n).2.1, hd⟩
    have : Std.Symm (α := Set X) Disjoint := ⟨fun _ _ h ↦ h.symm⟩
    refine exists_seq_of_forall_finset_exists' (fun U : Set X ↦ U.Nonempty ∧ IsOpen U ∧ Uᶜ ∈ 𝓝 x)
      Disjoint fun S hS ↦ ?_
    have : (⋂ U ∈ S, interior (Uᶜ)) \ {x} ∈ 𝓝[≠] x := inter_mem_inf ((biInter_finset_mem _).2
      fun U hU ↦ interior_mem_nhds.2 (hS _ hU).2.2) (mem_principal_self _)
    rcases hx.nonempty_of_mem this with ⟨y, hyU, hyx : y ≠ x⟩
    rcases t2_separation hyx with ⟨V, W, hVo, hWo, hyV, hxW, hVW⟩
    refine ⟨V ∩ ⋂ U ∈ S, interior (Uᶜ), ⟨⟨y, hyV, hyU⟩, ?_, ?_⟩, fun U hU ↦ ?_⟩
    · exact hVo.inter (isOpen_biInter_finset fun _ _ ↦ isOpen_interior)
    · refine mem_of_superset (hWo.mem_nhds hxW) fun z hzW ⟨hzV, _⟩ ↦ ?_
      exact disjoint_left.1 hVW hzV hzW
    · exact disjoint_left.2 fun z hzU ⟨_, hzU'⟩ ↦ interior_subset (mem_iInter₂.1 hzU' U hU) hzU

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ OrderDual.instTopologicalSpace = upperSet αᵒᵈ

Tactic:
by ext; rw [IsLowerSet.topology_eq α]

Goal state after: