mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y : cell C 0
⊢ (OneSkeletonGraph C).IsLink e x y ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}

Tactic:
rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
    singleton_union]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x y : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 y) ![], ↑(map 0 x) ![]}
⊢ (fun x ↦ ↑(map 0 x) ![]) x ∈ {↑(map 0 y) ![], ↑(map 0 x) ![]}

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x y : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 y) ![], ↑(map 0 x) ![]}
⊢ (fun x ↦ ↑(map 0 x) ![]) y ∈ {↑(map 0 y) ![], ↑(map 0 x) ![]}

Tactic:
by simp

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

Goal state before:
pp: X : Compactum
A : Set X.A
a : X.A
ha : a ∈ A
⊢ X.str (X.incl a) = a

Tactic:
by simp

Goal state after:
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✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
J : (Finset ι)ᵒᵖ
⊢ CompactSpace ↑(obj C fun x ↦ x ∈ unop J)

Tactic:
← isCompact_iff_compactSpace

Goal state after:
ι : 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
J : (Finset ι)ᵒᵖ
⊢ IsCompact (obj C fun x ↦ x ∈ unop J)
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 K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
⊢ CompactSpace ↑C

Tactic:
← isCompact_iff_compactSpace

Goal state after:
ι : 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
⊢ IsCompact C
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
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closure (ball 0 1))

Tactic:
closure_ball 0 (by exact one_ne_zero)

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closedBall 0 1)
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
s : (Finset I)ᵒᵖ
⊢ CompactSpace ↑(π C fun x ↦ x ∈ unop s)

Tactic:
← isCompact_iff_compactSpace

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 : (Finset I)ᵒᵖ
⊢ IsCompact (π C fun x ↦ x ∈ unop s)
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
⊢ IsClosed[t] (A ∩ (D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j))

Tactic:
simp_rw [inter_union_distrib_left, inter_iUnion,
    ← iUnion_subtype (fun m ↦ m < n + 1) (fun m ↦ ⋃ i ∈ I m, A ∩ closedCell m i)]

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
⊢ IsClosed[t] (A ∩ D ∪ ⋃ x, ⋃ i ∈ I ↑x, A ∩ closedCell (↑x) i)
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
⊢ CompactSpace ↑C

Tactic:
← isCompact_iff_compactSpace

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
⊢ IsCompact C
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
apply Monad.Algebra.Hom.ext

Goal state after:
X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝
⊢ a₁✝.f = a₂✝.f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
i : I
hi : i ∈ ↑l
⊢ (LocallyConstant.evalMonoidHom x) (e C i) = 1

Tactic:
exact if_pos (h i hi)

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

Tactic:
by simp

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

Tactic:
by simp

Goal state after:
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)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
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
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

Tactic:
specialize hp l (Nat.le_of_lt_succ hln) j hxj
      simp_rw [mem_union, mem_iUnion, exists_prop] at hp
      refine .imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp
      simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]
      exact .inr ⟨l, hln, j, hj, by simp [Nat.le_of_lt_succ hln, hi]⟩

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

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ ((fun f ↦ extensionHom f) ((fun f ↦ X.completionHom ≫ f.hom) f)).hom = f.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: 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)
m : ℕ
⊢ 0 < m + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: 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)
m : ℕ
U : Fin (m + 1) → Set X
hU1 : ∀ (i : Fin (m + 1)), IsClopen (U i)
hU2 : ∀ (i : Fin (m + 1)), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
⊢ ↑m ≤ ↑(m + 1)

Tactic:
by simp

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

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

Tactic:
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]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
this : (⨅ i, 𝓟 (A \ U i)).NeBot
hle : ⨅ i, 𝓟 (A \ U i) ≤ 𝓟 A
a : E
ha : a ∈ A
hac : ClusterPt a (⨅ i, 𝓟 (A \ U i))
k : ι
hk : a ∈ U k
⊢ False

Tactic:
exact closure_minimal (fun _ hx => hx.2) (hUo k).isClosed_compl
    (hac.mono (iInf_le _ k)).mem_closure hk

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this : IsCountablyCompact A
⊢ False

Tactic:
obtain ⟨a, ha⟩ : ∃ a ∈ A, MapClusterPt a atTop x := by
    refine isCountablyCompact_iff_seq_clusterPt.1 this _ (.of_forall fun n => ?_)
    exact mem_iUnion_of_mem n <| subset_closure <| mem_singleton (x n)

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
⊢ False
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case a
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
K : Set X
hK : K ∈ S
⊢ ∀ y ∈ {t | t.Finite ∧ t ⊆ T},
    {f | MapsTo (⇑f) K (⋃₀ y)} ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {U | IsOpen[inst✝] U}

Tactic:
t

Goal state after:
case a
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
K : Set X
hK : K ∈ S
t : Set (Set Y)
⊢ t ∈ {t | t.Finite ∧ t ⊆ T} →
    {f | MapsTo (⇑f) K (⋃₀ t)} ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {U | IsOpen[inst✝] U}
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
⊢ ∀ᶠ (x_1 : ℕ) in cofinite, x x_1 ∈ A → x x_1 ∈ range x ∩ A

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist (some val✝) none = edist none (some val✝)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none (some val✝) = edist (some val✝) none

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
⊢ edist none none = edist none none

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist none (some val✝) ≤ edist none (some val✝¹) + edist (some val✝¹) (some val✝)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist (some val✝¹) (some val✝) ≤ edist (some val✝¹) none + edist none (some val✝)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none (some val✝) ≤ edist none none + edist none (some val✝)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist (some val✝¹) none ≤ edist (some val✝¹) (some val✝) + edist (some val✝) none

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none none ≤ edist none (some val✝) + edist (some val✝) none

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist (some val✝) none ≤ edist (some val✝) none + edist none none

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
⊢ edist none none ≤ edist none none + edist none none

Tactic:
by simp

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) := 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 ↑U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ Subtype.val '' V ⊆ U

Tactic:
by simp

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) := 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 ↑U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ V = Subtype.val ⁻¹' Subtype.val '' V

Tactic:
by simp

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 : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ Subtype.val '' V ⊆ F

Tactic:
by simp

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 : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ V = Subtype.val ⁻¹' Subtype.val '' V

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ n

Tactic:
by simp

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

Goal state before:
pp: ⊢ 3⁻¹ ≠ 0

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ 1 / 3 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
⊢ IsClosed (preCantorSet n)

Tactic:
let g := (Homeomorph.addLeft (2 : ℝ)).trans f

Goal state after:
n : ℕ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
⊢ IsClosed (preCantorSet n)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
S : Set ι
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), CompactSpace (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
⊢ IsClosed (S.domRestrict '' s)

Tactic:
by
  classical
  have : S.domRestrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd (· ∈ S) α) := rfl
  rw [this, image_comp]
  exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs

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

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem :
  0 ≤ (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∧
    (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ≤ 1
⊢ 3 ^ n ≠ 0

Tactic:
by simp

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
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
⊢ s ∈ traverse 𝓝 u

Tactic:
have : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v := by
      refine List.Forall₂.flip ?_
      replace hv := hv.flip
      simp only [List.forall₂_and_left, Function.flip_def] at hv ⊢
      exact ⟨hv.1, hu.flip⟩

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
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this✝ : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
this : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) u v
⊢ s ∈ traverse 𝓝 u
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
⊢ Tendsto (fun p ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 []) (𝓝 ([].insertIdx (n + 1) a))

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝¹ : AddZeroClass R
inst✝ : Preorder R
x✝² x✝¹ x✝ : X
⊢ 0 x✝² x✝ ≤ 0 x✝² x✝¹ + 0 x✝¹ x✝

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x✝ : X
⊢ d x✝ x✝ ⊔ d' x✝ x✝ = 0

Tactic:
by simp

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
⊢ 0 + 0 = 0

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝¹ : AddZeroClass R
inst✝ : SemilatticeSup R
⊢ ∀ (x y z : X), ⊥ x z ≤ ⊥ x y ⊔ ⊥ y z

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (insertIdx a i ⟨l, hl⟩))

Tactic:
rw [insertIdx, tendsto_subtype_rng]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x ↦ ↑(insertIdx x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨(↑⟨l, hl⟩).insertIdx (↑i) a, ⋯⟩)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ uniformity (Set α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | hausdorffEDist p.1 p.2 < ε}

Tactic:
by
    refine le_antisymm
      (le_iInf₂ fun ε hε => Filter.le_principal_iff.mpr ?_)
      (uniformity_basis_edist.lift' monotone_hausdorffEntourage |>.ge_iff.mpr fun ε hε =>
        Filter.mem_iInf_of_mem ε <| Filter.mem_iInf_of_mem hε fun _ =>
        mem_hausdorffEntourage_of_hausdorffEDist_lt)
    obtain ⟨δ, hδ, hδε⟩ := exists_between hε
    filter_upwards [Filter.mem_lift' (uniformity_basis_edist_le.mem_of_mem hδ)]
      with _ h using hδε.trans_le' <| hausdorffEDist_le_of_mem_hausdorffEntourage h

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
⊢ 2 ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
⊢ packingNumber ε ∅ = 0

Tactic:
simp [packingNumber]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 1 = 2 * 0 + 1 + 2 * 0

Tactic:
by simp

Goal state after: