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

Goal state before:
pp: case cons.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
rw [List.reverseAux, ← IH (a :: l₁) l₂' e]

Goal state after:
case cons.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂' R'))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case nil
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
f : List.Vector Bool [].length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux [].length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux (f ⟨[], ⋯⟩) v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')

Tactic:
| nil =>

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂ R')) =
    stepAux (f ⟨a :: l₂, ⋯⟩) v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
IH

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (f (a ::ᵥ ⟨l₂, ⋯⟩)) v (Tape.mk' (ListBlank.append (l₂.reverseAux (a :: l₁)) L') R') =
    stepAux (f ⟨a :: l₂, ⋯⟩) v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
a : Γ → σ → σ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.load a q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.load a q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
exact ⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩

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

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (↑m).testBit n

Tactic:
IH

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ (↑m).testBit n = (↑m).testBit n
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case rfind.mpr
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
x : List ℕ
⊢ (∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x) →
    ∃
      a ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: ↑v),
      x = [a.headI.pred]

Tactic:
rintro ⟨n, ⟨hn, hm⟩, rfl⟩
      refine ⟨n.succ::v.1, ?_, rfl⟩
      have : (n.succ::v.1 : List ℕ) ∈
        PFun.fix (fun v =>
          (cf.eval v).bind fun y =>
            Part.some <|
              if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail)
                else Sum.inr (v.headI.succ :: v.tail))
            (n::v.val) :=
        PFun.mem_fix_iff.2 (Or.inl (by simp [hf, hn]))
      generalize (n.succ :: v.1 : List ℕ) = w at this ⊢
      clear hn
      induction n with
      | zero => exact this
      | succ n IH =>
        refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
        simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false,
          Part.mem_some_iff, List.tail_cons]

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
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ IsOpen[inst✝³] (range fun x ↦ ↑↑x)

Tactic:
· have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset
        rw [this]
        apply isOpen_interior

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

Goal state before:
pp: case refine_1
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
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
⊢ (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')) →
    TM2.SupportsStmt S (stRun s q✝) →
      (∀ x ∈ trStmts₁ (stRun s q✝), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
          ∀ l' ∈ trStmts₁ (stRun s q✝), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
IH

Goal state after:
case refine_1
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
k✝ : K
s : StAct K Γ σ k✝
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')
⊢ TM2.SupportsStmt S (stRun s q✝) →
    (∀ x ∈ trStmts₁ (stRun s q✝), x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
        ∀ l' ∈ trStmts₁ (stRun s q✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], 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₂ ([].reverseAux (S k₂)) }

Tactic:
| nil =>

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

Goal state before:
pp: case refine_2
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
a✝ : σ → σ
q✝ : TM2.Stmt Γ Λ σ
⊢ (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')) →
    TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝) →
      (∀ x ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
          ∀ l' ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
IH

Goal state after:
case refine_2
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
a✝ : σ → σ
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')
⊢ TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝) →
    (∀ x ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
        ∀ l' ∈ trStmts₁ (TM2.Stmt.load a✝ q✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Topology.Category.CompHaus.Projective

Goal state before:
pp: case h
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ (⇑(TopCat.Hom.hom g.hom) ∘ h) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure

Tactic:
rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]

Goal state after:
case h
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ ⇑(ConcreteCategory.hom f) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], 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:
| nil =>

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

Goal state before:
pp: case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a [] c d }
    { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) }

Tactic:
| nil =>

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

Goal state before:
pp: case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some q.copy, var := some x, stk := elim ((some x).getD default :: a) b c ((some x).getD default :: d) }
    { l := some q, var := none, stk := elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d)) }

Tactic:
exact IH _ _ _

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

Goal state before:
pp: 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

Tactic:
exact ⟨rfl, rfl⟩

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

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

Tactic:
let f : ∀ s ∈ G, j0 ⟶ j s := fun s hs => (hj0 (Finset.mem_image.mpr ⟨s, hs, rfl⟩)).some

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

Goal state before:
pp: case cons.succ.one
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 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail✝

Tactic:
exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case cons.succ.bit1
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 : ℕ
a✝ : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos a✝.bit1)).tail ++ Γ'.cons :: trList tail✝

Tactic:
exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case cons.succ.bit0
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 : ℕ
a✝ : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos a✝.bit0)).tail ++ Γ'.cons :: trList tail✝

Tactic:
exact ⟨rfl, rfl⟩

Goal state after:
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)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } =
    Sigma.ι (fun a ↦ of P (σ a)) a ≫
      ((finiteCoproduct.isColimit fun a ↦ of P (σ a)).coconePointUniqueUpToIso
              (coproductIsCoproduct fun a ↦ of P (σ a))).op.inv.unop

Tactic:
IsColimit.fac

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)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } = (finiteCoproduct.cofan fun a ↦ of P (σ a)).ι.app { as := a }
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

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

Tactic:
simpa only [proj_comp_transitionMap'] using S.proj_surjective n

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

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S : (CompHausLike P)ᵒᵖ
⊢ ∀ ⦃Y_1 : (CompHausLike P)ᵒᵖ⦄ (f : S ⟶ Y_1),
    ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map f ≫
        match Y_1 with
        | op S => counitAppApp S Y) =
      (match S with
        | op S => counitAppApp S Y) ≫
        Y.map f

Tactic:
T

Goal state after:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
⊢ ∀ (f : S ⟶ T),
    ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map f ≫
        match T with
        | op S => counitAppApp S Y) =
      (match S with
        | op S => counitAppApp S Y) ≫
        Y.map f
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
X : Type (max u w)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) (functorToPresheaves.obj X)

Tactic:
by
    rw [Presheaf.isSheaf_of_iso_iff (functorToPresheavesIso P hs X)]
    exact ((TopCat.discrete.obj X).toSheafCompHausLike P hs).property

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

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).map
      ((constantSheafAdj (coherentTopology CompHaus) (ModuleCat R) CompHaus.isTerminalPUnit).counit.app
        ((functor R).obj M)))

Tactic:
← constantSheafAdj_counit_w

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso
    ((constantCommuteCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).hom.app
        (((functor R).obj M).obj.obj (op (CompHaus.of PUnit.{u + 1}))) ≫
      (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit).counit.app
        ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M)))