mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: m n : ℕ
h : m < 2 ^ n
⊢ m.size ≤ n

Tactic:
induction m using binaryRec' generalizing n with
    | zero => simp
    | bit b m e IH =>
      rw [← Nat.bit_ne_zero_iff] at e
      rw [size_bit e]
      cases n with
      | zero => exact (e (Nat.lt_one_iff.mp h)).elim
      | succ n => exact succ_le_succ (IH (bit_lt_two_pow_succ_iff.mp h))

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
⊢ bitwise (swap f) = swap (bitwise f)

Tactic:
funext m n
  simp only [Function.swap]
  induction m using Nat.binaryRec' generalizing n with
  | zero => simp
  | bit bm m hm ihm =>
    induction n using Nat.binaryRec' with
    | zero => simp
    | bit bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ a ^^^ b < c

Tactic:
hab

Goal state after:
case inr.inr
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ c ^^^ v < c
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: m n : ℕ
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
by
  by_cases h : (m + n) % 2 = 0
  · simp only [h, mod_two_eq_zero_iff_testBit_zero, testBit_zero, xor_mod_two_eq_one, decide_not,
      Bool.decide_iff_dist, Bool.not_eq_false', beq_iff_eq, decide_eq_decide]
    lia
  · simp only [mod_two_ne_zero] at h
    simp only [h, xor_mod_two_eq_one]
    lia

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
n x : ℕ
⊢ x ∈ c.eval n ↔ x ∈ rfindOpt fun k ↦ evaln k c n

Tactic:
by
    refine evaln_complete.trans (Nat.rfindOpt_mono ?_).symm
    intro a m n hl; apply evaln_mono hl

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s : σ
hs : s ∈ M.εClosure ∅
⊢ False

Tactic:
induction hs <;> assumption

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ M.stepSet ∅ a = ∅

Tactic:
stepSet_empty

Goal state after:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ ∅ = ∅
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') → ∃ n, M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
· simp_rw [List.reduceOption_eq_nil_iff]
      intro ⟨_, ⟨n, rfl⟩, h⟩
      exact ⟨n, h⟩

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) → ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
intro ⟨t, ht, h⟩

Goal state after:
case append_singleton.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : s₂ ∈ M.εClosure (M.step t (some a))
⊢ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
h : L.IsRegular
⊢ (Set.range L.leftQuotient).Finite

Tactic:
have ⟨σ, x, M, hM⟩ := h

Goal state after:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range L.leftQuotient).Finite
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
L : Language α
s : ↑(Set.range L.leftQuotient)
a : α
y : List α
hy : L.leftQuotient y = ↑s
⊢ (↑s).leftQuotient [a] ∈ Set.range L.leftQuotient

Tactic:
exists y ++ [a]

Goal state after:
α : Type u
σ : Type v
L : Language α
s : ↑(Set.range L.leftQuotient)
a : α
y : List α
hy : L.leftQuotient y = ↑s
⊢ L.leftQuotient (y ++ [a]) = (↑s).leftQuotient [a]
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
⊢ (m + n).toZNum = m.toZNum + n.toZNum

Tactic:
by
  cases m <;> cases n <;> rfl

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
⊢ BlankRel l₁ l₂ → BlankRel l₂ l₃ → BlankRel l₁ l₃

Tactic:
grind [eq_def, BlankExtends.below_of_le, BlankExtends.above_of_le, BlankExtends.trans]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
⊢ Reaches f a b ∧ f b = none

pp: case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a

Tactic:
· refine evalInduction h fun a h IH ↦ ?_
    rcases e : f a with - | a'
    · rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]
      exact ⟨ReflTransGen.refl, e⟩
    · rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩) <;> rw [e] at h <;>
        cases Part.mem_some_iff.1 h
      obtain ⟨h₁, h₂⟩ := IH a' e
      exact ⟨ReflTransGen.head e h₁, h₂⟩

Goal state after:
case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case inr
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
⊢ mk l₁ = mk l₂

Tactic:
cases le_total l₁.length l₂.length <;> [skip; symm]

Goal state after:
case inr.inl
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
h✝ : l₁.length ≤ l₂.length
⊢ mk l₁ = mk l₂

case inr.inr
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
h✝ : l₂.length ≤ l₁.length
⊢ mk l₂ = mk l₁
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ mk l₁ = mk l₂

