mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringDegree

Goal state before:
pp: f g h : ℕ →. ℕ
hg : f ≤ᵀ g
hh : g ≤ᵀ h
⊢ ∀ g_1 ∈ {g}, RecursiveIn {h} g_1

Tactic:
simpa using

Goal state after:
f g h : ℕ →. ℕ
hg : f ≤ᵀ g
hh : g ≤ᵀ h
⊢ RecursiveIn {h} g
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inl.h
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ i < (List.map some tl).reverse.length

Tactic:
simpa using

Goal state after:
case neg.inl.h
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ i < tl.length
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
x✝ : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b
e : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b := x✝
b : ↑B.toTop
t : α
x : ↑(X t).toTop
h : (ConcreteCategory.hom (π t)) x = b
⊢ (ConcreteCategory.hom (Sigma.ι X t ≫ Sigma.desc π)) x = b

Tactic:
simpa using

Goal state after:
α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
x✝ : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b
e : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b := x✝
b : ↑B.toTop
t : α
x : ↑(X t).toTop
h : (ConcreteCategory.hom (π t)) x = b
⊢ (ConcreteCategory.hom (π t)) x = b
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
⊢ ∃ b,
    TrCfg (TM2.stepAux (M l) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (M l)) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
generalize M l = N

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
N : TM2.Stmt Γ Λ σ
⊢ ∃ b, TrCfg (TM2.stepAux N v S) b ∧ Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal N) v (Tape.mk' ∅ (addBottom L))) b
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
f1 : IsOpenEmbedding fun x ↦ ↑↑x
⊢ IsOpen[inst✝³] (Subtype.val '' V)

Tactic:
have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
f1 : IsOpenEmbedding fun x ↦ ↑↑x
f2 : IsOpen[instTopologicalSpaceSubtype] v
⊢ IsOpen[inst✝³] (Subtype.val '' V)
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
i : β✝
⊢ Z i ⊆ (C ∘ ⇑e.symm) i

Tactic:
simpa using

Goal state after:
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
i : β✝
⊢ Z i ⊆ C (e.symm i)
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
i : β✝
⊢ (C ∘ ⇑e.symm) i ⊆ D i

Tactic:
simpa using

Goal state after:
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
i : β✝
⊢ C (e.symm i) ⊆ D i
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h5 : univ.PairwiseDisjoint C
h4 : ∀ (i : α✝), D (e i) ⊆ ⋃ i, C i
⊢ ⋃ i, D i ⊆ ⋃ i, (C ∘ ⇑e.symm) i

Tactic:
simpa using

Goal state after:
case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h5 : univ.PairwiseDisjoint C
h4 : ∀ (i : α✝), D (e i) ⊆ ⋃ i, C i
⊢ ∀ (i : β✝), D i ⊆ ⋃ y, C y
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
⊢ Z none ⊆ D none ∧ Disjoint (Z none) (⋃ i, Z (some i))

Tactic:
simpa using

Goal state after:
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
⊢ Z none ⊆ D none ∧ ∀ (i : I), Disjoint (Z none) (Z (some i))
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

Tactic:
simpa using

Goal state after:
case pos
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : G = ∅
⊢ ∅ ⊆ closure (ρ '' ∅ᶜ)ᶜ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ y ∈ G ∩ ρ ⁻¹' N

Tactic:
simpa using

Goal state after:
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ y ∈ G ∧ ρ y ∈ N
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective fun x ↦
    match x with
    | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes

Tactic:
intro ⟨_, _⟩

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝ x))
⊢ ∀ ⦃a₂ : DiscreteQuotient X⦄,
    (fun x ↦
            match x with
            | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
          { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ } =
        (fun x ↦
            match x with
            | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
          a₂ →
      { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ } = a₂
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
⊢ IsClopen (⋃ s ∈ G, W s)

Tactic:
apply isClopen_biUnion_finset
    intro s hs
    dsimp [W]
    rw [dif_pos hs]
    exact ⟨(hV s).1.1.preimage (F.map _).hom.hom.continuous,
      (hV s).1.2.preimage (F.map _).hom.hom.continuous⟩

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

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
let G : Finset J := Finset.univ.image j

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' : a (↑⟨(x, y), hxy⟩).1 = a (↑⟨(x, y), hxy⟩).2
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
h₂ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y
⊢ a x = a y

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' : a (↑⟨(x, y), hxy⟩).1 = a (↑⟨(x, y), hxy⟩).2
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
h₂ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y
⊢ a x = a y
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ Supports (Finset.univ.biUnion K) S ↔ ∀ (a : Option Γ'), Supports (K a) S

Tactic:
simpa using

Goal state after:
K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ (∀ (q : Λ') (x : Option Γ'), q ∈ K x → TM2.SupportsStmt S (tr q)) ↔
    ∀ (a : Option Γ'), ∀ q ∈ K a, TM2.SupportsStmt S (tr q)
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))))

Tactic:
simpa using

Goal state after:
S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.proj n))
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)))

Tactic:
simpa using

Goal state after:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.proj n))
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ (ConcreteCategory.hom
        (X.obj.map
          (isTerminalPUnit.from
              (fiber ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a)).op))
      (Fiber.image (⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)) a) =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x

Tactic:
← map_eq_image _ a ⟨PUnit.unit, by simp [mem_iff_eq_image, ← map_preimage_eq_image]⟩

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ (ConcreteCategory.hom
        (X.obj.map
          (isTerminalPUnit.from
              (fiber ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a)).op))
      (((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) ↑⟨PUnit.unit, ⋯⟩) =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x