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

Goal state before:
pp: case prec
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k₂ + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k₂ (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k₂ + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case prec
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
h :
  x ∈
    unpaired
      (fun a n ↦
        Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
          let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
          evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
      n
⊢ x ∈
    unpaired
      (fun a n ↦
        Nat.casesOn n (evaln (k₂ + 1) a✝¹ a) fun y ↦ do
          let i ← evaln k₂ (a✝¹.prec a✝) (Nat.pair a y)
          evaln (k₂ + 1) a✝ (Nat.pair a (Nat.pair y i)))
      n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k₂ + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k₂ a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case rfind'
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x
h :
  x ∈
    unpaired
      (fun a m ↦ do
        let x ← evaln (k + 1) a✝ (Nat.pair a m)
        if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
      n
⊢ x ∈
    unpaired
      (fun a m ↦ do
        let x ← evaln (k₂ + 1) a✝ (Nat.pair a m)
        if x = 0 then pure m else evaln k₂ a✝.rfind' (Nat.pair a (m + 1)))
      n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case hbc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ #(Ico (r i n) n) • (c₂ * g ↑n / ↑n ^ (p a b + 1)) ≤ ∑ _u ∈ Ico (r i n) n, c₂ * g ↑n / ↑n ^ (p a b + 1)

Tactic:
exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)

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

Goal state before:
pp: case hbc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ #(Ico (r i n) n) • (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) ≤ ∑ _u ∈ Ico (r i n) n, c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)

Tactic:
exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  ∃ a,
    evaln (k + 1) a✝ n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

Tactic:
case rfind' cf hf _ =>
      rcases h with ⟨m, h₁, h₂⟩
      by_cases m0 : m = 0 <;> simp [m0] at h₂
      · exact
          ⟨0, ⟨by simpa [m0] using hf _ _ h₁, fun {m} => (Nat.not_lt_zero _).elim⟩, by simp [h₂]⟩
      · have := evaln_sound h₂
        simp [eval] at this
        rcases this with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩
        refine
          ⟨y + 1, ⟨by simpa [add_comm, add_left_comm] using hy₁, fun {i} im => ?_⟩, by
            simp [add_comm, add_left_comm]⟩
        rcases i with - | i
        · exact ⟨m, by simpa using hf _ _ h₁, m0⟩
        · rcases hy₂ (Nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩
          exact ⟨z, by simpa [add_comm, add_left_comm] using hz, z0⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec.succ
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ m : ℕ
IH :
  ∀ {n x : ℕ},
    x ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m →
      ∃ k,
        n ≤ k ∧
          Nat.rec (evaln (k + 1) cf n₁)
              (fun n n_ih ↦
                (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
              m =
            some x
n x y : ℕ
hy : y ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m
hx : x ∈ cg.eval (Nat.pair n₁ (Nat.pair m y))
k₁ : ℕ
nk₁ : max n (Nat.pair n₁ m) ≤ k₁
hk₁ :
  Nat.rec (evaln (k₁ + 1) cf n₁)
      (fun n n_ih ↦ (evaln k₁ (cf.prec cg) (Nat.pair n₁ n)).bind fun i ↦ evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n i)))
      m =
    some y
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m y))
⊢ Nat.pair n₁ m ≤ k₁ ∧
    Nat.rec (evaln (k₁ + 1) cf n₁)
        (fun n n_ih ↦
          (evaln k₁ (cf.prec cg) (Nat.pair n₁ n)).bind fun a ↦ evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n a)))
        m =
      some y

Tactic:
exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'.succ
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
rcases hf ha with ⟨k₁, hk₁⟩

Goal state after:
case rfind'.succ
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Tactic:
induction p with

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ x ∈ (M1.union M2).acceptsFrom (s1, s2) ↔ x ∈ M1.acceptsFrom s1 + M2.acceptsFrom s2

Tactic:
simp only [acceptsFrom]

