mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) 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
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, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ 1 ≤ 2 * (c₁⁻¹ * c₁) * (1 / 2)

Tactic:
by
          rw [inv_mul_cancel₀ (by positivity : c₁ ≠ 0)]; norm_num

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg
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₂
cf : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
n x✝ : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) cf (Nat.pair a m)
              if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x✝
h :
  ∃ a,
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x✝
x : ℕ
x0 : ¬x = 0
⊢ evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x✝ →
    evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x✝

Tactic:
exact evaln_mono hl'

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
⊢ f x - ‖g x‖ ≥ f x + 1 / 2 * f x

Tactic:
by
                  rw [sub_eq_add_neg]
                  gcongr
                  refine le_of_neg_le_neg ?bc.a
                  rwa [neg_neg, ← neg_mul, ← neg_div]

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ 3 / 2 * f u ≥ 3 / 2 * (c₁ * f x)

Tactic:
by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1

Goal state after:
Module: Mathlib.Computability.Language

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

Tactic:
one_add_self_mul_kstar_eq_kstar

Goal state after:
α : Type u_1
l : Language α
⊢ l∗ = l∗
Module: Mathlib.Computability.Language

Goal state before:
pp: case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ l ≤ m∗ * n

Tactic:
intro x

Goal state after:
case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
⊢ x ∈ l → x ∈ m∗ * n
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
⊢ m∗ * n = (1 + m * m∗) * n

Tactic:
one_add_self_mul_kstar_eq_kstar

Goal state after:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
⊢ m∗ * n = m∗ * n
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : y ∈ {a} * {b}∗ * {c}
⊢ y ∈ M.accepts

Tactic:
rw [Language.mem_mul] at hy

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : ∃ a_1 ∈ {a} * {b}∗, ∃ b ∈ {c}, a_1 ++ b = y
⊢ y ∈ M.accepts
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hrf
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
have cf := Primrec.fst.comp (Primrec.snd (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Option ℕ))

Goal state after:
case hrf
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case ub
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹

Tactic:
case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ ((List.range k)[n]?.bind fun a ↦ evaln k c a) = evaln k c n

Tactic:
rw [List.getElem?_eq_none]

Goal state after:
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.none.bind fun a ↦ evaln k c a) = evaln k c n

case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (List.range k).length ≤ n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inl
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)

Tactic:
refine ⟨c₁^p, hc₁p, ?_⟩

Goal state after:
case inl
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ ∃ c₂_1 > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₂ ^ p * (fun x ↦ f x ^ p) x) (c₂_1 * (fun x ↦ f x ^ p) x)

Tactic:
refine ⟨c₁^p, hc₁p, ?_⟩

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₂ ^ p * (fun x ↦ f x ^ p) x) (c₁ ^ p * (fun x ↦ f x ^ p) x)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
⊢ j ≠ 0

Tactic:
intro x

Goal state after:
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: a : Code × ℕ
⊢ (rfindOpt fun b ↦
      evaln (((a, b).2, (a, b).1.1), (a, b).1.2).1.1 (((a, b).2, (a, b).1.1), (a, b).1.2).1.2
        (((a, b).2, (a, b).1.1), (a, b).1.2).2) =
    a.1.eval a.2

Tactic:
by simp [eval_eq_rfindOpt]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
intro ⟨t, hx, _⟩
    induction x generalizing s <;> cases hx <;> tauto

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

Goal state before:
pp: m n : Num
⊢ (m.cmp n).swap = n.cmp m

Tactic:
by
  cases m <;> cases n <;> try { rfl }; apply PosNum.cmp_swap

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: 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
n : ℕ
⊢ ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
intro x

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
n x : ℕ
⊢ (x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n) → x ∈ cf.eval n ∨ x ∈ cg.eval n
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n →. ℕ
pf : Partrec' f
⊢ Partrec f

Tactic:
induction pf with

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : 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 ∈ k' a, x ∈ f a ∨ x ∈ g a

Tactic:
intro x

Goal state after:
α : 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 : σ
⊢ x ∈ k' a → x ∈ f a ∨ x ∈ g a
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' fun v ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : ℕ → Part ℕ := fun n₁ ↦ (↑(decode n₁)).bind fun a ↦ Part.map encode (f a)
i : List.Vector ℕ n
⊢ ((↑(decode (encode i))).bind fun a ↦ Part.map encode (f a)) = f i

Tactic:
simp [encodek, Part.map_id']

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
⊢ BlankExtends l (head (Quotient.mk'' l) :: l.tail)

Tactic:
cases l

Goal state after:
case nil
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ BlankExtends [] (head (Quotient.mk'' []) :: [].tail)

case cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: (head✝ :: tail✝).tail)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
⊢ (List.map f.f l).headI = f.f l.headI

Tactic:
cases l

Goal state after:
case nil
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
⊢ (List.map f.f []).headI = f.f [].headI

case cons
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
tail✝ : List Γ
⊢ (List.map f.f (head✝ :: tail✝)).headI = f.f (head✝ :: tail✝).headI
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ Supports M Set.univ

Tactic:
constructor <;> intros <;> apply Set.mem_univ

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]
      simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]
      cases a <;> rfl

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

Goal state before:
pp: m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : List.Vector ℕ m), cl.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i.succ v
v : List.Vector ℕ m
⊢ (cg.cons cl).eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v

Tactic:
simp [Vector.mOfFn, hg₁, hl]

Goal state after:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : List.Vector ℕ m), cl.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i.succ v
v : List.Vector ℕ m
⊢ (do
      let a ← g 0 v
      let a_1 ← Vector.mOfFn fun i ↦ g i.succ v
      Part.some (a :: ↑a_1)) =
    do
    let a ← g 0 v
    let a_1 ← Vector.mOfFn fun i ↦ g i.succ v
    Subtype.val <$> Part.some (a ::ᵥ a_1)
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
e : (a : α) → X a ⟶ B
⊢ Continuous fun x ↦
    match x with
    | ⟨a, x⟩ => (ConcreteCategory.hom (e a)) x

Tactic:
apply continuous_sigma
      intro a; exact (e a).hom.hom.continuous

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ Function.Injective ⇑(ConcreteCategory.hom (ι X a))

Tactic:
intro x

Goal state after:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x : ↑(X a).toTop
⊢ ∀ ⦃a₂ : (fun X ↦ ↑X.toTop) (X a)⦄, (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) a₂ → x = a₂
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
⊢ ∀ (a : X) (u : Set X), a ∈ u → IsOpen[inst✝³] u → ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, a ∈ v ∧ v ⊆ u

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
⊢ ∀ (u : Set X), x ∈ u → IsOpen[inst✝³] u → ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, x ∈ v ∧ v ⊆ u
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: α : Type u_1
p : α → Bool
a : α
L l₁ : List α
o : Option α
l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) o
⊢ splitAtPred p (a :: L) = (l₁, o, l₂)

Tactic:
rw [splitAtPred]

Goal state after:
α : Type u_1
p : α → Bool
a : α
L l₁ : List α
o : Option α
l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) o
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (l₁, o, l₂)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [Code.eval, IHf]

Goal state after:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let v ←
      (fun v ↦ do
            let n ← f.eval v
            let ns ← fs.eval v
            pure (n.headI :: ns))
          v
    eval step (Cfg.ret k v)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
⊢ IsTotallySeparated univ

Tactic:
intro x

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
⊢ x ∈ univ →
    ∀ ⦃y : X⦄,
      y ∈ univ → x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
⊢ Surjective f

Tactic:
intro x

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
⊢ ∃ a, f a = x
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case refine_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
⊢ U ⊆ φ ⁻¹' Z₂

Tactic:
intro x

Goal state after:
case refine_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
⊢ x ∈ U → x ∈ φ ⁻¹' Z₂