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
⊢ ∑ i, a i * T (r i n) + g ↑n ≤ ∑ i, a i * (C * ((1 - ε ↑(r i n)) * asympBound g a b (r i n))) + g ↑n

Tactic:
gcongr (∑ i, a i * ?_) + g n with i _

Goal state after:
case ha
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := ⋯
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
i : α
a✝ : i ∈ univ
⊢ 0 ≤ a i

case hbc
α : 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
i : α
a✝ : i ∈ univ
⊢ T (r i n) ≤ C * ((1 - ε ↑(r i n)) * asympBound g a b (r i n))
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
⊢ n₁ = n₂

Tactic:
injection h₂ with h₃ h₄

Goal state after:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : 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 : p a b + 1 < 0
⊢ c₂ * (↑n ^ (p a b + 1) / ↑n ^ (p a b + 1)) * g ↑n = c₂ * g ↑n

Tactic:
rw [div_self (by positivity), mul_one]

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

Goal state before:
pp: α : 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
⊢ c₂ * (1 - c₃) * g ↑n * (↑n ^ (p a b + 1) / ↑n ^ (p a b + 1)) = c₂ * (1 - c₃) * g ↑n

Tactic:
rw [div_self (by positivity), mul_one]

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.1.length).1
n : Primrec Prod.snd
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
⊢ Primrec fun p ↦
    (fun p k' ↦
        Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2)
          (fun cf cg x x_1 ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
            let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            some (Nat.pair x y))
          (fun cf cg x x_1 ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
          (fun cf cg x x_1 ↦
            have z := (unpair p.2).1;
            Nat.casesOn (unpair p.2).2 (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y ↦ do
              let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
          fun cf x ↦
          have z := (unpair p.2).1;
          have m := (unpair p.2).2;
          do
          let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
          Nat.casesOn x (some m) fun x ↦ lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)))
      p.1 p.2

Tactic:
have n := n.comp (Primrec.fst (β := ℕ))

Goal state after:
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
⊢ Primrec fun p ↦
    (fun p k' ↦
        Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2)
          (fun cf cg x x_1 ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
            let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            some (Nat.pair x y))
          (fun cf cg x x_1 ↦ do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
            lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
          (fun cf cg x x_1 ↦
            have z := (unpair p.2).1;
            Nat.casesOn (unpair p.2).2 (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y ↦ do
              let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
          fun cf x ↦
          have z := (unpair p.2).1;
          have m := (unpair p.2).2;
          do
          let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
          Nat.casesOn x (some m) fun x ↦ lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)))
      p.1 p.2
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
H : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
| inl H =>

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

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
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
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
this : 1 + ε ↑n < 2
⊢ 0 ≤ (C - c₁ * (1 + ε ↑n)) * g ↑n

Tactic:
exact mul_nonneg (by grw [sub_nonneg, this, mul_comm, hC]) g_pos

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 : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ (1 + ε ↑n) * asympBound g a b n + (C - c₁ * (1 + ε ↑n)) * g ↑n ≥ (1 + ε ↑n) * asympBound g a b n + 0

Tactic:
gcongr
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was:
      `exact mul_nonneg (by grind +splitIndPred) g_pos` -/
      have : 1 + ε ↑n < 2 := by grind
      exact mul_nonneg (by grw [sub_nonneg, this, mul_comm, hC]) g_pos

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
i : ℕ
⊢ n.testBit i = false

Tactic:
by rw [← h (i + 1), testBit_bit_succ]

Goal state after:
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
⊢ ∃ 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:
cases le_or_gt 0 p with
  | inl => -- 0 ≤ p
    refine ⟨c₁^p, hc₁p, ?_⟩
    refine ⟨c₂^p, hc₂p, ?_⟩
    filter_upwards [eventually_gt_atTop 0, hfnew, hf_nonneg,
        (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf_nonneg]
        with x _ hf₁ hf_nonneg hf_nonneg₂
    intro u hu
    have fu_nonneg : 0 ≤ f u := hf_nonneg₂ u hu.1
    refine ⟨?lb, ?ub⟩
    case lb => calc
      c₁ ^ p * (f x) ^ p = (c₁ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
        _ ≤ _ := by gcongr; exact (hf₁ u hu).1
    case ub => calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]
  | inr hp => -- p < 0
    match hf.eventually_atTop_zero_or_pos_or_neg with
    | .inl hzero => -- eventually zero
      refine ⟨1, by norm_num, 1, by norm_num, ?_⟩
      filter_upwards [hzero, hfnew] with x hx hx'
      intro u hu
      simp only [hx, zero_rpow (ne_of_lt hp), mul_zero,
        Set.Icc_self, Set.mem_singleton_iff]
      simp only [hx, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx'
      rw [hx' u hu, zero_rpow (ne_of_lt hp)]
    | .inr (.inl hpos) => -- eventually positive
      refine ⟨c₂^p, hc₂p, ?_⟩
      refine ⟨c₁^p, hc₁p, ?_⟩
      filter_upwards [eventually_gt_atTop 0, hfnew, hpos,
          (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hpos]
          with x _ hf₁ hf_pos hf_pos₂
      intro u hu
      refine ⟨?lb, ?ub⟩
      case lb => calc
        c₂ ^ p * (f x) ^ p = (c₂ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₂_mem) (le_of_lt hf_pos)]
          _ ≤ _ := rpow_le_rpow_of_nonpos (hf_pos₂ u hu.1) (hf₁ u hu).2 (le_of_lt hp)
      case ub => calc
        (f u) ^ p ≤ (c₁ * f x) ^ p := by
              exact rpow_le_rpow_of_nonpos (by positivity) (hf₁ u hu).1 (le_of_lt hp)
          _ = _ := by rw [← mul_rpow (le_of_lt hc₁_mem) (le_of_lt hf_pos)]
    | .inr (.inr hneg) => -- eventually negative (which is impossible)
      have : ∀ᶠ (_ : ℝ) in atTop, False := by
        filter_upwards [hf_nonneg, hneg] with x hx hx'; linarith
      rw [Filter.eventually_false_iff_eq_bot] at this
      exact False.elim <| atTop_neBot.ne this

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:
by
    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.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
⊢ a :: x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ a :: x ∈ M.acceptsFrom S ∧ p

Tactic:
have h : M.stepSet {s ∈ S | p} a = {s ∈ M.stepSet S a | p} := by
      ext s; simp only [stepSet, mem_ofPred_eq, mem_iUnion, exists_prop]; tauto
    simp [h, ih]

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

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

Tactic:
rw [size, succ_to_nat, size_to_nat n, cast_bit1, ← two_mul, ← Nat.bit_true_apply,
        Nat.size_bit]

Goal state after:
n : PosNum
⊢ Nat.bit true ↑n ≠ 0
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start : Set σ
this : M.toεNFA.stepSet = M.stepSet
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
by rw [this]

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Partrec' fun v ↦ f v.head

Tactic:
obtain ⟨c, rfl⟩ := exists_code.1 hf
    simpa [eval_eq_rfindOpt] using
      rfindOpt <|
        of_prim <|
          Primrec.encode_iff.2 <|
            primrec_evaln.comp <|
              (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <|
                Primrec.vector_head.comp Primrec.vector_tail

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✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := l₁, var := v, Tape := T })
    (TM1.step M { l := l₁, var := v, Tape := T })

Tactic:
rcases l₁ with - | l₁

Goal state after:
case none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := none, var := v, Tape := T })
    (TM1.step M { l := none, var := v, Tape := T })

case some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
l₁ : Λ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := some l₁, var := v, Tape := T })
    (TM1.step M { l := some l₁, var := v, Tape := T })
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
deriv,

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (if a = head✝ then 1 else 0).rmatch [] = true ↔ [head✝] = [a]
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
deriv,

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ ((if a = head✝ then 1 else 0).deriv head).rmatch tail = true ↔ head✝ :: head :: tail = [a]
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
let : DecidableEq Γ := e.decidableEq

Goal state after:
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
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.star.deriv a).rmatch x = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
deriv,

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)
⊢ (P.deriv a * P.star).rmatch x = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
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)
hsum : a :: x = S.flatten
⊢ (P.star.deriv a).rmatch x = true

Tactic:
deriv,

Goal state after:
case mpr.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
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)
hsum : a :: x = S.flatten
⊢ (P.deriv a * P.star).rmatch x = true
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 → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
l₁ : Option Λ
v : σ
L R : ListBlank Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := l₁, var := v, Tape := Tape.mk' L R })
    (step M { l := l₁, var := v, Tape := Tape.mk' L R })

Tactic:
rcases l₁ with - | l₁

Goal state after:
case none
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := none, var := v, Tape := Tape.mk' L R })
    (step M { l := none, var := v, Tape := Tape.mk' L R })

case some
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := some l₁, var := v, Tape := Tape.mk' L R })
    (step M { l := some l₁, var := v, Tape := Tape.mk' L R })
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
by
      intro X Y Z f
      infer_instance

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ TM1.stepAux (branch (fun a x ↦ a.1) (trNormal q) (move Dir.left (goto fun x x_1 ↦ ret q))) v
      ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
TM1.stepAux,

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L))).head.1 then
      TM1.stepAux (trNormal q) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (move Dir.left (goto fun x x_1 ↦ ret q)) v
        ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }