mathlib-initiative/mathlib-tactics huggingface dataset:
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
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
i : I
a✝¹ : some i ∈ univ
j : I
a✝ : some j ∈ univ
⊢ i ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Limits

Goal state before:
pp: ⊢ HasLimits CondensedSet

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none, stk := elim (trPosNum a ++ Γ'.cons :: trList v) [] c d }

Tactic:
by

Goal state after:
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
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
i : I
a✝¹ : some i ∈ univ
j : I
a✝ : some j ∈ univ
⊢ j ∈ univ

Tactic:
by

Goal state after:
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
Z D : I → Set X
Z_closed : ∀ (i : I), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : I), IsClopen (D i)
Z_subset_D : ∀ (i : I), Z i ⊆ D i
Z_disj : 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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ ∃ a l, trPosNum m = a :: l ∧ natEnd a = false

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
s : Option Γ'
v : List ℕ
c d : List Γ'
⊢ ∃ s',
    Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList v) [] c d }
      (Nat.rec { l := some q₁, var := s', stk := elim (trList v.tail) [] c d }
        (fun n x ↦ { l := some q₂, var := s', stk := elim (trList (n :: v.tail)) [] c d }) v.headI)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
toSetoid✝¹ : Setoid X
isOpen_setOfPred_rel✝¹ : ∀ (x : X), IsOpen[inst✝] (ofPred (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝] (ofPred (toSetoid✝ x))
x✝ :
  { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ }.toSetoid =
    { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }.toSetoid
⊢ { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
⊢ IsOpen[inst✝²] (ofPred ((fun x y ↦ x ∈ A ↔ y ∈ A) x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsOpen {S.proj x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ IsClopen (ofPred (S.toSetoid x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S a : DiscreteQuotient X
⊢ a ≤ { toSetoid := ⊤, isOpen_setOfPred_rel := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
⊢ ∀ (a b : Quotient ⊤.toSetoid), a = b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A B : DiscreteQuotient Y
h : A ≤ B
⊢ comap f A ≤ comap f B

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
⊢ ofLE ⋯ = id

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
a : Quotient A.toSetoid
⊢ ofLE ⋯ a = a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
⊢ ofLE h₂ (ofLE h₁ x) = ofLE ⋯ x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x : X
⊢ IsOpen[inst✝³] (ofPred ((connectedComponentSetoid X) x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
⊢ ⊥.proj x = ⊥.proj y ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ LEComap g B C → LEComap f A B → LEComap (g.comp f) A C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
⊢ map (ContinuousMap.id X) ⋯ = id

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
⊢ map (g.comp f) ⋯ = map g h1 ∘ map f h2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case tail.convert_9.nil
k : Cont
s : Option Γ'
o : Option Γ' := List.casesOn [] none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim' (elim (trList []) [] [] (trContStack k) main = trNat [].headI ∧ trList [].tail = [])
    (fun a ↦ natEnd a = true ∧ elim (trList []) [] [] (trContStack k) main = trNat [].headI ++ a :: trList [].tail) o

Tactic:
simp [o]

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case tail.convert_9.cons
k : Cont
s : Option Γ'
head✝ : ℕ
tail✝ : List ℕ
o : Option Γ' := List.casesOn (head✝ :: tail✝) none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim'
    (elim (trList (head✝ :: tail✝)) [] [] (trContStack k) main = trNat (head✝ :: tail✝).headI ∧
      trList (head✝ :: tail✝).tail = [])
    (fun a ↦
      natEnd a = true ∧
        elim (trList (head✝ :: tail✝)) [] [] (trContStack k) main =
          trNat (head✝ :: tail✝).headI ++ a :: trList (head✝ :: tail✝).tail)
    o

Tactic:
simp [o]

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f ⋯ a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
⊢ map f cond (ofLE h c) = map f ⋯ c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.cons₁ fs v k))), var := none,
      stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k)) }
    c
⊢ main ≠ rev

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : Quotient A.toSetoid
⊢ A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {ofLE h a}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ x✝¹.proj ⁻¹' {Qs x✝¹} ⊆ x✝.proj ⁻¹' {Qs x✝}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
⊢ Finite (Quotient S.toSetoid)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ y, x✝¹ = {x | d.toSetoid x y}
y : X
h : x✝¹ = {x | d.toSetoid x y}
⊢ d.proj ⁻¹' {d.proj y} = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ ((image fun t ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X = fun x ↦
    match x with
    | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg ((fun k v ↦ Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
simp only

Goal state after:
case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (finsetClopens X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.AB

Goal state before:
pp: A : Type u_1
J : Type u_2
inst✝⁸ : Category.{v_1, u_1} A
inst✝⁷ : Category.{v_2, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
⊢ HasExactColimitsOfShape J (Condensed A)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.AB

Goal state before:
pp: A : Type u_1
J : Type u_2
inst✝⁸ : Category.{v_1, u_1} A
inst✝⁷ : Category.{v_2, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasLimitsOfShape J A
inst✝¹ : HasExactLimitsOfShape J A
inst✝ : HasFiniteColimits A
⊢ HasExactLimitsOfShape J (Condensed A)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
i : J
h : i = j
⊢ Set ↑(F.obj i)

Tactic:
by

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

Goal state before:
pp: X : Profinite
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst✝¹, instTopologicalSpaceProd] fun y ↦ (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x | MapsTo (Prod.mk x) V ↑W}
hUV : U ×ˢ V ⊆ ↑W
⊢ a.1 ∈ { carrier := U, isClopen' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: c : Code
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal c k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal c (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case halt
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepRet Cont.halt v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont Cont.halt)), var := s, stk := elim (trList v) [] [] (trContStack Cont.halt) } b₂

Tactic:
| halt =>

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ main ≠ rev ∧ aux ≠ rev ∧ main ≠ aux

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
⊢ ∃ I, W = I.sup fun i ↦ i.1 ×ˢ i.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : CompactSpace Y
inst✝² : CompactSpace X
inst✝¹ : Finite (Clopens X)
inst✝ : Finite (Clopens Y)
⊢ Finite (Clopens (X × Y))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ stack ≠ rev ∧ main ≠ rev ∧ stack ≠ main

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s ↦ ⋯.choose
⊢ Injective f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
⊢ Countable (Clopens X) ↔ SecondCountableTopology X

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ aux ≠ rev ∧ stack ≠ rev ∧ aux ≠ stack

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)

Tactic:
by

Goal state after: