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

Goal state before:
pp: case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u

Tactic:
exact hu.1

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u

Tactic:
exact hu.1

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

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 2
⊢ (match 2 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match 2 + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
apply Nat.xor_self

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ [] ∈ M.acceptsFrom S ↔ ∃ s ∈ S, s ∈ M.accept

Tactic:
simp only [mem_acceptsFrom, evalFrom_nil]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.bit0.cmp b.bit0) (↑a.bit0 < ↑b.bit0) (a.bit0 = b.bit0) (↑b.bit0 < ↑a.bit0)

Tactic:
dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.add_lt_add this this
    · rw [this]
    · exact Nat.add_lt_add this this

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

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ ↑a < ↑b ↔ ↑a ≤ ↑b ∧ ¬↑b ≤ ↑a

Tactic:
apply lt_iff_le_not_ge

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x✝ ∈ M.step i s

Tactic:
apply exists_congr

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x✝ ∈ M.step a s
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
L : Language α
s : ↑(Set.range L.leftQuotient)
a : α
⊢ ↑(Set.range L.leftQuotient)

Tactic:
by
    refine ⟨s.val.leftQuotient [a], ?_⟩
    obtain ⟨y, hy⟩ := s.prop
    exists y ++ [a]
    rw [← hy, leftQuotient_append]

Goal state after:
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: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = f.f (l.getD n default)

Tactic:
rw [← List.getD_map _ _ f]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q

Tactic:
cases s

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ TM2.SupportsStmt S (stRun (push a✝) q) ↔ TM2.SupportsStmt S q

case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (peek a✝) q) ↔ TM2.SupportsStmt S q

case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ TM2.SupportsStmt S (stRun (pop a✝) q) ↔ TM2.SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trNormal (stRun s q) = goto fun x x_1 ↦ go k s q

Tactic:
cases s

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ trNormal (stRun (StAct.push a✝) q) = goto fun x x_1 ↦ go k (StAct.push a✝) q

case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.peek a✝) q) = goto fun x x_1 ↦ go k (StAct.peek a✝) q

case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trNormal (stRun (StAct.pop a✝) q) = goto fun x x_1 ↦ go k (StAct.pop a✝) q
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trStmts₁ (stRun s q) = {go k s q, ret q} ∪ trStmts₁ q

Tactic:
cases s

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Γ k
⊢ trStmts₁ (stRun (StAct.push a✝) q) = {go k (StAct.push a✝) q, ret q} ∪ trStmts₁ q

case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trStmts₁ (stRun (StAct.peek a✝) q) = {go k (StAct.peek a✝) q, ret q} ∪ trStmts₁ q

case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
q : TM2.Stmt Γ Λ σ
a✝ : σ → Option (Γ k) → σ
⊢ trStmts₁ (stRun (StAct.pop a✝) q) = {go k (StAct.pop a✝) q, ret q} ∪ trStmts₁ q
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ a = b

Tactic:
exact hsum.1

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

Goal state before:
pp: case gff
⊢ (false && false) = false

Tactic:
try cases_type* Bool

Goal state after:
case gff
⊢ (false && false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 &&& 0 = 0

Tactic:
try cases_type* Bool

Goal state after:
case f00
⊢ 0 &&& 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0

Tactic:
try cases_type* Bool

Goal state after:
case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0

Tactic:
try cases_type* Bool

Goal state after:
case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

Tactic:
try cases_type* Bool

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

Tactic:
try cases_type* Bool

Goal state after:
case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit b✝ n✝) = bit (true && b✝) (bif false && true then pos n✝ else 0)

Tactic:
try cases_type* Bool

Goal state after:
case p1b.false
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit false n✝) = bit (true && false) (bif false && true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit true n✝) = bit (true && true) (bif false && true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land 1 = bit (a✝ && true) (bif true && false then pos m✝ else 0)

Tactic:
try cases_type* Bool

Goal state after:
case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).land 1 = bit (false && true) (bif true && false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).land 1 = bit (true && true) (bif true && false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)

Tactic:
try cases_type* Bool

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : List.Vector ℕ m), cg.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((Vector.mOfFn fun i ↦ g i v) >>= f)

Tactic:
obtain ⟨cf, hf⟩ := hf
    exact
      ⟨cf.comp cg, fun v => by
        simp [hg, hf, map_bind]
        rfl⟩

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

Goal state before:
pp: case gff
⊢ (false && !false) = false

Tactic:
try cases_type* Bool

Goal state after:
case gff
⊢ (false && !false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ ldiff 0 0 = 0

Tactic:
try cases_type* Bool

Goal state after:
case f00
⊢ ldiff 0 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0

Tactic:
try cases_type* Bool

Goal state after:
case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0

Tactic:
try cases_type* Bool

Goal state after:
case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝

Tactic:
try cases_type* Bool

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

Tactic:
try cases_type* Bool

Goal state after:
case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit b✝ n✝) = bit (true && !b✝) (bif false && !true then pos n✝ else 0)

Tactic:
try cases_type* Bool

Goal state after:
case p1b.false
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit false n✝) = bit (true && !false) (bif false && !true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit true n✝) = bit (true && !true) (bif false && !true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff 1 = bit (a✝ && !true) (bif true && !false then pos m✝ else 0)

Tactic:
try cases_type* Bool

Goal state after:
case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff 1 = bit (false && !true) (bif true && !false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff 1 = bit (true && !true) (bif true && !false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff (PosNum.bit b✝ n✝) = bit (a✝ && !b✝) (m✝.ldiff n✝)

Tactic:
try cases_type* Bool

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit false n✝) = bit (false && !false) (m✝.ldiff n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit true n✝) = bit (false && !true) (m✝.ldiff n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit false n✝) = bit (true && !false) (m✝.ldiff n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit true n✝) = bit (true && !true) (m✝.ldiff n✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false != false) = false

Tactic:
try cases_type* Bool

Goal state after:
case gff
⊢ (false != false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 ^^^ 0 = 0

Tactic:
try cases_type* Bool

Goal state after:
case f00
⊢ 0 ^^^ 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0

Tactic:
try cases_type* Bool

Goal state after:
case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0

Tactic:
try cases_type* Bool

Goal state after:
case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

Tactic:
try cases_type* Bool

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

Tactic:
try cases_type* Bool

Goal state after:
case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit b✝ n✝) = bit (true != b✝) (bif false != true then pos n✝ else 0)

Tactic:
try cases_type* Bool

Goal state after:
case p1b.false
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit false n✝) = bit (true != false) (bif false != true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit true n✝) = bit (true != true) (bif false != true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor 1 = bit (a✝ != true) (bif true != false then pos m✝ else 0)

Tactic:
try cases_type* Bool

Goal state after:
case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).lxor 1 = bit (false != true) (bif true != false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).lxor 1 = bit (true != true) (bif true != false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor (PosNum.bit b✝ n✝) = bit (a✝ != b✝) (m✝.lxor n✝)

Tactic:
try cases_type* Bool

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit false n✝) = bit (false != false) (m✝.lxor n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit true n✝) = bit (false != true) (m✝.lxor n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit false n✝) = bit (true != false) (m✝.lxor n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit true n✝) = bit (true != true) (m✝.lxor n✝)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
⊢ TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
cases s

Goal state after:
case move
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Dir
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.move a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

case write
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a✝ : Γ
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.write a✝) q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match TM0.Stmt.write a✝ with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
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 Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  n ≤ S.length →
    Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
      { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
H : n + 1 ≤ S.length
⊢ some
      (bif (L.nth n k).isNone then
        TM1.stepAux (trStAct (goto fun x x_1 ↦ ret q) o) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))
      else
        { l := some (go k o q), var := v,
          Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }) =
    some
      { l := some (go k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }

Tactic:
stk_nth_val _ hL,

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 Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  n ≤ S.length →
    Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
      { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
H : n + 1 ≤ S.length
⊢ some
      (bif S.reverse[n]?.isNone then
        TM1.stepAux (trStAct (goto fun x x_1 ↦ ret q) o) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))
      else
        { l := some (go k o q), var := v,
          Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }) =
    some
      { l := some (go k o q), var := v,
        Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ V ∩ U = ∅

Tactic:
rw [← Set.disjoint_iff_inter_eq_empty, disjoint_comm]

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ Disjoint U V
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
⊢ ∃ E, CompactSpace ↑E ∧ X '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ

Tactic:
by
    rcases zorn_superset S this with ⟨E, E_min⟩
    obtain ⟨E_closed, E_surj⟩ := E_min.prop
    refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
    intro E₀ E₀_min E₀_closed
    contrapose E₀_min
    exact eq_univ_of_image_val_eq <|
      E_min.eq_of_subset ⟨E₀_closed.trans E_closed, image_image_val_eq_domRestrict_image ▸ E₀_min⟩
        image_val_subset

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

Goal state before:
pp: case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }

pp: case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }

Tactic:
· refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))
    rw [tr]
    simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append,
      elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_self,
      List.headI_nil, trNat_default]
    convert! unrev_ok using 2
    simp

Goal state after:
case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }