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

Goal state before:
pp: case inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m < n
⊢ n ∈ rfind p

pp: case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ n ∈ rfind p

pp: case inr.inr
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p

Tactic:
· injection mem_unique (h₂ h) (rfind_spec hm)

Goal state after:
case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ n ∈ rfind p

case inr.inr
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
⊢ Option.map Prod.snd (graph b (m b + 1))[0]? = some (f b)

Tactic:
have graph_eq_map_bindList (i : ℕ) (hi : i ≤ m b + 1) :
        graph b i = (bindList b (m b + 1 - i)).map fun x ↦ (x, f x) := by
      have bindList_eq_nil : bindList b (m b + 1) = [] :=
        have bindList_m_lt (k : ℕ) : ∀ b' ∈ bindList b k, m b' < m b + 1 - k := by
          induction k with simp [bindList]
          | succ k ih =>
            grind
        List.eq_nil_iff_forall_not_mem.mpr
          (by intro b' ha'; by_contra; simpa using bindList_m_lt (m b + 1) b' ha')
      have mapGraph_graph {bs bs' : List β} (has : bs' ⊆ bs) :
          mapGraph (bs.map <| fun x => (x, f x)) bs' = bs'.map f := by
        induction bs' with simp [mapGraph]
        | cons b bs' ih =>
          have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has
          rcases this with ⟨ha, has'⟩
          simpa [List.lookup_graph f ha] using ih has'
      have graph_succ : ∀ i, graph b (i + 1) =
        (bindList b (m b - i)).filterMap fun b' =>
          (g b' <| mapGraph (graph b i) (l b')).map (b', ·) := fun _ => rfl
      have bindList_succ : ∀ i, bindList b (i + 1) = (bindList b i).flatMap l := fun _ => rfl
      induction i with
      | zero => symm; simpa [graph] using bindList_eq_nil
      | succ i ih =>
        simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.le_of_lt_succ hi),
          Nat.succ_eq_add_one, bindList_succ, Nat.reduceSubDiff]
        apply List.filterMap_eq_map_iff_forall_eq_some.mpr
        intro b' ha'; simp; rw [mapGraph_graph]
        · exact H b'
        · exact (List.infix_flatMap_of_mem ha' l).subset
    simp [graph_eq_map_bindList (m b + 1) (Nat.le_refl _), bindList]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 0).encodeCode = 0

Tactic:
by simp [ofNatCode, encodeCode]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 1).encodeCode = 1

Tactic:
by simp [ofNatCode, encodeCode]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 2).encodeCode = 2

Tactic:
by simp [ofNatCode, encodeCode]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 3).encodeCode = 3

Tactic:
by simp [ofNatCode, encodeCode]

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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ 2 ^ (-↑k - 1) * x₀ ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀)

Tactic:
Set.left_mem_Icc

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ 2 ^ (-↑k - 1) * x₀ ≤ 2 ^ (-↑k) * x₀
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (deriv fun x ↦ (fun z ↦ z ^ p a b) x * (fun z ↦ 1 - ε z) x) =ᶠ[atTop] fun x ↦
    deriv (fun z ↦ z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z ↦ 1 - ε z) x

Tactic:
filter_upwards [eventually_ne_atTop 0, eventually_gt_atTop 1] with x hx hx'
      rw [deriv_fun_mul] <;> aesop

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

Goal state before:
pp: ⊢ deriv ε =ᶠ[atTop] fun x ↦ -x⁻¹ / log x ^ 2

Tactic:
filter_upwards with x

Goal state after:
x : ℝ
⊢ deriv ε x = -x⁻¹ / log x ^ 2
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ -deriv ε =ᶠ[atTop] fun x ↦ x⁻¹ / log x ^ 2

Tactic:
filter_upwards with x

Goal state after:
x : ℝ
⊢ (-deriv ε) x = x⁻¹ / log x ^ 2
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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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
⊢ c₂ / c₁ ^ (p a b + 1) ≤ max c₂ (c₂ / c₁ ^ (p a b + 1))

Tactic:
exact le_max_right _ _

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

Goal state before:
pp: case hbc
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ c₄ ≤ max c₂ c₄

Tactic:
exact le_max_right _ _

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

Goal state before:
pp: case refine_3
α : 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'
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ 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:
obtain ⟨c₁, hc₁, h_sumTransform_aux⟩ := R.eventually_atTop_sumTransform_le

Goal state after:
case refine_3
α : 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₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ 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
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ.mpr.cons.refl
α : Type u_1
l : Language α
a : List α
S : List (List α)
hS : a ∈ l ∧ ∀ x ∈ S, x ∈ l
ihn : ∀ {x : List α}, x ∈ l ^ S.length ↔ ∃ S_1, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S_1, b = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten

Tactic:
exact ⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.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:
replace k := k.comp (Primrec.fst (β := ℕ))

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

Goal state before:
pp: m k : ℕ
⊢ 2 * shiftLeft' true m k + 1 + 1 = (m + 1) * 2 ^ (k + 1)

Tactic:
Nat.add_assoc,

Goal state after:
m k : ℕ
⊢ 2 * shiftLeft' true m k + (1 + 1) = (m + 1) * 2 ^ (k + 1)
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: m n : ℕ
⊢ m < n.size ↔ ¬n < 2 ^ m

Tactic:
Decidable.iff_not_comm,

Goal state after:
m n : ℕ
⊢ n < 2 ^ m ↔ ¬m < n.size
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : filterMap id l₂ = []
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
rw [filterMap_eq_nil_iff] at hl₂

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T → ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x

Tactic:
rintro (⟨s, hs, h⟩ | ⟨s, hs, h⟩) <;> exists s <;> tauto

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

Goal state before:
pp: n : PosNum
⊢ ↑n.size = (↑n).size

Tactic:
size_to_nat

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
m n : PosNum
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
by
  rw [← cast_to_nat, mul_to_nat, Nat.cast_mul, cast_to_nat, cast_to_nat]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : PosNum
⊢ ↑m < ↑n ↔ m < n

Tactic:
lt_to_nat

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : PosNum
⊢ m < n ↔ m < n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : Num
⊢ ↑n.size = (↑n).size

Tactic:
size_to_nat

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : Num
⊢ ↑m < ↑n ↔ m < n

Tactic:
lt_to_nat

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : Num
⊢ m < n ↔ m < n
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
⊢ Reaches f b c

Tactic:
rcases TransGen.head'_iff.1 h₁ with ⟨b', hab, hbc⟩

Goal state after:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun a b ↦ b ∈ f a) b' c
⊢ Reaches f b c
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b✝ x → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
intro g₂ gg cg

Goal state after:
case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ b✝ g₂
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Dir
a✝ : Stmt Γ Λ σ
⊢ move a✝¹ a✝ ∈ stmts₁ (move a✝¹ a✝)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

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

Goal state before:
pp: case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → Γ
a✝ : Stmt Γ Λ σ
⊢ write a✝¹ a✝ ∈ stmts₁ (write a✝¹ a✝)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

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

Goal state before:
pp: case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → σ
a✝ : Stmt Γ Λ σ
⊢ load a✝¹ a✝ ∈ stmts₁ (load a✝¹ a✝)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

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

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝² : Γ → σ → Bool
a✝¹ a✝ : Stmt Γ Λ σ
⊢ branch a✝² a✝¹ a✝ ∈ stmts₁ (branch a✝² a✝¹ a✝)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

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

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝ : Γ → σ → Λ
⊢ goto a✝ ∈ stmts₁ (goto a✝)

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

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

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
⊢ halt ∈ stmts₁ halt

Tactic:
simp only [stmts₁, Finset.mem_insert_self, Finset.mem_singleton_self]

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

Goal state before:
pp: Γ : 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
⊢ TM0.Supports (tr M) ↑(trStmts M S)

Tactic:
classical
  constructor
  · apply Finset.mem_product.2
    constructor
    · simp only [default, TM1.stmts, Finset.mem_insertNone, Option.mem_def, Option.some_inj,
        forall_eq', Finset.mem_biUnion]
      exact ⟨_, ss.1, TM1.stmts₁_self⟩
    · apply Finset.mem_univ
  · intro q a q' s h₁ h₂
    rcases q with ⟨_ | q, v⟩; · cases h₁
    obtain ⟨q', v'⟩ := q'
    simp only [trStmts, Finset.mem_coe] at h₂ ⊢
    rw [Finset.mem_product] at h₂ ⊢
    simp only [Finset.mem_univ, and_true] at h₂ ⊢
    cases q'; · exact Multiset.mem_cons_self _ _
    simp only [tr, Option.mem_def] at h₁
    have := TM1.stmts_supportsStmt ss h₂
    revert this; induction q generalizing v with intro hs
    | move d q =>
      cases h₁; refine TM1.stmts_trans ?_ h₂
      unfold TM1.stmts₁
      exact Finset.mem_insert_of_mem TM1.stmts₁_self
    | write b q =>
      cases h₁; refine TM1.stmts_trans ?_ h₂
      unfold TM1.stmts₁
      exact Finset.mem_insert_of_mem TM1.stmts₁_self
    | load b q IH =>
      refine IH _ (TM1.stmts_trans ?_ h₂) h₁ hs
      unfold TM1.stmts₁
      exact Finset.mem_insert_of_mem TM1.stmts₁_self
    | branch p q₁ q₂ IH₁ IH₂ =>
      cases h : p a v <;> rw [trAux, h] at h₁
      · refine IH₂ _ (TM1.stmts_trans ?_ h₂) h₁ hs.2
        unfold TM1.stmts₁
        exact Finset.mem_insert_of_mem (Finset.mem_union_right _ TM1.stmts₁_self)
      · refine IH₁ _ (TM1.stmts_trans ?_ h₂) h₁ hs.1
        unfold TM1.stmts₁
        exact Finset.mem_insert_of_mem (Finset.mem_union_left _ TM1.stmts₁_self)
    | goto l =>
      cases h₁
      exact Finset.some_mem_insertNone.2 (Finset.mem_biUnion.2 ⟨_, hs _ _, TM1.stmts₁_self⟩)
    | halt => cases h₁

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
    stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Tactic:
dsimp [readAux, stepAux]

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif (ListBlank.cons a (ListBlank.append l₂ R')).head then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R'))))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R'))))) =
    stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))