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

Goal state before:
pp: ⊢ GrowsPolynomially log

Tactic:
by
  intro b hb
  have hb₀ : 0 < b := hb.1
  refine ⟨1 / 2, by norm_num, ?_⟩
  refine ⟨1, by norm_num, ?_⟩
  have h_tendsto : Tendsto (fun x => 1 / 2 * Real.log x) atTop atTop :=
    Tendsto.const_mul_atTop (by norm_num) Real.tendsto_log_atTop
  filter_upwards [eventually_gt_atTop 1,
                  (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop
                    <| h_tendsto.eventually (eventually_gt_atTop (-Real.log b))] with x hx_pos hx
  intro u hu
  refine ⟨?lb, ?ub⟩
  case lb => calc
    1 / 2 * Real.log x = Real.log x + (-1 / 2) * Real.log x := by ring
      _ ≤ Real.log x + Real.log b := by grind
      _ = Real.log (b * x) := by rw [← Real.log_mul (by positivity) (by positivity), mul_comm]
      _ ≤ Real.log u := by gcongr; exact hu.1
  case ub =>
    rw [one_mul]
    gcongr
    · calc 0 < b * x := by positivity
         _ ≤ u := by exact hu.1
    · exact hu.2

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n✝)).bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n✝)).bind fun i ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

Tactic:
]

Goal state after:
case succ.prec.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n✝)).bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n✝)).bind fun i ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (true ^^ true) = false

Tactic:
]

Goal state after:
case inr.inr.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (true ^^ true) = false
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((evaln k cf n).bind fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
]

Goal state after:
case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((evaln k cf n).bind fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)) =
    match Fin.ofNat 4 (n + ↑(Fin.ofNat 4 1)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
]

Goal state after:
case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)) =
    match Fin.ofNat 4 (n + ↑(Fin.ofNat 4 1)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ (match Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match Fin.ofNat 4 n + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
]

Goal state after:
case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ (match Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match Fin.ofNat 4 n + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.rfind'.some.succ
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
n✝ : ℕ
⊢ evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) =
    evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
]

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

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 = 0
⊢ n % 2 = 0

Tactic:
]

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 = 0
⊢ n % 2 = 0
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 = 0
⊢ ↑0 % 2 = 0

Tactic:
]

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 = 0
⊢ ↑0 % 2 = 0
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 + 1 ^^^
      match 1 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) =
    match 1 + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
]

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 + 1 ^^^
      match 1 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) =
    match 1 + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
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
⊢ (↑1 % 2 + 1 % 2) % 2 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑p + ↑p = ↑p + ↑p

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑p + ↑p + 1 = ↑p + ↑p + 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑n = ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: α : Type u_1
Γ : Type u_2
e : Encoding α Γ
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ e.decode (e.encode x✝) = e.decode (e.encode x✝)

Tactic:
]

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1

Tactic:
]

Goal state after:
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n

Tactic:
]

Goal state after:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n

Tactic:
]

Goal state after:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: b : PosNum
⊢ 1 + ↑b = 1 + ↑b

Tactic:
]

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

Goal state before:
pp: a : PosNum
⊢ ↑a + 1 = ↑a + 1

Tactic:
]

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

Goal state before:
pp: a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)

Tactic:
]

Goal state after:
a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ p.bit1.bit0 = p.bit1.bit0

Tactic:
]

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

Goal state before:
pp: case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)

Tactic:
]

Goal state after:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ n.bit1 = n.bit1

Tactic:
]

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

Goal state before:
pp: m p : PosNum
⊢ ↑m * ↑p + ↑m * ↑p = ↑m * ↑p + ↑m * ↑p

Tactic:
]

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

Goal state before:
pp: m p : PosNum
⊢ ↑m * ↑p + ↑m * ↑p + ↑m = ↑m * ↑p + ↑m * ↑p + ↑m

Tactic:
]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ ⋃ s ∈ S, M.evalFrom {s} x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ ⋃ s ∈ S, M.evalFrom {s} x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n

Tactic:
]

Goal state after:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ [] = []

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ n, l = replicate n none

Tactic:
]

Goal state after:
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ n, l = replicate n none
Module: Mathlib.Data.List.ReduceOption

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

Tactic:
]

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
h : ∃ l₁ a_1 l₂, l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none
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₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
]

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: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S ∪ M.acceptsFrom T
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none

Tactic:
]

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
]

Goal state after:
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
]

Goal state after:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
hl₂ : ∃ m n, w✝ = replicate m none ++ some a :: replicate n none
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
]

Goal state after:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
hl₂ : ∃ m n, w✝ = replicate m none ++ some a :: replicate n none
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ b.bit0 = b.bit0

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ l' ++ [a] = l' ++ [a]

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length

Tactic:
]

Goal state after:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → a.isSome = true) ↔ ∀ (x : Option α), x ∈ l → x.isSome = true

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l

Tactic:
]

Goal state after:
α : Type u_1
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1

Tactic:
]

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ some x ∈ l ↔ some x ∈ l

Tactic:
]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s t : σ
x✝ : List α
a : α
x : List α
h : ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x✝ : List α
a : α
x : List α
h : ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a

Tactic:
]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x

Tactic:
]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x