mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 1 ≠ ⊤

Tactic:
by simp

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 ⊆ Set.univ

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this✝¹ : IsAntichain H.Adj sᶜ
this✝ : IsAntichain G.Adj (⇑f ⁻¹' sᶜ)
this : G.IsVertexCover (⇑f ⁻¹' s)
⊢ ∀ ⦃x : V⦄, x ∈ ⇑f ⁻¹' s → { toFun := ⇑f, inj' := hf } x ∈ s

Tactic:
by simp

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: x✝ : YoungDiagram
⊢ x✝.transpose.transpose = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: ⊢ ∀ {a b : YoungDiagram},
    { toFun := transpose, invFun := transpose, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := transpose, invFun := transpose, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ Nat.pair (unpair n).1 (unpair n).2 = id n

Tactic:
by simp

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

Goal state before:
pp: f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
n : ℕ
⊢ unpaired (fun z n ↦ Nat.rec m (fun y IH ↦ f (unpair (Nat.pair z (Nat.pair y IH))).2) n) (Nat.pair 0 (id n)) =
    Nat.rec m (fun y IH ↦ f (Nat.pair y IH)) n

Tactic:
by simp

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

Goal state before:
pp: f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
⊢ ∀ (n : ℕ), Nat.rec m (fun y IH ↦ f (unpair (Nat.pair y IH)).1) n = Nat.casesOn n m f

Tactic:
by simp

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

Goal state before:
pp: f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
n : ℕ
⊢ unpaired
      (fun z n ↦
        Nat.rec (f z)
          (fun y IH ↦
            g (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).1 (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).1))
          n)
      n =
    unpaired (fun z n ↦ Nat.casesOn n (f z) fun y ↦ g (Nat.pair z y)) n

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ Nat.pair (unpair n).2 (unpair n).1 = unpaired (swap Nat.pair) n

Tactic:
by simp

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

Goal state before:
pp: f : ℕ → ℕ → ℕ
hf : Nat.Primrec (unpaired f)
n : ℕ
⊢ unpaired f (unpaired (swap Nat.pair) n) = unpaired (swap f) n

Tactic:
by simp

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

Goal state before:
pp: ⊢ ppred 0 = none ↔ 0 = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type ?u.3
inst✝ : Denumerable α
⊢ ∀ (n : ℕ), n.succ = encode (decode n)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Primrec f
n : ℕ
⊢ (encode (Option.map f (decode n))).pred = encode (f (ofNat α n))

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Nat.Primrec fun n ↦ encode (f (ofNat α n))
n : ℕ
⊢ (encode (f (ofNat α n))).succ = encode (Option.map f (decode n))

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ ∀ (n : ℕ), encode (decode n) = encode (Option.map id (decode n))

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → β
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun a ↦ e (f a)
a : σ
⊢ e.symm (e (f a)) = f a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → α
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun a ↦ e.symm (f a)
a : σ
⊢ e (e.symm (f a)) = f a

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ ((Nat.unpair n).1, (Nat.unpair n).2) = Nat.unpair n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
σ : Type u_6
inst✝² : Denumerable α
inst✝¹ : Denumerable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun n ↦ f (ofNat (α × β) n).1 (ofNat (α × β) n).2) ↔
    Primrec (Nat.unpaired fun m n ↦ f (ofNat α m) (ofNat β n))

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
h : (p'.takeUntil x' hx'p).toSubgraph.Adj x b
⊢ b ∈ {x, b}

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
h : (p'.takeUntil x' hx'p).toSubgraph.Adj x b
⊢ x ∈ {x, b}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → Prop
w✝ : DecidablePred p
hp : Primrec fun a ↦ decide (p a)
⊢ ∀ (n : α), (!decide (p n)) = decide ¬p n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p q : α → Prop
w✝¹ : DecidablePred p
hp : Primrec fun a ↦ decide (p a)
w✝ : DecidablePred q
hq : Primrec fun a ↦ decide (q a)
⊢ ∀ (n : α), (decide (p n) && decide (q n)) = decide (p n ∧ q n)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p q : α → Prop
w✝¹ : DecidablePred p
hp : Primrec fun a ↦ decide (p a)
w✝ : DecidablePred q
hq : Primrec fun a ↦ decide (q a)
⊢ ∀ (n : α), (decide (p n) || decide (q n)) = decide (p n ∨ q n)

Tactic:
by simp

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

Goal state before:
pp: p : ℕ × ℕ
⊢ ¬p.2 ≤ p.1 ↔ (fun x1 x2 ↦ x1 < x2) p.1 p.2

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n : ℕ
⊢ f✝ (g✝ n) ∈ ↑g✝ n >>= ↑f✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: this : Primrec₂ fun n m ↦ if n = m.succ then 0 else 1
⊢ ∀ (a : ℕ),
    a ∉ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> ↑(unpaired fun n m ↦ if n = m.succ then 0 else 1) (Nat.pair 0 n)

Tactic:
by simp

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

Goal state before:
pp: case succ
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
k : ℕ
ih : ∀ b' ∈ bindList b k, m b' < m b + 1 - k
⊢ ∀ (b' x : β), x ∈ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) k → b' ∈ l x → m b' < m b - k

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
e : decode n = Option.none
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a ↦
          Part.map encode ((fun a ↦ Part.map (fun b ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑Option.none).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)

Tactic:
simp [e, Nat.rfind_zero_none, map_map, map_id']

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
val✝ : α
e : decode n = Option.some val✝
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a ↦
          Part.map encode ((fun a ↦ Part.map (fun b ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑(Option.some val✝)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)

Tactic:
simp [e, Nat.rfind_zero_none, map_map, map_id']

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Computable (f i)
a : α
⊢ (Vector.mOfFn fun i ↦ ↑(f i) a) = (↑fun a ↦ List.Vector.ofFn fun i ↦ f i a) a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : Primcodable α
w✝ : DecidablePred p
hf : Primrec fun a ↦ decide (p a)
⊢ ∀ (a : List α), ¬(filter (fun x ↦ decide (p x)) a).length = 0 ↔ ∃ a_1 ∈ a, p a_1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : Primcodable α
w✝ : DecidablePred p
hf : Primrec fun a ↦ decide (p a)
⊢ ∀ (a : List α), (filter (fun x ↦ decide (p x)) a).length = a.length ↔ ∀ a_1 ∈ a, p a_1

Tactic:
by simp

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

Goal state before:
pp: p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∃ a_1 ∈ range a, p a_1) ↔ ∃ x < a, p x

Tactic:
by simp

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

Goal state before:
pp: p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∀ a_1 ∈ range a, p a_1) ↔ ∀ x < a, p x

Tactic:
by simp

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

Goal state before:
pp: R : ℕ → ℕ → Prop
hf : PrimrecRel R
⊢ ∀ (a : ℕ × ℕ), (∃ a_1 ∈ range a.1, R a_1 a.2) ↔ (fun n y ↦ ∃ x < n, R x y) a.1 a.2

Tactic:
by simp

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

Goal state before:
pp: R : ℕ → ℕ → Prop
hf : PrimrecRel R
⊢ ∀ (a : ℕ × ℕ), (∀ a_1 ∈ range a.1, R a_1 a.2) ↔ (fun n y ↦ ∀ x < n, R x y) a.1 a.2

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_3
inst✝ : Primcodable σ
n : ℕ
x✝ : (Fin n → σ) × Fin n
v : Fin n → σ
i : Fin n
⊢ (List.Vector.ofFn (v, i).1).get (v, i).2 = id (v, i).1 (v, i).2

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
h : ∀ (i : Fin n), Primrec (f i)
a : Fin n × α
⊢ (List.Vector.ofFn fun i ↦ f i a.2).get a.1 = f a.1 a.2

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Code.const 0 = Code.const 0
⊢ 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2.inl.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 : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
m : ℕ
mk : m < k.succ
km : k ≤ m
⊢ Sum.inr a₂ ∈ F a m

Tactic:
le_antisymm (Nat.le_of_lt_succ mk) km

Goal state after:
case refine_2.inl.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 : ℕ
hk : Sum.inr a₂ ∈ F a k
h₂ : Sum.inl b ∈ f a₂
m : ℕ
mk : m < k.succ
km : k ≤ m
⊢ Sum.inr a₂ ∈ F a k
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: f : ℕ → ℕ
h : Primrec fun v ↦ f v.head
v : ℕ
⊢ f (ofFn fun i ↦ id v).head = f v

Tactic:
by simp

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

Goal state before:
pp: f : ℕ → ℕ → ℕ
h : Primrec fun v ↦ f v.head v.tail.head
v : ℕ × ℕ
⊢ f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Ackermann

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ 0 < ack 0 n

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ 1 < ack (0 + 1) n

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ 1 < ack 0 (n + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ 0 + n < ack 0 n

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case zero
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m : ℕ
⊢ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) 0 < ack (max a b + 9) (m + 0)

Tactic:
apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p ↦
    p.1.2[p.2.2]?.bind fun s ↦
      p.1.2[(unpair p.2.2).1]?.bind fun s₁ ↦
        Option.map
          (fun s₂ ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          p.1.2[(unpair p.2.2).2]?
this✝ : Primrec G₁
G : α → List σ → Option σ :=
  fun a IH ↦
    Nat.casesOn IH.length (some (z a)) fun n ↦
      Nat.casesOn n (some (s a)) fun n ↦
        Nat.casesOn n (some (l a)) fun n ↦ Nat.casesOn n (some (r a)) fun n ↦ G₁ ((a, IH), n, n.div2.div2)
this : Primrec₂ G
a : α
⊢ F (id a) (ofNat Code (encode (c a))) = F a (c a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < n
⊢ 4 + 4 ≤ 9

Tactic:
by simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p ↦
    p.1.2[p.2.2]?.bind fun s ↦
      p.1.2[(unpair p.2.2).1]?.bind fun s₁ ↦
        Option.map
          (fun s₂ ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          p.1.2[(unpair p.2.2).2]?
this✝ : Primrec G₁
G : α → List σ → Option σ :=
  fun a IH ↦
    Nat.casesOn IH.length (some (z a)) fun n ↦
      Nat.casesOn n (some (s a)) fun n ↦
        Nat.casesOn n (some (l a)) fun n ↦ Nat.casesOn n (some (r a)) fun n ↦ G₁ ((a, IH), n, n.div2.div2)
this : Primrec₂ G
a : α
⊢ G (a, List.map (fun n ↦ F a (ofNat Code n)) (List.range 0)).1
      (a, List.map (fun n ↦ F a (ofNat Code n)) (List.range 0)).2 =
    some (F a (ofNat Code 0))

Tactic:
simp [ofNatCode_eq, ofNatCode]; rfl

Goal state after: