mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
⊢ ↑F ≤ 𝓝 x → X.str F = x

Tactic:
let T1 := insert AA T0

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
⊢ ↑F ≤ 𝓝 x → X.str F = x
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]
    simp only [LocallyConstant.toFun_eq_coe, LocallyConstant.coe_one, Pi.one_apply, sub_zero]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
⊢ ⋃ n, ⋃ j, openCell n j = C

Tactic:
simpa using RelCWComplex.union_iUnion_openCell_eq_complex (C := C)

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
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (n + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j
m : ℕ
mlt : m < n + 1
⊢ IsClosed[t] (⋃ i ∈ I ↑⟨m, mlt⟩, A ∩ closedCell (↑⟨m, mlt⟩) i)

Tactic:
← iUnion_subtype (fun i ↦ i ∈ I m) (fun i ↦ A ∩ closedCell m i.1)

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (n + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j
m : ℕ
mlt : m < n + 1
⊢ IsClosed[t] (⋃ x, A ∩ closedCell m ↑x)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
x✝ : X✝.A
⊢ (ConcreteCategory.hom a₁✝.f).toFun x✝ = (ConcreteCategory.hom a₂✝.f).toFun x✝

Tactic:
simpa using! ConcreteCategory.congr_hom h _

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

Goal state before:
pp: ⊢ CreatesLimits (forget Profinite)

Tactic:
by
  change CreatesLimits (profiniteToCompHaus ⋙ forget _)
  infer_instance

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

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent (ι := ↑(GoodProducts (π C fun x ↦ ord I x < o))) ℤ (eval (π C fun x ↦ ord I x < o))

Tactic:
exact h (le_of_lt ho') (π C (ord I · < o)) (isClosed_proj C o hC) (contained_proj C o)

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

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : X.carrier
⊢ (ConcreteCategory.hom ((fun f ↦ X.completionHom ≫ f.hom) ((fun f ↦ extensionHom f) f))) x = (ConcreteCategory.hom f) x

Tactic:
rcases f with ⟨⟨_, _⟩⟩

Goal state after:
X : UniformSpaceCat
Y : CpltSepUniformSpace
x : X.carrier
val✝ : X.carrier → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y).carrier
property✝ : UniformContinuous val✝
⊢ (ConcreteCategory.hom ((fun f ↦ X.completionHom ≫ f.hom) ((fun f ↦ extensionHom f) { hom' := ⟨val✝, property✝⟩ })))
      x =
    (ConcreteCategory.hom { hom' := ⟨val✝, property✝⟩ }) x
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Infinite (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]
      intro m
      obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)
      exact le_trans (by simp) (h U hU1 hU2 hU3 hU4)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⋯
K₂ : Set ↑(Icc b c) := ⋯
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
⊢ MapsTo (⇑IccInclusionRight) K₂ K

Tactic:
rintro x ⟨y, ⟨⟨z, hz⟩, ⟨h1, (h2 : b ≤ z)⟩, rfl⟩, rfl⟩

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
z : α
hz : z ∈ Icc a c
h1 : ⟨z, hz⟩ ∈ K
h2 : b ≤ z
⊢ IccInclusionRight (projIccCM ↑⟨z, hz⟩) ∈ K
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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun l ↦ Products.eval (C' C ho) (↑l).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail

Tactic:
rw [hh]

Goal state after:
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
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun l ↦ Products.eval (C' C ho) (↑l).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (eval (C' C ho) ∘ f)
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ {x | ∀ i ∈ l, i ∈ x} = {x | x ≤ l}

Tactic:
← Filter.le_def

Goal state after:
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) := ⋯
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := ⋯
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
⊢ Continuous[instTopologicalSpaceSubtype, _] ⇑WithGeneratedByTopology.equiv.symm

Tactic:
continuous_def

Goal state after:
ι : 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)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case refine_2
α✝ : 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∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
⊢ Subtype.val ⁻¹' some '' s' = Subtype.val ⁻¹' Metric.eball (some x) r

Tactic:
ext ⟨y, yh⟩

Goal state after:
case refine_2
α✝ : 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∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
y : Option α
yh : y ∈ Metric.eball (some x) ∞
⊢ ⟨y, yh⟩ ∈ Subtype.val ⁻¹' some '' s' ↔ ⟨y, yh⟩ ∈ Subtype.val ⁻¹' Metric.eball (some x) r
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)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ IsOpen[inst✝²] V

Tactic:
IsGeneratedBy.isOpen_iff X

Goal state after:
ι : 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)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝³ i] (⇑f ⁻¹' V)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x y : Option α
xy : edist x y = 0
⊢ x = y

Tactic:
cases x <;> cases y

Goal state after:
case none.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
xy : edist none none = 0
⊢ none = none

case none.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist none (some val✝) = 0
⊢ none = some val✝

case some.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist (some val✝) none = 0
⊢ some val✝ = none

case some.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝¹ val✝ : α
xy : edist (some val✝¹) (some val✝) = 0
⊢ some val✝¹ = some val✝
Module: Mathlib.Topology.Homotopy.HSpaces

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

Tactic:
rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]

Goal state after:
θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 2 * ↑t

Tactic:
rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]

Goal state after:
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := ⋯
l : ℕ := ⋯
⊢ P 0

Tactic:
simpa [P, finset_logSizeBallSeq_zero] using ⟨hs, ht⟩

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

Goal state before:
pp: case succ
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 1 / 4 ∈ preCantorSet (n + 1) ∧ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
apply And.intro
    · -- goal: 1 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 3 / 4 ∈ preCantorSet n
      exact Or.inl ⟨3 / 4, ih.2, by norm_num⟩
    · -- goal: 3 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 1 / 4 ∈ preCantorSet n
      exact Or.inr ⟨1 / 4, ih.1, by norm_num⟩

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this✝ : IsClosed ({i}.domRestrict '' s)
this : ⇑(Homeomorph.piUnique fun t ↦ α ↑t) ∘ {i}.domRestrict = fun x ↦ x i
⊢ IsClosed ((fun x ↦ x i) '' s)

Tactic:
rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ cons <$> 𝓝 a <*> 𝓝 l = (fun p ↦ p.1 :: p.2) <$> (Prod.mk <$> 𝓝 a <*> 𝓝 l)

Tactic:
simp [-Filter.map_def, Function.comp_def, functor_norm]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Prod.mk <$> 𝓝 a <*> (cons <$> 𝓝 a' <*> 𝓝 l) =
    (fun p ↦ (p.1, p.2.1 :: p.2.2)) <$> (Prod.mk <$> 𝓝 a <*> (Prod.mk <$> 𝓝 a' <*> 𝓝 l))

Tactic:
simp [-Filter.map_def, Function.comp_def, functor_norm]

Goal state after:
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:
by refine add_lt_add H (d.symm x y ▸ H)

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

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → ↑KC := Subtype.coind f ⋯
hf'_surjective : Function.Surjective f'
h : ↑KC → ↑KH := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
⊢ ∃ f, Continuous f ∧ Function.Surjective f

Tactic:
have hh_surjective : Function.Surjective h :=
    Set.restrictPreimage_surjective _ cantorToHilbert_surjective

Goal state after:
X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → ↑KC := Subtype.coind f ⋯
hf'_surjective : Function.Surjective f'
h : ↑KC → ↑KH := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
hh_surjective : Function.Surjective h
⊢ ∃ f, Continuous f ∧ Function.Surjective f
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
hX : IsEmpty X
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r f), ↑i < b

Tactic:
exact fun ε hε => ⟨0, .of_isEmpty, hε⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ⨅ d, uncurry edist ↑d

Tactic:
by
  refine eq_of_forall_le_iff fun _ => ?_
  simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : s.offDiag = ∅
⊢ (↑s).infsep = 0

Tactic:
rw [← Finset.not_nonempty_iff_eq_empty] at hs
  rw [Finset.coe_infsep, dif_neg hs]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : IsUltrametricDist X
x y : X
h : x ≠ y
r : ℝ
hr : 0 < r
hr' : r < dist x y
⊢ x ∈ ball x r

Tactic:
simp only [mem_ball, dist_self, hr]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ (fun f ↦ ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a b : α
⊢ a ⤳ b ↔ a ≤ b

Tactic:
simp only [specializes_iff_closure_subset, closure_singleton, Ici_subset_Ici]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ image2 (fun x1 x2 ↦ x1 ×ˢ x2) (IsLower.lowerBasis α) (IsLower.lowerBasis β) ⊆ {s | IsOpen[lower (α × β)] s}

Tactic:
image2_subset_iff

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ ∀ x ∈ IsLower.lowerBasis α, ∀ y ∈ IsLower.lowerBasis β, x ×ˢ y ∈ {s | IsOpen[lower (α × β)] s}
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
⊢ IsOpen[lower (α × β)] ((↑(upperClosure s))ᶜ ×ˢ (↑(upperClosure t))ᶜ)

Tactic:
simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
⊢ IsOpen[lower (α × β)] ((⋂ i ∈ s, (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ i ∈ t, (Prod.snd ⁻¹' Ici i)ᶜ)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝¹ : TopologicalSpace (α × β) := lower (α × β)
b : β
x✝ : b ∈ t
⊢ IsOpen[lower (α × β)] (Prod.snd ⁻¹' Ici b)ᶜ

Tactic:
· exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case e'_5.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
he : IsEmpty ↑X
⊢ s.arrows (𝟙 ⊤)

Tactic:
exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim

Goal state after: