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

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k' a).Dom

Tactic:
rw [bind_dom]

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ∃ (h : (k (encode a)).Dom), (↑(decode ((k (encode a)).get h))).Dom
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case nil
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ BlankExtends [] (head (Quotient.mk'' []) :: [].tail)

pp: case cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: (head✝ :: tail✝).tail)

Tactic:
· exact ⟨1, rfl⟩

Goal state after:
case cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: (head✝ :: tail✝).tail)
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
⊢ eval f a = eval f b

Tactic:
refine Part.ext fun _ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
⊢ x✝ ∈ eval f b

case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
⊢ x✝ ∈ eval f a
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inl.none
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
eg : f₁ e₁ = none
⊢ f₂ b✝ = none → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

pp: case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b✝ x → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
· intro c0
        cases cd.symm.trans c0

Goal state after:
case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b✝ x → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)

Tactic:
simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]

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

Goal state before:
pp: case nil
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
⊢ append [] (mk l₂) = mk ([] ++ l₂)

Tactic:
simp only [*, ListBlank.append, List.nil_append, List.cons_append, ListBlank.cons_mk]

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

Goal state before:
pp: case cons
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
head✝ : Γ
tail✝ : List Γ
tail_ih✝ : append tail✝ (mk l₂) = mk (tail✝ ++ l₂)
⊢ append (head✝ :: tail✝) (mk l₂) = mk (head✝ :: tail✝ ++ l₂)

Tactic:
simp only [*, ListBlank.append, List.nil_append, List.cons_append, ListBlank.cons_mk]

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ RecursiveIn O g

Tactic:
iff_nat

Goal state after:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun x ↦ s} f
g : ℕ →. ℕ
hg : g ∈ {fun x ↦ s}
⊢ Partrec g

Tactic:
by rw [Set.mem_singleton_iff.mp hg]; exact .const' s

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
⊢ q₀ ∈ stmts₁ q₂

Tactic:
induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind

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

Goal state before:
pp: case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
have := TM1.stmts_supportsStmt ss h₂

Goal state after:
case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
this : TM1.SupportsStmt S q
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (P.deriv a * Q + Q.deriv a).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
· rw [add_rmatch_iff, ih]
      constructor
      · rintro (⟨t, u, _⟩ | h)
        · exact ⟨a :: t, u, by tauto⟩
        · exact ⟨[], a :: x, rfl, hepsilon, h⟩
      · rintro ⟨t, u, h, hP, hQ⟩
        rcases t with - | ⟨b, t⟩
        · right
          rw [List.nil_append] at h
          rw [← h] at hQ
          exact hQ
        · left
          rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (ListBlank.mk (List.map some S.reverse)).nth n = S.reverse[n]?

Tactic:
ListBlank.nth_mk,

Goal state after:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (List.map some S.reverse).getI n = S.reverse[n]?
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ((addBottom L).tail.nth n).1 = false

Tactic:
addBottom,

Goal state after:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ((ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)).tail.nth n).1 = false
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ (addBottom L).head.1 = true

Tactic:
addBottom,

Goal state after:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ (ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)).head.1 = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (Language.map f) (char a).matches' = (map f (char a)).matches'

Tactic:
exact image_singleton

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

Goal state before:
pp: case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (trNormal dec q) v
      (trTape' enc0 (ListBlank.cons (f a v) L).tail (ListBlank.cons (ListBlank.cons (f a v) L).head R)))
    (trCfg enc enc0 (stepAux q v (Tape.write (f a v) (Tape.mk' L (ListBlank.cons a R)))))

Tactic:
simpa using! IH ..

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

Goal state before:
pp: case prim.zero
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
⊢ ∃ c, ∀ (v : List.Vector ℕ 0), c.eval ↑v = pure <$> (↑fun x ↦ 0) v

Tactic:
exact ⟨zero', fun ⟨[], _⟩ => rfl⟩

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

Goal state before:
pp: case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0

Tactic:
rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]

Goal state after:
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
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
⊢ (ListBlank.mk (List.map some (S k)).reverse).nth i = (List.map some tl).reverse.getI i

Tactic:
ListBlank.nth_mk,

Goal state after:
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
⊢ (List.map some (S k)).reverse.getI i = (List.map some tl).reverse.getI i
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
⊢ fst f g ≫ f = snd f g ≫ g

Tactic:
by
  ext ⟨_, h⟩; exact h

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

Goal state after:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
rsuffices ⟨⟨s, hs, hs'⟩, hs''⟩ : ∃ s : N, s.val ⊆ U

Goal state after:
case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
s : Set X
hs : IsClopen s
hs' : x ∈ s
hs'' : ↑⟨s, ⋯⟩ ⊆ U
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := ⋯
⊢ ∃ s, ↑s ⊆ U
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: 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 : ℕ
⊢ (ListBlank.mk (List.map (proj k').f (List.map (fun a ↦ update default k (some a)) L.reverse))).nth i =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i

Tactic:
ListBlank.nth_mk,

Goal state after:
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 : ℕ
⊢ (List.map (proj k').f (List.map (fun a ↦ update default k (some a)) L.reverse)).getI i =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i
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
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
i : ℕ
this : ((proj k).f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k).f (update default k (some a))
⊢ (Option.map (fun a ↦ some a) L.reverse[i]?).getD default = (ListBlank.mk (List.map some L).reverse).nth i

Tactic:
ListBlank.nth_mk,

Goal state after:
case pos
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)
i : ℕ
this : ((proj k).f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k).f (update default k (some a))
⊢ (Option.map (fun a ↦ some a) L.reverse[i]?).getD default = (List.map some L).reverse.getI i
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 ↦ default k') L.reverse[i]?).getD default = (ListBlank.mk (List.map some []).reverse).nth i

Tactic:
ListBlank.nth_mk,

Goal state after:
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 ↦ default k') L.reverse[i]?).getD default = (List.map some []).reverse.getI i
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ CompactT2.Projective (StoneCech X)

Tactic:
intro Y

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y : Type u
⊢ ∀ {Z : Type u} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] [CompactSpace Y] [T2Space Y] [CompactSpace Z]
    [T2Space Z] {f : StoneCech X → Z} {g : Y → Z},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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
this : closure U = φ ⁻¹' Z₂
⊢ IsClosed (g ⁻¹' Subtype.val ⁻¹' Z₁)

pp: 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
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅

Tactic:
· exact hZ₁.preimage hφ

Goal state after:
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
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅
Module: Mathlib.Topology.Category.Profinite.EffectiveEpi

Goal state before:
pp: B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

Goal state after:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE
Module: Mathlib.Topology.Category.Stonean.EffectiveEpi

Goal state before:
pp: B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

Goal state after:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_2.refine_1
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false

pp: case refine_2.refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (unrev q), var := none,
      stk := update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }

Tactic:
· exact fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)

Goal state after:
case refine_2.refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (unrev q), var := none,
      stk := update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x y : X
⊢ y ∈ ofPred ((connectedComponentSetoid X) x) ↔ y ∈ connectedComponent x

Tactic:
simpa only [connectedComponentSetoid, ← connectedComponent_eq_iff_mem] using! eq_comm

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

Goal state before:
pp: case fix
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 Γ'
⊢ ∃ b₂,
    TrCfg (stepRet (Cont.fix f k) v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

Tactic:
rw [stepRet]
    have :
      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 := by
      obtain - | n := v
      · exact ⟨rfl, rfl⟩
      rcases n with - | n
      · simp
      rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]
      cases (n : Num).succ' <;> exact ⟨rfl, rfl⟩
    by_cases h : v.headI = 0 <;> simp only [h, ite_true, ite_false] at this ⊢
    · obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?
      refine ⟨c, h₁, TransGen.head rfl ?_⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]
      exact h₂
    · obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)
      refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this.1]
      convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
      · simp
        convert! rfl
      · exact fun x h => trNat_natEnd _ _ (List.tail_subset _ h)
      · exact ⟨rfl, this.2⟩

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

Goal state before:
pp: c : Code
v : List ℕ
⊢ eval (TM2.step tr) (init c v) = halt <$> c.eval v

Tactic:
obtain ⟨i, h₁, h₂⟩ := tr_init c v

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
⊢ eval (TM2.step tr) (init c v) = halt <$> c.eval v