Tactic:
refine Quotient.sound' (Or.inl ⟨l₂.length - l₁.length, ?_⟩)

Goal state after:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default
Module: Mathlib.Computability.StateTransition

Goal state before:
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₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ b✝ g₂
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩

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₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ b✝ g₂
d' : σ₂
cd' : d' ∈ f₂ b✝
dg : ReflTransGen (fun a b ↦ b ∈ f₂ a) d' g₂
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c

Tactic:
by rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]

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

Goal state before:
pp: case branch.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

pp: case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

pp: case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
· unfold stmts₁ at h₀₁
      exact h₀₁

Goal state after:
case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch f q₁ q₂)
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

pp: case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

pp: case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
· unfold stmts₁ at h₀₁
      exact h₀₁

Goal state after:
case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case load.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
a✝ : σ → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (load a✝ q)
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

pp: case load.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

Tactic:
· unfold stmts₁ at h₀₁
      exact h₀₁

Goal state after:
case load.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case push.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Γ k✝
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (push k✝ a✝ q)
IH : push k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (push k✝ a✝ q) (stmts₁ q)

pp: case push.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Γ k✝
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (push k✝ a✝ q) (stmts₁ q)

Tactic:
· unfold stmts₁ at h₀₁
      exact h₀₁

Goal state after:
case push.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Γ k✝
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (push k✝ a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case peek.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (peek k✝ a✝ q)
IH : peek k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (peek k✝ a✝ q) (stmts₁ q)

pp: case peek.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (peek k✝ a✝ q) (stmts₁ q)

Tactic:
· unfold stmts₁ at h₀₁
      exact h₀₁

Goal state after:
case peek.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (peek k✝ a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (pop k✝ a✝ q)
IH : pop k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

pp: case pop.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Tactic:
· unfold stmts₁ at h₀₁
      exact h₀₁

Goal state after:
case pop.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)
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
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
this :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' ?m.41 ?m.42 σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
rw [read, this, stepAux_move, encdec, trTape'_move_left enc0]
    simp only [ListBlank.head_cons, ListBlank.cons_head_tail, ListBlank.tail_cons]

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
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
clear f L a R

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 : σ
⊢ ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case halt
k' : Cont
v : List ℕ
⊢ (halt.then k').eval v = halt.eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, pure_bind]

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
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
⊢ univ.PairwiseDisjoint (C ∘ ⇑e.symm)

Tactic:
simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]

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

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

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

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

Goal state before:
pp: X Y : CompHaus
Z : Stonean
e : Z.compHaus ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e

Tactic:
by simp [lift]

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

Goal state before:
pp: X Y : Profinite
Z : Stonean
e : Stonean.toProfinite.obj Z ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e

Tactic:
by simp [lift]

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

Goal state before:
pp: case cons.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ ∃ s',
    Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList (0 :: v)) [] c d }
      (Nat.rec { l := some q₁, var := s', stk := elim (trList (0 :: v).tail) [] c d }
        (fun n x ↦ { l := some q₂, var := s', stk := elim (trList (n :: (0 :: v).tail)) [] c d }) (0 :: v).headI)

Tactic:
refine ⟨some Γ'.cons, TransGen.single ?_⟩
    simp

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

Tactic:
have H₁ : ∀ Q₁ Q₂, Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂} := fun _ _ h => by
    rw [← compat _ _ h]
    exact fiber_subset_ofLE _ _
  obtain ⟨x, hx⟩ : Set.Nonempty (⋂ Q, proj Q ⁻¹' {Qs Q}) :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
      (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _}) (directed_of_isDirected_ge H₁)
      (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
      (fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _
  exact ⟨x, mem_iInter.1 hx⟩

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

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
let ff := (f.map ι).flip

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
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:
simp only [codeSupp, codeSupp', trNormal, Finset.union_assoc, contSupp]

Goal state after:
f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
rw [contSupp_cons₁, Finset.union_subset_iff] at H₁

Goal state after:
case cons₁
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x ↦ false) aux stack (trNormal a✝¹ a✝.cons₂)))) ⊆
      S ∧
    codeSupp a✝¹ a✝.cons₂ ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.cons₁ a✝¹ a✝)))