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

Goal state before:
pp: case pos
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k)).reverse).nth i

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : i = (S k).length
⊢ update (L.nth i) k (some (f v)) k = (ListBlank.mk (List.map some (update S k (f v :: S k) k)).reverse).nth i

case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : ¬i = (S k).length
⊢ L.nth i k = (ListBlank.mk (List.map some (update S k (f v :: S k) k)).reverse).nth i
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑0 = ↑zero <<< n

pp: case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos (a✝ <<< n)) = ↑(pos a✝) <<< n

Tactic:
· symm
    apply Nat.zero_shiftLeft

Goal state after:
case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos (a✝ <<< n)) = ↑(pos a✝) <<< n
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 → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
q : Stmt Γ Λ σ
hs : SupportsStmt S q
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
induction q with

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

Goal state before:
pp: case pos
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
⊢ (if i = tl.length then update (L.nth i) k none else L.nth i) k =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k)).reverse).nth i

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
⊢ update (L.nth i) k none k = (ListBlank.mk (List.map some (update S k (hd :: tl).tail k)).reverse).nth i

case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = tl.length
⊢ L.nth i k = (ListBlank.mk (List.map some (update S k (hd :: tl).tail k)).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
⊢ (f.cons fs).Ok

Tactic:
(intro k v; rw [stepNormal])

Goal state after:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
⊢ (f.comp g).Ok

Tactic:
(intro k v; rw [stepNormal])

Goal state after:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal g (Cont.comp f k) v) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case case
f g : Code
IHf : f.Ok
IHg : g.Ok
⊢ (f.case g).Ok

Tactic:
(intro k v; rw [stepNormal])

Goal state after:
case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) k v) = do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
f : Code
IHf : f.Ok
⊢ f.fix.Ok

Tactic:
(intro k v; rw [stepNormal])

Goal state after:
case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.fix f k) v) k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case zero'
⊢ Code.zero'.Ok

Tactic:
(intro k v; rw [stepNormal])

Goal state after:
case zero'
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k (0 :: v)) k v) = do
    let v ← Code.zero'.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case succ
⊢ Code.succ.Ok

Tactic:
(intro k v; rw [stepNormal])

Goal state after:
case succ
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k [v.headI.succ]) k v) = do
    let v ← Code.succ.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case tail
⊢ Code.tail.Ok

Tactic:
(intro k v; rw [stepNormal])

Goal state after:
case tail
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k v.tail) k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.false
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    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₂)) }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩

Goal state after:
case cons.cons.false
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    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₂)) }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
rw [e.symm.isInducing.closure_eq_preimage_closure_image, Homeomorph.isOpen_preimage]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure (⇑e.symm '' U))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    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₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
⊢ 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)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩

Goal state after:
case cons.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    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₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
⊢ 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)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
⊢ C.pt.str = ⨅ i, induced (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) (F.obj i).str

Tactic:
exact induced_of_isLimit C hC

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

Goal state before:
pp: case refine_1
S : LightDiagram
⊢ Countable ((n : ℕ) × LocallyConstant (↑((S.diagram ⋙ toProfinite).obj (op n)).toTop) (Fin 2))

Tactic:
apply @instCountableSigma _ _ _ ?_
    intro n
    refine @Finite.to_countable _ ?_
    refine @Finite.of_injective _ ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩ → (Fin 2)) ?_ _
      LocallyConstant.coe_injective
    refine @Pi.finite _ _ ?_ _
    simp only [Functor.comp_obj]
    exact show (Finite (S.diagram.obj _)) from inferInstance

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

Goal state before:
pp: q q' : Λ'
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q

Tactic:
induction q with

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

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

case copy
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy

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

case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)

case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ

case pred
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)

case ret
q' : Λ'
k✝ : Cont'
⊢ q' ∈ trStmts₁ (Λ'.ret k✝) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k✝)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: f g : Code
k : Cont'
⊢ codeSupp (f.comp g) k = trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k)

Tactic:
by
  simp only [codeSupp, codeSupp', trNormal, Finset.union_assoc, contSupp]
  rw [← Finset.union_assoc _ _ (contSupp k),
    Finset.union_eq_right.2 (codeSupp'_self _ _)]

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

Goal state before:
pp: S : Finset Λ'
q : Λ'
H₁ : Λ'.Supports S q
HS₁ : trStmts₁ q ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
⊢ Supports (trStmts₁ q) S

Tactic:
induction q with

Goal state after:
case move
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)
HS₁ : trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q)) S

case clear
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p✝ k✝ q)
HS₁ : trStmts₁ (Λ'.clear p✝ k✝ q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.clear p✝ k✝ q)) S

case copy
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : trStmts₁ q.copy ⊆ S
⊢ Supports (trStmts₁ q.copy) S

case push
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k✝ s✝ q)
HS₁ : trStmts₁ (Λ'.push k✝ s✝ q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.push k✝ s✝ q)) S

case read
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : trStmts₁ (Λ'.read q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.read q)) S

case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : trStmts₁ q.succ ⊆ S
⊢ Supports (trStmts₁ q.succ) S

case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : trStmts₁ (q₁.pred q₂) ⊆ S
⊢ Supports (trStmts₁ (q₁.pred q₂)) S

case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : trStmts₁ (Λ'.ret k✝) ⊆ S
⊢ Supports (trStmts₁ (Λ'.ret k✝)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
⊢ Supports (contSupp k) S

Tactic:
induction k with
  | halt => simp [contSupp_halt, Supports]
  | cons₁ f k IH =>
    have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁
    refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_
    refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩
    simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
    exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
  | cons₂ k IH =>
    have H' := H; rw [contSupp_cons₂] at H'
    exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
  | comp f k IH =>
    have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H'
    exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩
  | fix f k IH =>
    rw [contSupp] at H
    exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

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

Goal state before:
pp: case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
⊢ ∀ (xi : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i)))
    (xj : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj

Tactic:
(fi : LocallyConstant _ _)

Goal state after:
case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
⊢ ∀ (xj : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
          (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
⊢ ∀ (xi : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i)))
    (xj : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj

Tactic:
(fi : LocallyConstant _ _)

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
⊢ ∀ (xj : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
          (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
⊢ traverse (h ∘ g) = traverse h ∘ map g

Tactic:
ext
  rw [comp_apply, traverse_map]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } (toList xs)).down = (toList xs).length

Tactic:
generalize toList xs = ys

Goal state after:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } ys).down = ys.length
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f g) = f' ∧ g = g'

Tactic:
H,

Goal state after:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ g = g'
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a

Tactic:
simp only [dom_iff_mem, not_exists] at h₀

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (⇑f) x a
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (error a✝)) = error a✝

Tactic:
simp [Except.map]

Goal state after: