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

Goal state before:
pp: a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
⊢ Primrec fun p ↦
    (fun a n ↦
        Nat.casesOn (ofNat (ℕ × Code) a.length).1 Option.none fun k' ↦
          Code.recOn (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
            (fun cf cg x x_1 ↦ do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) n
              let y ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
              some (Nat.pair x y))
            (fun cf cg x x_1 ↦ do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
              lup a ((ofNat (ℕ × Code) a.length).1, cf) x)
            (fun cf cg x x_1 ↦
              have z := (unpair n).1;
              Nat.casesOn (unpair n).2 (lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun y ↦ do
                let i ← lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y)
                lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun cf x ↦
            have z := (unpair n).1;
            have m := (unpair n).2;
            do
            let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m)
            Nat.casesOn x (some m) fun x ↦ lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1)))
      p.1 p.2

Tactic:
have n := Primrec.snd (α := List (List (Option ℕ))) (β := ℕ)

Goal state after:
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n : Primrec Prod.snd
⊢ Primrec fun p ↦
    (fun a n ↦
        Nat.casesOn (ofNat (ℕ × Code) a.length).1 Option.none fun k' ↦
          Code.recOn (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
            (fun cf cg x x_1 ↦ do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) n
              let y ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
              some (Nat.pair x y))
            (fun cf cg x x_1 ↦ do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
              lup a ((ofNat (ℕ × Code) a.length).1, cf) x)
            (fun cf cg x x_1 ↦
              have z := (unpair n).1;
              Nat.casesOn (unpair n).2 (lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun y ↦ do
                let i ← lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y)
                lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun cf x ↦
            have z := (unpair n).1;
            have m := (unpair n).2;
            do
            let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m)
            Nat.casesOn x (some m) fun x ↦ lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1)))
      p.1 p.2
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.zero
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ n ≤ m * l + n

Tactic:
add_comm

Goal state after:
case a.zero
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ n ≤ n + m * l
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (2 * x + 1) / 2 = x

Tactic:
add_comm

Goal state after:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (1 + 2 * x) / 2 = x
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : i = 0
⊢ bit b n < bit b' m

pp: case neg
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i = 0
⊢ bit b n < bit b' m

Tactic:
· subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _

Goal state after:
case neg
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i = 0
⊢ bit b n < bit b' m
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (n + m)

Tactic:
add_comm

Goal state after:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
⊢ M.toDFA.accepts = M.accepts

Tactic:
ext x
  rw [mem_accepts, DFA.mem_accepts]
  constructor <;> · exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

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

Goal state before:
pp: x✝¹ x✝ : Num
⊢ ↑x✝¹ + ↑x✝ = ↑x✝ + ↑x✝¹

Tactic:
add_comm

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

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:
· intro ⟨n, _⟩
      use List.replicate n none
      rw [List.reduceOption_replicate_none]
      trivial

Goal state after:
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)
Module: Mathlib.Computability.Halting

Goal state before:
pp: C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
⊢ ComputablePred fun c ↦ c ∈ C

Tactic:
{
          obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _}

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑n.bit0 = 2 * ↑n

Tactic:
← bit0_of_bit0,

Goal state after:
α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑(n + n) = 2 * ↑n
Module: Mathlib.Computability.Reduce

Goal state before:
pp: d₁ d₂ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂

Tactic:
induction d₁ using ManyOneDegree.ind_on
  induction d₂ using ManyOneDegree.ind_on
  intro hp hq
  simp_all only [ManyOneEquiv, of_le_of, of_eq_of, true_and]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
x : List α
⊢ (char a).rmatch (head✝ :: x) = true ↔ head✝ :: x = [a]

Tactic:
rcases x with - | ⟨head, tail⟩

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (char a).rmatch [head✝] = true ↔ [head✝] = [a]

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ (char a).rmatch (head✝ :: head :: tail) = true ↔ head✝ :: head :: tail = [a]
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)

Tactic:
iterate_succ',

Goal state after:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v ((Tape.move d)^[i + 1] T)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
⊢ ∀ {L' R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
        Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
intro _ _ l₁ l₂ e

Goal state after:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₁ l₂ : List Bool
e : (enc a).toList = l₁.reverseAux l₂
⊢ (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m ||| n) = ↑m ||| ↑n

Tactic:
apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y) <;>
    (try rintro (_ | _))

Goal state after:
case gff
⊢ (false || false) = false

case f00
⊢ 0 ||| 0 = 0

case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0

case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0

case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0

case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0

case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0

case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0

case fnn.one
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)

case fnn.bit1
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit1 ||| pos n = pos (a✝.bit1.lor n)

case fnn.bit0
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit0 ||| pos n = pos (a✝.bit0.lor n)

case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0

case p1b.false
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)

case p1b.true
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)

case pb1.false
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)

case pb1.true
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)

case pbb.false
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))

case pbb.true
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case right.e_a.e_a.cons
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) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[tail✝.length + 1] (Tape.mk' ∅ (addBottom L)))).head.2 k =
    (head✝ :: tail✝).head?

Tactic:
iterate_succ',

Goal state after:
case right.e_a.e_a.cons
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) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (Tape.move Dir.left ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[tail✝.length]) (Tape.mk' ∅ (addBottom L)))).head.2
      k =
    (head✝ :: tail✝).head?
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
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
⊢ TM1.stepAux q (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.2 k))
      (Tape.write
        ((Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.1,
          update (Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L)))).head.2 k none)
        (Tape.move Dir.left ((Tape.move Dir.right)^[tl.length + 1] (Tape.mk' ∅ (addBottom L))))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))

Tactic:
iterate_succ',

Goal state after:
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
⊢ TM1.stepAux q
      (f v
        ((Tape.move Dir.left
                ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[tl.length]) (Tape.mk' ∅ (addBottom L)))).head.2
          k))
      (Tape.write
        ((Tape.move Dir.left
                ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[tl.length]) (Tape.mk' ∅ (addBottom L)))).head.1,
          update
            (Tape.move Dir.left
                  ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[tl.length]) (Tape.mk' ∅ (addBottom L)))).head.2
            k none)
        (Tape.move Dir.left ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[tl.length]) (Tape.mk' ∅ (addBottom L))))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: case snd
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ (↑((ConcreteCategory.hom a) z)).2 = (↑((ConcreteCategory.hom b) z)).2

Tactic:
exact hsnd

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then TM1.stepAux (trNormal q) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (goto fun x x_1 ↦ ret q) v
        (Tape.move Dir.left ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L))))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
iterate_succ',

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then
      TM1.stepAux (trNormal q) v ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[n]) (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (goto fun x x_1 ↦ ret q) v
        (Tape.move Dir.left ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[n]) (Tape.mk' ∅ (addBottom L))))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
intro h
      obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
        this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl
      refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
      simp only [Part.eq_some_iff.2 hv₁, Part.map_some]
      split_ifs at hv₂ ⊢
      · rw [Part.mem_some_iff.1 hv₂]
        exact Or.inl (Part.mem_some _)
      · exact Or.inr ⟨_, Part.mem_some _, hv₂⟩

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

Goal state before:
pp: case refine_1.inl.inr
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')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M (ret q✝))

pp: case refine_1.inr
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')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)

Tactic:
· unfold TM1.SupportsStmt TM2to1.tr
        exact ⟨IH₁, fun _ _ ↦ hret⟩

Goal state after:
case refine_1.inr
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')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let v ← (fun v ↦ g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)

Tactic:
simp only [bind_assoc]

Goal state after:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let x ← g.eval v
    let v ← f.eval x
    eval step (Cfg.ret k v)
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₂
⊢ IsOpen (closure U)

Tactic:
have hZ₁₂ : Disjoint Z₁ Z₂ := disjoint_left.2 fun x hx₁ hx₂ => by cases hx₁.2.symm.trans hx₂.2

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₂
⊢ IsOpen (closure U)
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₂
⊢ IsOpen (closure U)

Tactic:
have hZ₁ : IsClosed Z₁ := hU.isClosed_compl.prod (T1Space.t1 _)

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₁
⊢ IsOpen (closure U)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ {a}.Nonempty

Tactic:
exact singleton_nonempty a

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
⊢ ofLE h₂ (ofLE h₁ x) = ofLE ⋯ x

Tactic:
by
  rcases x with ⟨⟩
  rfl

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

Goal state before:
pp: case h
X : Profinite
a : (fun X ↦ ↑X.toTop) (limitCone X.diagram).pt
b : ↑X.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toTop), Q.proj b = ↑a Q
⊢ ∀ (x : DiscreteQuotient ↑X.toTop),
    ↑((ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) b) x = ↑a x

Tactic:
rintro S

Goal state after:
case h
X : Profinite
a : (fun X ↦ ↑X.toTop) (limitCone X.diagram).pt
b : ↑X.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toTop), Q.proj b = ↑a Q
S : DiscreteQuotient ↑X.toTop
⊢ ↑((ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) b) S = ↑a S