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

Goal state before:
pp: case prim
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
hf : Nat.Primrec' f✝
⊢ ∃ c, ∀ (v : List.Vector ℕ n✝), c.eval ↑v = pure <$> ↑f✝ v

Tactic:
induction hf with
    | zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩
    | succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩
    | get i =>
      refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
      · exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩
      · obtain ⟨c, h⟩ := IH
        exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩
    | comp g hf hg IHf IHg =>
      simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg
    | @prec n f g _ _ IHf IHg =>
      obtain ⟨cf, hf⟩ := IHf
      obtain ⟨cg, hg⟩ := IHg
      simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
      refine ⟨prec cf cg, fun v => ?_⟩
      rw [← v.cons_head_tail]
      specialize hf v.tail
      replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
      simp only [Vector.cons_val, Vector.tail_val] at hf hg
      simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val, Vector.tail_val]
      simp only [← Part.pure_eq_some] at hf hg ⊢
      induction v.head with
      | zero => simp [prec, hf, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp [prec, Part.bind_assoc, Bind.bind]
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl

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

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔
    x ∈ do
      let v ← f.fix.eval v
      eval step (Cfg.ret k v)

Tactic:
simp only [Part.bind_eq_bind, Part.mem_bind_iff]

Goal state after:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
⊢ (Option.map (fun a ↦ update default k (some a) k') L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i

Tactic:
· simp only [Function.update_of_ne h]
      rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, List.map, List.reverse_nil]
      cases L.reverse[i]? <;> rfl

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

Goal state before:
pp: case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))

Tactic:
show update S rev [] = S by rw [← h₂, Function.update_eq_self]

Goal state after:
case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update S k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case hnc
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ (ConcreteCategory.hom f).toFun x ∉ U

Tactic:
simp [U, C]

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

Goal state before:
pp: case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ (val✝ :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ (val✝ :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ (val✝ :: L₂) k₂)

Tactic:
show update S rev [] = S by rw [← h₂, Function.update_eq_self]

Goal state after:
case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update S k₁ (val✝ :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ (val✝ :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ (val✝ :: L₂) k₂)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case refine_2
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ x ∈ closure U

Tactic:
← hφ₁ x

Goal state after:
case refine_2
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ (φ x).1 ∈ closure U
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝ : Projective X
A : Type u
⊢ ∀ {Z : Type u} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace Z] [CompactSpace A] [T2Space A] [CompactSpace Z]
    [T2Space Z] {f : ↑X.toTop → Z} {g : A → Z},
    Continuous f → Continuous g → Function.Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
B

Goal state after:
X : CompHaus
inst✝ : Projective X
A B : Type u
⊢ ∀ [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : ↑X.toTop → B} {g : A → B}, Continuous f → Continuous g → Function.Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := g, continuous_toFun := hg }
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f

Tactic:
have : Epi g' := by
    rw [CompHaus.epi_iff_surjective]
    assumption

Goal state after:
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case hnc
X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ f.hom.hom' x ∉ U

Tactic:
simpa only [U, Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not]
      using! exists_apply_eq_apply f x

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

Goal state before:
pp: X : CompHaus
⊢ Projective X ↔ ExtremallyDisconnected ↑X.toTop

Tactic:
by
  constructor
  · intro h
    change ExtremallyDisconnected X.toStonean
    infer_instance
  · intro h
    let X' : Stonean := ⟨X.toTop, inferInstance⟩
    change Projective X'.compHaus
    apply Stonean.instProjectiveCompHausCompHaus

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
⊢ i ∈ univ

Tactic:
trivial

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:
trivial

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)
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
let V : Set Y := {y | (a.1, y) ∈ W}

Goal state after:
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}
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
obtain - | n := v

Goal state after:
case nil
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 Γ'
⊢ if [].headI = 0 then natEnd ((trList []).head?.getD default) = true ∧ (trList []).tail = trList [].tail
  else
    natEnd ((trList []).head?.getD default) = false ∧
      (trList []).tail = (trNat [].headI).tail ++ Γ'.cons :: trList [].tail

case cons
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 Γ'
n : ℕ
tail✝ : List ℕ
⊢ if (n :: tail✝).headI = 0 then
    natEnd ((trList (n :: tail✝)).head?.getD default) = true ∧ (trList (n :: tail✝)).tail = trList (n :: tail✝).tail
  else
    natEnd ((trList (n :: tail✝)).head?.getD default) = false ∧
      (trList (n :: tail✝)).tail = (trNat (n :: tail✝).headI).tail ++ Γ'.cons :: trList (n :: tail✝).tail
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
A : LightProfinite
⊢ ∀ {B : LightProfinite} (f : A ⟶ B) [IsIso ((forget LightProfinite).map f)], IsIso f

Tactic:
B

Goal state after:
X Y : LightProfinite
f : X ⟶ Y
A B : LightProfinite
⊢ ∀ (f : A ⟶ B) [IsIso ((forget LightProfinite).map f)], IsIso f
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case hnc
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ (ConcreteCategory.hom f).toFun x ∉ U

Tactic:
simp [U, C]

Goal state after:
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
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z : C
⊢ ∀ (B : C) (π : Z ⟶ B) [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))

Tactic:
B

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
⊢ ∀ (π : Z ⟶ B) [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
x : ↑(G.obj (unop (op B)))
⊢ a x = b x

Tactic:
obtain ⟨y, hy⟩ := (hq Z B π).surjective x

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
x : ↑(G.obj (unop (op B)))
y : ↑(G.obj Z)
hy : (ConcreteCategory.hom (G.map π)) y = x
⊢ a x = b x
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case halt
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
H₁ : contSupp Cont'.halt ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret Cont'.halt))

Tactic:
trivial

Goal state after:
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✝
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
Z : CompHausLike P
⊢ ∀ (B : CompHausLike P) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap ⇑(ConcreteCategory.hom ((CompHausLike.compHausLikeToTop P).map π))

Tactic:
B

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X✝ : Type w'
inst✝² : TopologicalSpace X✝
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
Z B : CompHausLike P
⊢ ∀ (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom ((CompHausLike.compHausLikeToTop P).map π))
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case inj
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) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ Function.Injective ι

Tactic:
intro a b hh

Goal state after:
case inj
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) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
a b : α
hh : ι a = ι b
⊢ a = b