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

Goal state before:
pp: case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m ≤ n,
        encode
            (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
              (ofNat (List ℕ) m)) =
          encode (decode m)) →
      encode
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (n + 1))) =
        encode (decode (n + 1))

Tactic:
intro n IH

Goal state after:
case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) (n + 1))) =
    encode (decode (n + 1))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case hi.some.some.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH✝ :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
val✝¹ : List ℕ
val✝ : List α
IH : encode (some val✝¹) = encode (some val✝)
⊢ encode (Option.map (List.cons (encode a)) (some val✝¹)) = encode (Option.map (List.cons a) (some val✝))

Tactic:
· exact congr_arg (fun k => (Nat.pair (encode a) k).succ.succ) (Nat.succ.inj IH)

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ PrimrecPred fun p ↦ (fun a ↦ decide (encode a = p.1)) p.2 = true

Tactic:
by simpa using Primrec.eq.comp (Primrec.encode.comp .snd) .fst

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a ↦ Part.map encode (↑g a)
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ f (g a)) a)

Tactic:
simp only [PFun.coe_val, map_some, bind_eq_bind]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (((↑(decode n)).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑(decode n)).bind fun a ↦ Part.map encode (f (g a))
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
| fun G' ↦ G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x x' ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
G',

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
G' : SimpleGraph V
| G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x x' ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
n : ℕ
IH : Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) (n + 1) = (n + 1).sqrt

Tactic:
dsimp; rw [IH]; split_ifs with h
    · exact le_antisymm (Nat.sqrt_le_sqrt (Nat.le_succ _)) (Nat.lt_succ_iff.1 <| Nat.sqrt_lt.2 h)
    · exact Nat.eq_sqrt.2
        ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * (2 ^ (n + 3) - 3) + 3 = 2 ^ (n + 3) * 2 - 3

Tactic:
mul_comm _ 2,

Goal state after:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * (2 ^ (n + 3) - 3) + 3 = 2 * 2 ^ (n + 3) - 3
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Tactic:
let m := n.div2.div2
    have hm : m < n + 4 := by
      simp only [m, div2_val]
      exact
        lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
          (Nat.succ_le_succ (Nat.le_add_right _ _))
    have _m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm
    have _m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm
    have IH := encode_ofNatCode m
    have IH1 := encode_ofNatCode m.unpair.1
    have IH2 := encode_ofNatCode m.unpair.2
    conv_rhs => rw [← Nat.bit_bodd_div2 n, ← Nat.bit_bodd_div2 n.div2]
    simp only [ofNatCode.eq_5]
    cases n.bodd <;> cases n.div2.bodd <;>
      simp [m, encodeCode, IH, IH1, IH2, Nat.bit_val]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ (ack (m + 1) 0 + 1) ^ 2 ≤ ack (m + 1 + 3) 0

Tactic:
by
    rw [ack_succ_zero, ack_succ_zero]
    apply ack_add_one_sq_lt_ack_add_three

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case case3
m n : ℕ
hmn₁ : (pappAck (m + 1)).eval n = Part.some (ack (m + 1) n)
hmn₂ : (pappAck m).eval (ack (m + 1) n) = Part.some (ack m (ack (m + 1) n))
⊢ (pappAck m.succ).eval n.succ = Part.some (ack m.succ n.succ)

Tactic:
dsimp only [pappAck] at *

Goal state after:
case case3
m n : ℕ
hmn₁ : (pappAck.step (pappAck m)).eval n = Part.some (ack (m + 1) n)
hmn₂ : (pappAck m).eval (ack (m + 1) n) = Part.some (ack m (ack (m + 1) n))
⊢ (pappAck.step (pappAck m)).eval n.succ = Part.some (ack m.succ n.succ)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case h₂
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2
i : α
⊢ ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2

Tactic:
exact hn i

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

Goal state before:
pp: ⊢ deriv ε =o[atTop] fun x ↦ x⁻¹

Tactic:
exact isLittleO_deriv_smoothingFn

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

Goal state before:
pp: ⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 + ε ↑n

Tactic:
filter_upwards [eventually_one_add_smoothingFn_pos] with n hn

Goal state after:
n : ℕ
hn : 0 < 1 + ε ↑n
⊢ 0 ≤ 1 + ε ↑n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a : ℕ
⊢ (cf.prec cg).eval (Nat.pair a 0) = cf.eval a

Tactic:
rw [eval, Nat.unpaired, Nat.unpair_pair]
  rw [Nat.rec_zero]

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

Goal state before:
pp: 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₂ * f x + c₄ * g x ≥ f u + g u

Tactic:
by gcongr
                          · exact (hf u hu).2
                          · exact (hg u hu).2

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
⊢ ⌈rexp 1⌉₊ ≤ 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:
h_exp

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
⊢ ∀ 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
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 = 1
⊢ (n % 2 + 1 % 2) % 2 = 0

Tactic:
← @mod_mod_of_dvd _ 4 n <| by simp,

Goal state after:
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 = 1
⊢ (n % 4 % 2 + 1 % 2) % 2 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ (p + p).succ.bit0 = p.bit1.bit0

Tactic:
rw [bit0_of_bit0 p, succ]

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

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

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

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

Goal state before:
pp: x✝ : Num
⊢ x✝ * 1 = x✝

Tactic:
by rw [← to_nat_inj, mul_to_nat, cast_one, mul_one]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mp
α : 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₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : s₂ ∈ M.εClosure (M.step t (some a))
x' : List (Option α)
left✝ : x'.reduceOption = x
right✝ : M.IsPath s₁ t x'
⊢ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
rw [mem_εClosure_iff_exists] at h

Goal state after:
case append_singleton.mp
α : 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₂ t : σ
ht : t ∈ M.evalFrom {s₁} x
h : ∃ t_1 ∈ M.step t (some a), s₂ ∈ M.εClosure {t_1}
x' : List (Option α)
left✝ : x'.reduceOption = x
right✝ : M.IsPath s₁ t x'
⊢ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
intro _ _

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

Goal state before:
pp: cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
⊢ ∃ h,
    Nat.Partrec h ∧
      ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ cg.eval a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (cg.eval a).Dom)

Tactic:
have : Nat.Partrec fun n => Nat.rfindOpt fun k => cf.evaln k n <|> cg.evaln k n :=
    Partrec.nat_iff.1
      (Partrec.rfindOpt <|
        Primrec.option_orElse.to_comp.comp
          (Code.primrec_evaln.to_comp.comp <| (snd.pair (const cf)).pair fst)
          (Code.primrec_evaln.to_comp.comp <| (snd.pair (const cg)).pair fst))

Goal state after:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
⊢ ∃ h,
    Nat.Partrec h ∧
      ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ cg.eval a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (cg.eval a).Dom)
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a

Tactic:
refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_

Goal state after:
case refine_2.refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f b

case refine_2.refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b ↦ b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ b ∈ eval f a✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
⊢ stmts₁ q₁ ⊆ stmts₁ q₂

Tactic:
q₀

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
⊢ q₀ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₂
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₁ : p ≤₀ q
h₂ : ComputablePred q
⊢ ComputablePred p

Tactic:
rcases h₁ with ⟨f, c, hf⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch.false
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif false then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

pp: case branch.true
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif true then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

Tactic:
· exact IH₂ _ _ hs.2

Goal state after:
case branch.true
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif true then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.move
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
a✝¹ : Dir
a✝ : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.move a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (TM1.stepAux (TM1.Stmt.move a✝¹ a✝) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.move a✝¹ a✝) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.move a✝¹ a✝) v T).Tape }

Tactic:
| move _ _ IH =>

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
⊢ stmts₁ q₁ ⊆ stmts₁ q₂

Tactic:
q₀

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
⊢ q₀ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₂
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mp.cons
α : 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)
⊢ (P.deriv a * P.star).rmatch x = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
mul_rmatch_iff

Goal state after:
case mp.cons
α : 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)
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true) →
    ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch.false
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif false then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

pp: case branch.true
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif true then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

Tactic:
· exact IH₂ _ _ hs.2

Goal state after:
case branch.true
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif true then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S