Goal state after:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ x ∈ {x | (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept} ↔
    x ∈ {x | M1.evalFrom s1 x ∈ M1.accept} + {x | M2.evalFrom s2 x ∈ M2.accept}
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case bit
b : Bool
n : ℕ
h : n = 0 → b = true
IH : n < 2 ^ n.size
⊢ bit b n < 2 ^ (bit b n).size

Tactic:
← Nat.bit_ne_zero_iff

Goal state after:
case bit
b : Bool
n : ℕ
h : bit b n ≠ 0
IH : n < 2 ^ n.size
⊢ bit b n < 2 ^ (bit b n).size
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case bit
b : Bool
m : ℕ
e : m = 0 → b = true
IH : ∀ {n : ℕ}, m < 2 ^ n → m.size ≤ n
n : ℕ
h : bit b m < 2 ^ n
⊢ (bit b m).size ≤ n

Tactic:
← Nat.bit_ne_zero_iff

Goal state after:
case bit
b : Bool
m : ℕ
e : bit b m ≠ 0
IH : ∀ {n : ℕ}, m < 2 ^ n → m.size ≤ n
n : ℕ
h : bit b m < 2 ^ n
⊢ (bit b m).size ≤ n
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl.false
n i : ℕ
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit i = (false.toNat * 2 ^ i).testBit i

pp: case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i

pp: case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

pp: case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j

Tactic:
· simp [h]

Goal state after:
case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i

case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i

pp: case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

pp: case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j

Tactic:
· simp [h]

Goal state after:
case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ M.evalFrom S (x ++ y) = M.evalFrom (M.evalFrom S x) y

Tactic:
by
  simp only [evalFrom, List.foldl_append]

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

Goal state before:
pp: n : Num
⊢ (↑n + 1).pred = ↑n

Tactic:
Nat.add_one,

Goal state after:
n : Num
⊢ (↑n).succ.pred = ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ (↑n).pred + 1 = ↑n

Tactic:
Nat.add_one,

Goal state after:
n : PosNum
⊢ (↑n).pred.succ = ↑n
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr
α : 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 : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
· exact Or.inr ha

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg Γ Λ
⊢ c' ∈ step M { q := q, Tape := T } → { q := q, Tape := T }.q ∈ S → c'.q ∈ S

Tactic:
h₁

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg Γ Λ
h₁ : c' ∈ step M { q := q, Tape := T }
⊢ { q := q, Tape := T }.q ∈ S → c'.q ∈ S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

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

Tactic:
· exact h₀₁

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

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ d₂ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
⊢ ManyOneEquiv p₁ p₂ → d₂.liftOn (f p₁) ⋯ = d₂.liftOn (f p₂) ⋯

Tactic:
hp

Goal state after:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ d₂ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
⊢ d₂.liftOn (f p₁) ⋯ = d₂.liftOn (f p₂) ⋯
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

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

Tactic:
· exact h₀₁

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

Goal state before:
pp: case load.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
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
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
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:
· exact h₀₁

Goal state after:
case load.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
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.PostTuringMachine

Goal state before:
pp: case right
Γ : 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
q : Λ' M
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
⊢ (q', s) ∈ tr M q a → q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts M S)

Tactic:
h₁

Goal state after:
case right
Γ : 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
q : Λ' M
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
h₁ : (q', s) ∈ tr M q a
⊢ q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts M S)
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
rintro (_ | _)

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

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

Tactic:
rintro (_ | _)

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:
rintro (_ | _)

Goal state after:
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
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:
rintro (_ | _)

Goal state after:
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
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)

Tactic:
rintro (_ | _)

Goal state after:
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)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0

Tactic:
rintro (_ | _)

Goal state after:
case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)

Tactic:
rintro (_ | _)

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

Goal state before:
pp: case cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ l₂' : List Bool
e : l₂'.length = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
rcases l₂' with - | ⟨b, l₂'⟩

Goal state after:
case cons.nil
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
e : [].length = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

case cons.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : (b :: l₂').length = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)

Tactic:
rintro (_ | _)

Goal state after:
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)