mathlib-initiative/mathlib-tactics huggingface dataset:
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 π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
⊢ Sigma.desc π = i.hom ≫ finiteCoproduct.desc X π

Tactic:
apply colimit.hom_ext

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 π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X := ⋯
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := ⋯
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
⊢ ∀ (j : Discrete α),
    colimit.ι (Discrete.functor X) j ≫ Sigma.desc π =
      colimit.ι (Discrete.functor X) j ≫ i.hom ≫ finiteCoproduct.desc X π
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mpr.inr
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' : Sum.inr v'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v''
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
obtain ⟨v₁, he₁, he₂⟩ := (Part.mem_map_iff _).1 he₁'
      split_ifs at he₂ with h; cases he₂
      clear he₁'
      refine ⟨_, he₁, ?_⟩
      rw [reaches_eval]
      swap
      · exact ReflTransGen.single rfl
      rw [stepRet, if_neg h]
      exact IH v₁.tail ((Part.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩)

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)
i : I
⊢ Z' i ⊆ D (some i)

Tactic:
by grind

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)
i : I
⊢ Disjoint (⋃ i, Z' i) U

Tactic:
by grind

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
⊢ Z none ⊆ D none

Tactic:
by grind

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

Goal state before:
pp: case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ x ∈ trStmts₁ q₁✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧ ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ x ∈ trStmts₁ q₂✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧ ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝, x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
refine ⟨⟨IH₁₁, IH₂₁⟩, fun l h ↦ ?_⟩

Goal state after:
case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ x ∈ trStmts₁ q₁✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧ ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ x ∈ trStmts₁ q₂✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧ ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝, x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝)
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = Cfg.halt <$> k.eval x✝

Tactic:
← IH

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = eval step (stepRet k x✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ k₂
e : splitAtPred p (S k₁) = (L₁, o, L₂)
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }

Tactic:
induction L₁ generalizing S s with

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
⊢ Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
g_sur

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
⊢ ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

Tactic:
rw [sigma_mk_preimage_image' ij]

Goal state after:
case neg
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen ∅
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (L₁, o, L₂)
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
induction L₁ generalizing S s with

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'
x : X
hx0 : x ∉ C0
hxD : x ∉ D none
j : I
hi : x ∈ D (some j)
⊢ x ∈ D' j

Tactic:
by grind

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:
rcases A.proj_surjective a with ⟨a, rfl⟩

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case intro
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)
val✝ : Fintype (Clopens X)
⊢ Finite (Clopens (X × Y))

Tactic:
cases nonempty_fintype (Clopens Y)

Goal state after:
case intro.intro
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)
val✝¹ : Fintype (Clopens X)
val✝ : Fintype (Clopens Y)
⊢ Finite (Clopens (X × Y))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.zero
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
⊢ if (0 :: tail✝).headI = 0 then
    natEnd ((trList (0 :: tail✝)).head?.getD default) = true ∧ (trList (0 :: tail✝)).tail = trList (0 :: tail✝).tail
  else
    natEnd ((trList (0 :: tail✝)).head?.getD default) = false ∧
      (trList (0 :: tail✝)).tail = (trNat (0 :: tail✝).headI).tail ++ Γ'.cons :: trList (0 :: tail✝).tail

pp: case cons.succ
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if ((n + 1) :: tail✝).headI = 0 then
    natEnd ((trList ((n + 1) :: tail✝)).head?.getD default) = true ∧
      (trList ((n + 1) :: tail✝)).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trList ((n + 1) :: tail✝)).head?.getD default) = false ∧
      (trList ((n + 1) :: tail✝)).tail =
        (trNat ((n + 1) :: tail✝).headI).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail

Tactic:
· simp

Goal state after:
case cons.succ
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if ((n + 1) :: tail✝).headI = 0 then
    natEnd ((trList ((n + 1) :: tail✝)).head?.getD default) = true ∧
      (trList ((n + 1) :: tail✝)).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trList ((n + 1) :: tail✝)).head?.getD default) = false ∧
      (trList ((n + 1) :: tail✝)).tail =
        (trNat ((n + 1) :: tail✝).headI).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ LightProfinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop

Tactic:
change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
  exact Subtype.totallyDisconnectedSpace

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

Goal state before:
pp: case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective]
    apply (forget LightProfinite).epi_of_epi_map

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

Goal state before:
pp: c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) (init c v) ↔ x ∈ halt <$> c.eval v

Tactic:
rw [reaches_eval h₂.to_reflTransGen]

Goal state after:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) i ↔ x ∈ halt <$> c.eval v
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ Fiber.image (f ∘ fun x ↦ ↑x) b = f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b)

Tactic:
← Fiber.map_preimage_eq_image

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ (f ∘ fun x ↦ ↑x) (Fiber.preimage (f ∘ fun x ↦ ↑x) b) = f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b)
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
⊢ LocallyConstant.functor.essImage X

Tactic:
let i : (e.functor.obj X).obj ≅ (e.functor.obj (LocallyConstant.functor.obj _)).obj :=
    Condensed.isoLocallyConstantOfIsColimit _ h

Goal state after:
X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
i : (e.functor.obj X).obj ≅
  (e.functor.obj
      (LocallyConstant.functor.obj
        ((e.functor.obj X).obj.obj (toProfinite.op.obj (Opposite.op (of PUnit.{u + 1})))))).obj :=
  Condensed.isoLocallyConstantOfIsColimit (e.functor.obj X).obj h
⊢ LocallyConstant.functor.essImage X
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : LightCondMod R
⊢ [LightCondensed.IsDiscrete M, IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
  tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
  tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _
    LightProfinite.isTerminalPUnit (adjunction R) _
  tfae_have 1 ↔ 5 :=
    have : (functor R).Faithful := inferInstance
    have : (functor R).Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ LightProfinite.isTerminalPUnit (adjunction R) _
  tfae_have 6 → 1 := by
    intro h
    rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)]
    intro S
    let : PreservesFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
      preservesFilteredColimitsOfSize_shrink.{0, u, 0, u} _
    exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
  tfae_have 1 → 6 := by
    intro h S
    rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)] at h
    let : ReflectsFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
      reflectsFilteredColimitsOfSize_shrink.{0, u, 0, u} _
    exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩
  tfae_finish

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

Goal state before:
pp: F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
        (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
        (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) =
    colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)

Tactic:
apply colimit.hom_ext

Goal state after:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
        (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
        (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) =
    colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv)

Tactic:
apply colimit.hom_ext

Goal state after:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
            (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv)