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

Goal state before:
pp: k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n x : ℕ
left✝ : n ≤ k
⊢ Nat.rec (evaln (k + 1) cf (unpair n).1)
        (fun n_1 n_ih ↦
          (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
            evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 =
      some x →
    x ∈
      Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
        (unpair n).2

Tactic:
induction n.unpair.2 generalizing x with simp [Option.bind_eq_some_iff]
      | zero => apply hf
      | succ m IH =>
        refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
        · have := evaln_mono k.le_succ h₁
          simp [evaln, Option.bind_eq_some_iff] at this
          exact this.2
        · exact hg _ _ h₂

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
⊢ ∀ C ≥ 2 * c₁, (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n

Tactic:
intro C hC h_ind

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
⊢ (1 + ε ↑n) * asympBound g a b n ≤ C * T n
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ 1 + l∗ * l = l∗

Tactic:
mul_self_kstar_comm,

Goal state after:
α : Type u_1
l : Language α
⊢ 1 + l * l∗ = l∗
Module: Mathlib.Data.Nat.Bitwise

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

Tactic:
by
  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 succ
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
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)) =
    match Fin.ofNat 4 (n + ↑(Fin.ofNat 4 1)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
rw [List.range_succ, List.foldl_append, ih, ← Fin.ofNat_add, List.foldl_cons, List.foldl_nil]

Goal state after:
case succ
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
⊢ (match Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match Fin.ofNat 4 n + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m : PosNum
⊢ ∀ (n : PosNum), (m.cmp n).swap = n.cmp m

Tactic:
induction m with

Goal state after:
case one
⊢ ∀ (n : PosNum), (one.cmp n).swap = n.cmp one

case bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit1.cmp n).swap = n.cmp m.bit1

case bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit0.cmp n).swap = n.cmp m.bit0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one.one
⊢ Ordering.eq.swap = Ordering.eq

Tactic:
{ rfl }

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

Goal state before:
pp: case one.bit1
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
{ rfl }

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

Goal state before:
pp: case one.bit0
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
{ rfl }

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

Goal state before:
pp: case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
{ rfl }

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

Goal state before:
pp: case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
{ rfl }

Goal state after:
case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

Tactic:
{ rfl }

Goal state after:
case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
{ rfl }

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

Goal state before:
pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

Tactic:
{ rfl }

Goal state after:
case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
{ rfl }

Goal state after:
case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept

Tactic:
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u ([] ++ y) → ∃ t, M.IsPath s t [] ∧ M.IsPath t u y

Tactic:
List.nil_append

Goal state after:
case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u y → ∃ t, M.IsPath s t [] ∧ M.IsPath t u y
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
⊢ M.IsPath s u (x ++ y) → ∃ t, M.IsPath s t x ∧ M.IsPath t u y

Tactic:
by
    induction x generalizing s with
    | nil =>
      rw [List.nil_append]
      tauto
    | cons x a ih =>
      rintro (_ | ⟨t, _, _, _, _, _, h⟩)
      apply ih at h
      tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ [] = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
trivial

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mpr.cons
α : 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₂ : σ
x' : List (Option α)
left✝¹ : x'.reduceOption = x
n : ℕ
t : σ
left✝ : M.IsPath s₁ t x'
u : σ
a✝¹ : u ∈ M.step t (some a)
a✝ : M.IsPath u s₂ (List.replicate n none)
⊢ ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
use t

Goal state after:
case h
α : 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₂ : σ
x' : List (Option α)
left✝¹ : x'.reduceOption = x
n : ℕ
t : σ
left✝ : M.IsPath s₁ t x'
u : σ
a✝¹ : u ∈ M.step t (some a)
a✝ : M.IsPath u s₂ (List.replicate n none)
⊢ t ∈ M.evalFrom {s₁} x ∧ s₂ ∈ M.εClosure (M.step t (some a))
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
⊢ L.leftQuotient (y ++ [a]) = (L.leftQuotient y).leftQuotient [a]

Tactic:
leftQuotient_append

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).leftQuotient [a] = (L.leftQuotient y).leftQuotient [a]
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero.zero
⊢ (zero.cmp zero).swap = zero.cmp zero

Tactic:
{ rfl }

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

Goal state before:
pp: case zero.pos
a✝ : PosNum
⊢ (zero.cmp (pos a✝)).swap = (pos a✝).cmp zero

Tactic:
{ rfl }

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

Goal state before:
pp: case pos.zero
a✝ : PosNum
⊢ ((pos a✝).cmp zero).swap = zero.cmp (pos a✝)

Tactic:
{ rfl }

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

Goal state before:
pp: case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)

Tactic:
{ rfl }

Goal state after:
case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type ?u.5
f : σ → Option σ
b : σ
C : σ → Sort u_1
a : σ
h : b ∈ eval f a
H : (a : σ) → b ∈ eval f a → ((a' : σ) → f a = some a' → C a') → C a
a' : σ
ha' : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
h' : (a'' : σ) → Sum.inr a'' ∈ Part.some ((f a').elim (Sum.inl a') Sum.inr) → C a''
b' : σ
e : f a' = some b'
⊢ Sum.inr b' = (f a').elim (Sum.inl a') Sum.inr

Tactic:
rw [e]; rfl

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Sum.inl ?m.69 = (f a).elim (Sum.inl a) Sum.inr

Tactic:
rw [e]; rfl

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

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
hs : True
⊢ SupportsStmt S halt

Tactic:
trivial

Goal state after:
Module: Mathlib.Computability.RegularExpressions

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

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

Tactic:
· exact of_decide_eq_true rfl

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

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

Tactic:
unfold TM1.stmts₁

Goal state after:
case right.some.some.move.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
h₂ : some (TM1.Stmt.move d val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.move d val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), move d) → TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ val✝ ∈ insert (TM1.Stmt.move d val✝) (TM1.stmts₁ val✝)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
unfold TM1.stmts₁

Goal state after:
case right.some.some.write.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → Γ
h₂ : some (TM1.Stmt.write b val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.write b val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), write (b a v')) →
        TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ val✝ ∈ insert (TM1.Stmt.write b val✝) (TM1.stmts₁ val✝)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
unfold TM1.stmts₁

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

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

Tactic:
List.nil_append

Goal state after:
case pos.mpr.nil
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
h : a :: x = u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
unfold TM1.stmts₁

Goal state after:
case right.some.some.branch.false
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (bif false then trAux M a q₁ v else trAux M a q₂ v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = false
⊢ q₂ ∈ insert (TM1.Stmt.branch p q₁ q₂) (TM1.stmts₁ q₁ ∪ TM1.stmts₁ q₂)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
unfold TM1.stmts₁

Goal state after:
case right.some.some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (bif true then trAux M a q₁ v else trAux M a q₂ v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = true
⊢ q₁ ∈ insert (TM1.Stmt.branch p q₁ q₂) (TM1.stmts₁ q₁ ∪ TM1.stmts₁ q₂)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
hs : True
⊢ SupportsStmt S halt

Tactic:
trivial

Goal state after:
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
· rintro ⟨S, hsum, helem⟩
      rcases x with - | ⟨a, x⟩
      · rfl
      · rw [rmatch, deriv, mul_rmatch_iff]
        rcases S with - | ⟨t', U⟩
        · exact ⟨[], [], by tauto⟩
        · obtain - | ⟨b, t⟩ := t'
          · simp only [forall_eq_or_imp, List.mem_cons] at helem
            simp only [not_true, Ne, false_and] at helem
          simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum
          refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
          · specialize helem (b :: t) (by simp)
            rw [rmatch] at helem
            convert! helem.2
            exact hsum.1
          · grind

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

Goal state before:
pp: case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos (a✝ <<< n)) = ↑(pos a✝) <<< n

Tactic:
simp only [cast_pos]

Goal state after:
case pos
n : ℕ
a✝ : PosNum
⊢ ↑(a✝ <<< n) = ↑a✝ <<< n