mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
w✝ : α
hz : w✝ ∈ W
haz : w✝ ≠ a
hbz : w✝ ≠ b
hf : ¬G.Adj w✝ x
⊢ ¬G.Adj x w✝

Tactic:
by rwa [adj_comm] at hf

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case nil
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ : V
ht : Walk.nil.IsTrail
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) Walk.nil.edges) ↔ u✝ ≠ u✝ → x ≠ u✝ ∧ x ≠ u✝

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard + (1 + 1) ≤ ENat.card V

Tactic:
refine add_le_of_le_tsub_right_of_le (Order.add_one_le_of_lt ENat.one_lt_card) ?_

Goal state after:
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard ≤ ENat.card V - (1 + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
⊢ v ∈ M1.verts ∪ M2.verts

Tactic:
by_cases h : v ∈ M1.verts

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h✝ : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∈ M1.verts
⊢ v ∈ M1.verts ∪ M2.verts

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h✝ : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
⊢ v ∈ M1.verts ∪ M2.verts
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Tactic:
exact (psub_eq_none.2 (not_le.1 h)).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
⊢ (G a)^[n] (g a, f a) = (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))

Tactic:
generalize f a = l

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
l : List β
⊢ (G a)^[n] (g a, l) = (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take n l), List.drop n l)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n)
this : Primcodable (List β) := prim H
l : List β
⊢ ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r l = l.reverseAux r

Tactic:
induction l <;> simp [*, List.reverseAux]

Goal state after:
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) := 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 : ℕ
⊢ (∀ 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:
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
α : 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 : α
o : Option (List ℕ)
p : Option (List α)
⊢ encode o = encode p → encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)

Tactic:
IH

Goal state after:
case hi.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 : α
o : Option (List ℕ)
p : Option (List α)
IH : encode o = encode p
⊢ encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: m n : ℕ
⊢ (m, n).1 - (m, n).2 * (fun x1 x2 ↦ x1 / x2) (m, n).1 (m, n).2 = m % n

Tactic:
apply Nat.sub_eq_of_eq_add
    simp [add_comm (m % n), Nat.div_add_mod]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
n : ℕ
⊢ [][n]? = Sum.rec (fun val ↦ none) (fun val ↦ some val) (F [] n)

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
⊢ ((y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }) →
    (∀ n < m, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }

Tactic:
IH

Goal state after:
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
⊢ (∀ n < m, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i✝ : Fin m.succ
i : Fin m
⊢ Primrec' fun v ↦ ((fun v ↦ f v ::ᵥ g v) v).get i.succ

Tactic:
simp [hg i]

Goal state after:
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
⊢ (if
        n + 1 <
          (Nat.rec 0 (fun x y ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) *
            (Nat.rec 0 (fun x y ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) then
      Nat.rec 0 (fun x y ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n
    else Nat.rec 0 (fun x y ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) n + 1) =
    (n + 1).sqrt

Tactic:
IH

Goal state after:
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
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
⊢ (∀ (a'' : α),
      Sum.inr a'' ∈ f a₂ →
        ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m) →
    ∀ (k : ℕ), Sum.inr a₂ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
IH

Goal state after:
case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∀ (k : ℕ), Sum.inr a₂ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), n.succ < ack m n

Tactic:
refine ⟨1, fun n => ?_⟩

Goal state after:
case succ
f : ℕ → ℕ
n : ℕ
⊢ n.succ < ack 1 n
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: c : Code
⊢ (pappAck.step c).eval 0 = c.eval 1

Tactic:
simp [pappAck.step, Code.eval]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: c : Code
n : ℕ
⊢ (pappAck.step c).eval (n + 1) = ((pappAck.step c).eval n).bind c.eval

Tactic:
simp [pappAck.step, Code.eval]

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
by
  obtain ⟨c₁, _, c₂, _, h⟩ := hf (1 / 2) (by norm_num)
  match lt_trichotomy c₁ c₂ with
  | .inl hlt => -- c₁ < c₂
    left
    filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
    have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
    have hu := hx (3 / 4 * x) h'
    have hu := Set.nonempty_of_mem hu
    rw [Set.nonempty_Icc] at hu
    have hu' : 0 ≤ (c₂ - c₁) * f x := by linarith
    exact nonneg_of_mul_nonneg_right hu' (by linarith)
  | .inr (.inr hgt) => -- c₂ < c₁
    right
    filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
    have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
    have hu := hx (3 / 4 * x) h'
    have hu := Set.nonempty_of_mem hu
    rw [Set.nonempty_Icc] at hu
    have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith
    exact nonpos_of_mul_nonpos_right hu' (by linarith)
  | .inr (.inl heq) => -- c₁ = c₂
    have hmain : ∃ c, ∀ᶠ x in atTop, f x = c := by
      simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h
      rw [eventually_atTop] at h
      obtain ⟨n₀, hn₀⟩ := h
      refine ⟨f (max n₀ 2), ?_⟩
      rw [eventually_atTop]
      refine ⟨max n₀ 2, ?_⟩
      refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
      case base => grind
      case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
    obtain ⟨c, hc⟩ := hmain
    cases le_or_gt 0 c with
    | inl hpos =>
      exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
    | inr hneg =>
      right
      filter_upwards [hc] with x hc
      exact le_of_lt <| by simpa only [hc]

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

Goal state before:
pp: case neg.inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∧ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x

Tactic:
exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : m = 0
h₂ : (unpair n).2 = x
⊢ 0 + (unpair n).2 = x

Tactic:
simp [h₂]

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case nil
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
⊢ r.Rewrites ([] ++ [Symbol.nonterminal r.input] ++ q) ([] ++ r.output ++ q)

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
hS : ∀ y ∈ [], y ∈ {x}
⊢ M.evalFrom s [].flatten = s

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
⊢ (comap f M).evalFrom s [] = M.evalFrom s (List.map f [])

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
⊢ ((reindex g) M).evalFrom s [] = g (M.evalFrom (g.symm s) [])

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.union M2).evalFrom (s1, s2) [] ∈ (M1.union M2).accept ↔
    M1.evalFrom s1 [] ∈ M1.accept ∨ M2.evalFrom s2 [] ∈ M2.accept

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case nil
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.inter M2).evalFrom (s1, s2) [] ∈ (M1.inter M2).accept ↔
    M1.evalFrom s1 [] ∈ M1.accept ∧ M2.evalFrom s2 [] ∈ M2.accept

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.evalFrom (S ∪ T) [] = M.evalFrom S [] ∪ M.evalFrom T []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
⊢ M.evalFrom (⋃ i, s i) [] = ⋃ i, M.evalFrom (s i) []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map (Option.map f) []).reduceOption = map f [].reduceOption

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
⊢ [].reduceOption.length = (filter Option.isSome []).length

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
⊢ [] ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ [] ∈ M.acceptsFrom S ∧ p

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
x : Option α
⊢ ([].concat x).reduceOption = [].reduceOption ++ x.toList

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : DFA α σ
start : σ
⊢ List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' [])
⊢ Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S [])

Tactic:
| nil =>

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, _⟩

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
t : σ
hx : M.IsPath s t x
right✝ : M.IsPath t u y
⊢ M.IsPath s u (x ++ y)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b c : Num
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
transfer_rw

Goal state after:
a b c : Num
⊢ ↑a ≤ ↑b → ↑b ≤ ↑c → ↑a ≤ ↑c
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : Num
⊢ a ≤ b → b ≤ a → a = b

Tactic:
transfer_rw

Goal state after:
a b : Num
⊢ ↑a ≤ ↑b → ↑b ≤ ↑a → ↑a = ↑b
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ s₂ ∈ M.evalFrom {s₁} [] ↔ ∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
| nil =>

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

Goal state before:
pp: a b c : Num
⊢ a ≤ b → a + c ≤ b + c

Tactic:
transfer_rw

Goal state after:
a b c : Num
⊢ ↑a ≤ ↑b → ↑a + ↑c ≤ ↑b + ↑c
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b c : Num
⊢ a + b ≤ a + c → b ≤ c

Tactic:
transfer_rw

Goal state after:
a b c : Num
⊢ ↑a + ↑b ≤ ↑a + ↑c → ↑b ≤ ↑c
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : Num
⊢ a ≤ b ∨ b ≤ a

Tactic:
transfer_rw

Goal state after:
a b : Num
⊢ ↑a ≤ ↑b ∨ ↑b ≤ ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b c : Num
⊢ 0 < a → b < c → a * b < a * c

Tactic:
transfer_rw

Goal state after:
a b c : Num
⊢ 0 < ↑a → ↑b < ↑c → ↑a * ↑b < ↑a * ↑c
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b c : Num
⊢ 0 < a → b < c → b * a < c * a

Tactic:
transfer_rw

Goal state after:
a b c : Num
⊢ 0 < ↑a → ↑b < ↑c → ↑b * ↑a < ↑c * ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b c : PosNum
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b c : PosNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑c → ↑a ≤ ↑c
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b : PosNum
⊢ ↑a < ↑b ↔ ↑a ≤ ↑b ∧ ¬↑b ≤ ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ a ≤ b → b ≤ a → a = b

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b : PosNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑a → ↑a = ↑b
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ a ≤ b ∨ b ≤ a

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b : PosNum
⊢ ↑a ≤ ↑b ∨ ↑b ≤ ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑n.bit0 = 2 * ↑n

Tactic:
by
  rw [← bit0_of_bit0, two_mul, cast_add]

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: case nil
α : Type u
L : Language α
⊢ ↑(L.toDFA.eval []) = L.leftQuotient []

Tactic:
| nil =>

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ l.nth 0 = l.head

Tactic:
← ListBlank.cons_head_tail l

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ (cons l.head l.tail).nth 0 = (cons l.head l.tail).head
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ l.nth (n + 1) = l.tail.nth n

Tactic:
← ListBlank.cons_head_tail l

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ (cons l.head l.tail).nth (n + 1) = (cons l.head l.tail).tail.nth n