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

Goal state before:
pp: case succ
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
⊢ (Tape.move Dir.right)^[i] (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.left)^[i] L✝))) = L✝

Tactic:
Tape.move_left_right,

Goal state after:
case succ
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
⊢ (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ b :: t ∈ (b :: t) :: U

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R + S)) = map (g ∘ f) (R + S)

Tactic:
simp only [map, map_map]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R * S)) = map (g ∘ f) (R * S)

Tactic:
simp only [map, map_map]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R : RegularExpression α
⊢ map g (map f R.star) = map (g ∘ f) R.star

Tactic:
simp only [map, map_map]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)

pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)

Tactic:
case succ.bit1 n IH =>
      rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]

Goal state after:
case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)
Module: Mathlib.Computability.TuringDegree

Goal state before:
pp: f : ℕ →. ℕ
⊢ f ∈ {f}

Tactic:
by simp

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

Goal state before:
pp: p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k₁' k₂' : K'
q' : Λ'
⊢ move p k₁ k₂ q = move p' k₁' k₂' q' ↔ p = p' ∧ k₁ = k₁' ∧ k₂ = k₂' ∧ q = q'

Tactic:
by simp

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

Goal state before:
pp: p : Γ' → Bool
k : K'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k' : K'
q' : Λ'
⊢ clear p k q = clear p' k' q' ↔ p = p' ∧ k = k' ∧ q = q'

Tactic:
by simp

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

Goal state before:
pp: q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ q.copy = q'.copy ↔ q = q'

Tactic:
by simp

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

Goal state before:
pp: k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
k' : K'
s' : Option Γ' → Option Γ'
q' : Λ'
⊢ push k s q = push k' s' q' ↔ k = k' ∧ s = s' ∧ q = q'

Tactic:
by simp

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

Goal state before:
pp: q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ q.succ = q'.succ ↔ q = q'

Tactic:
by simp

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

Goal state before:
pp: q₁ q₂ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂ = b)
q₁' q₂' : Λ'
⊢ q₁.pred q₂ = q₁'.pred q₂' ↔ q₁ = q₁' ∧ q₂ = q₂'

Tactic:
by simp

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

Goal state before:
pp: k k' : Cont'
⊢ ret k = ret k' ↔ k = k'

Tactic:
by simp

Goal state after:
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
VisClopen' : IsClopen (Subtype.val '' V)
⊢ Subtype.val '' V ⊆ s

Tactic:
by simp

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 : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∀ (i : PEmpty.{u_5 + 1}), IsClopen ((fun x ↦ univ) i)

Tactic:
by simp

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 : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ (fun x ↦ univ) i

Tactic:
by simp

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 : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∀ (i : PEmpty.{u_5 + 1}), (fun x ↦ univ) i ⊆ D i

Tactic:
by simp

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 : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ⋃ i, D i ⊆ ⋃ i, (fun x ↦ univ) i

Tactic:
by simp

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))
⊢ some '' univ ⊆ univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
p : α → Bool
a : α
L l₁ : List α
o : Option α
l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) o
⊢ splitAtPred p (a :: L) = (l₁, o, l₂)

Tactic:
by
    rw [splitAtPred]
    have IH := splitAtPred_eq p L
    rcases o with - | o
    · rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨⟨⟩, rfl⟩
      rw [h₁ a (List.Mem.head _), cond, IH L none [] _ ⟨rfl, rfl⟩]
      exact fun x h => h₁ x (List.Mem.tail _ h)
    · rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨h₂, ⟨⟩⟩
      · rw [h₂, cond]
      rw [h₁ a (List.Mem.head _), cond, IH l₁ (some o) l₂ _ ⟨h₂, _⟩] <;> try rfl
      exact fun x h => h₁ x (List.Mem.tail _ h)

Goal state after:
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
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
h : x ∈ ρ '' Gᶜ
⊢ Gᶜ ⊆ (G ∩ ρ ⁻¹' N)ᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toProfinite.obj X).toTop
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
← Profinite.epi_iff_surjective

Goal state after:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toProfinite.obj X).toTop
⊢ Epi f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) stack =
    trNat a ++ Γ'.cons :: (trList L₂ ++ Γ'.consₗ :: L₃)

Tactic:
by simp

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

Goal state before:
pp: q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃) stack =
    trList L₂ ++ Γ'.consₗ :: L₃

Tactic:
by simp

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 simp

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 simp

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:
have : CompactSpace S := Quotient.compactSpace

Goal state after:
α : 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
this : CompactSpace (Quotient S.toSetoid)
⊢ Finite (Quotient S.toSetoid)
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
s : Clopens X
⊢ ∀ ⦃a₂ : Clopens X⦄, f s = f a₂ → s = a₂

Tactic:
t

Goal state after:
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
s t : Clopens X
⊢ f s = f t → s = t
Module: Mathlib.Topology.Category.CompHausLike.SigmaComparison

Goal state before:
pp: P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
⊢ IsIso (sigmaComparison X σ)

Tactic:
rw [sigmaComparison_eq_comp_isos]

Goal state after:
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
⊢ IsIso
    ((X.mapIso
          (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
            (productIsProduct fun x ↦ Opposite.op (of P (σ x))))).hom ≫
      (PreservesProduct.iso X fun a ↦ Opposite.op (of P (σ a))).hom ≫
        (Types.productIso fun a ↦ X.obj (Opposite.op (of P (σ a)))).hom)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.move p✝ k₁✝ k₂✝ q✝ ∈ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q✝)

Tactic:
apply Finset.mem_singleton_self

Goal state after:
case move
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.move p✝ k₁✝ k₂✝ q✝ ∈ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.clear p✝ k✝ q✝ ∈ trStmts₁ (Λ'.clear p✝ k✝ q✝)

Tactic:
apply Finset.mem_singleton_self

Goal state after:
case clear
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.clear p✝ k✝ q✝ ∈ trStmts₁ (Λ'.clear p✝ k✝ q✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ q✝.copy ∈ trStmts₁ q✝.copy

Tactic:
apply Finset.mem_singleton_self

Goal state after:
case copy
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ q✝.copy ∈ trStmts₁ q✝.copy
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.push k✝ s✝ q✝ ∈ trStmts₁ (Λ'.push k✝ s✝ q✝)

Tactic:
apply Finset.mem_singleton_self

Goal state after:
case push
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.push k✝ s✝ q✝ ∈ trStmts₁ (Λ'.push k✝ s✝ q✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read
f✝ : Option Γ' → Λ'
f_ih✝ : ∀ (a : Option Γ'), f✝ a ∈ trStmts₁ (f✝ a)
⊢ Λ'.read f✝ ∈ trStmts₁ (Λ'.read f✝)

Tactic:
apply Finset.mem_singleton_self

Goal state after:
case read
f✝ : Option Γ' → Λ'
f_ih✝ : ∀ (a : Option Γ'), f✝ a ∈ trStmts₁ (f✝ a)
⊢ Λ'.read f✝ ∈ trStmts₁ (Λ'.read f✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ q✝.succ ∈ trStmts₁ q✝.succ

Tactic:
apply Finset.mem_singleton_self

Goal state after:
case succ
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ q✝.succ ∈ trStmts₁ q✝.succ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred
q₁✝ q₂✝ : Λ'
q₁_ih✝ : q₁✝ ∈ trStmts₁ q₁✝
q₂_ih✝ : q₂✝ ∈ trStmts₁ q₂✝
⊢ q₁✝.pred q₂✝ ∈ trStmts₁ (q₁✝.pred q₂✝)

Tactic:
apply Finset.mem_singleton_self

Goal state after:
case pred
q₁✝ q₂✝ : Λ'
q₁_ih✝ : q₁✝ ∈ trStmts₁ q₁✝
q₂_ih✝ : q₂✝ ∈ trStmts₁ q₂✝
⊢ q₁✝.pred q₂✝ ∈ trStmts₁ (q₁✝.pred q₂✝)
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
⊢ f ⁻¹' {f y} ∈ Set.range fun x ↦ f ⁻¹' {↑x}

Tactic:
by simp

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

Goal state before:
pp: case ret
k✝ : Cont'
⊢ Λ'.ret k✝ ∈ trStmts₁ (Λ'.ret k✝)

Tactic:
apply Finset.mem_singleton_self

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
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
by
  inhabit α
  obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f
  classical
  let ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
  let σ : (α → Fin 2) → α := fun f => if h : ∃ a : α, ι a = f then h.choose else default
  refine ⟨j, gg.map σ, ?_⟩
  ext x
  simp only [LocallyConstant.coe_comap, LocallyConstant.map_apply,
    Function.comp_apply]
  dsimp [σ]
  have h1 : ι (f x) = gg (C.π.app j x) := by
    change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
    rw [h]
    rfl
  have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩
  rw [dif_pos]
  swap
  · assumption
  apply_fun ι
  · rw [h2.choose_spec]
    exact h1
  · intro a b hh
    have hhh := congr_fun hh a
    dsimp [ι] at hhh
    rw [if_pos rfl] at hhh
    split_ifs at hhh with hh1
    · exact hh1.symm
    · exact False.elim (bot_ne_top hhh)

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).inv =
    (functorIsoDiscreteComponents R X✝).inv ≫
      (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)

Tactic:
Iso.eq_inv_comp,

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functorIsoDiscreteComponents R X✝).hom ≫ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).inv =
    (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).inv =
    (functorIsoDiscreteComponents R X✝).inv ≫
      (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f)

Tactic:
Iso.eq_inv_comp,

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functorIsoDiscreteComponents R X✝).hom ≫ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).inv =
    (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f)
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ IsIso sequentialAdjunction.counit

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
X Y : LightCondSet
f : X ⟶ Y
⊢ ∀ (X : Sequential), IsIso (sequentialAdjunction.counit.app X)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
X✝ Y✝ : Profiniteᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : CostructuredArrow toProfinite.op X✝
⊢ colimit.ι (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
          { pt := colimit (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F),
            ι :=
              {
                app := fun g ↦
                  colimit.ι (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
                    ((CostructuredArrow.map x✝¹).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.ι (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop X✝)) ≫
        F.map x✝¹

Tactic:
by simp

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X✝ Y✝ : LightProfiniteᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : CostructuredArrow toLightProfinite.op X✝
⊢ colimit.ι (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
          { pt := colimit (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F),
            ι :=
              {
                app := fun g ↦
                  colimit.ι (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
                    ((CostructuredArrow.map x✝¹).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
          (LightProfinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.ι (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
          (LightProfinite.Extend.cocone F (Opposite.unop X✝)) ≫
        F.map x✝¹

Tactic:
by simp

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ lanPresheaf F ≅ F

Tactic:
refine NatIso.ofComponents
    (fun ⟨S⟩ ↦ (lanPresheafIso (hF S))) fun _ ↦ ?_
  simp only [lanPresheaf, pointwiseLeftKanExtension_map,
    lanPresheafIso_hom, Opposite.op_unop]
  exact colimit.hom_ext fun _ ↦ (by simp)

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i ∈ univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Condensed.Solid

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
⊢ (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R)

Tactic:
by
  dsimp only [profiniteSolidCounit, profiniteSolid]
  infer_instance

Goal state after: