mathlib-initiative/mathlib-tactics huggingface dataset:
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'
⊢ ¬a = x'

Tactic:
grind

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

Goal state before:
pp: case false
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (false, b).1 then f true (false, b).2 else f false (false, b).2) = f (false, b).1 (false, b).2

Tactic:
rfl

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

Goal state before:
pp: case true
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (true, b).1 then f true (true, b).2 else f false (true, b).2) = f (true, b).1 (true, b).2

Tactic:
rfl

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

Goal state before:
pp: case hi.some.none.none
α : 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 : α
IH : encode none = encode none
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) none)

Tactic:
rfl

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

Goal state before:
pp: case none.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
⊢ (Option.casesOn (none, none).1 (none, none).2 fun b ↦ ((none, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, none).1 (none, none).2

Tactic:
rfl

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

Goal state before:
pp: case none.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (none, some val✝).1 (none, some val✝).2 fun b ↦ ((none, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, some val✝).1 (none, some val✝).2

Tactic:
rfl

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

Goal state before:
pp: case some.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (some val✝, none).1 (some val✝, none).2 fun b ↦ ((some val✝, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, none).1 (some val✝, none).2

Tactic:
rfl

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

Goal state before:
pp: case some.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝¹ val✝ : α
⊢ (Option.casesOn (some val✝¹, some val✝).1 (some val✝¹, some val✝).2 fun b ↦ ((some val✝¹, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝¹, some val✝).1 (some val✝¹, some val✝).2

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun a b ↦ f a = b
⊢ Primrec f

Tactic:
rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩

Goal state after:
α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ (List.casesOn (id []) none fun b l ↦ some ([], b, l).2.1) = [].head?

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) none fun b l ↦ some (head✝ :: tail✝, b, l).2.1) = (head✝ :: tail✝).head?

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ (List.casesOn (id []) [] fun b l ↦ ([], b, l).2.2) = [].tail

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) [] fun b l ↦ (head✝ :: tail✝, b, l).2.2) = (head✝ :: tail✝).tail

Tactic:
rfl

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:
rfl

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

Goal state before:
pp: case false.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b) none) = encode (Option.map Sum.inl none)

Tactic:
rfl

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

Goal state before:
pp: case false.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ encode (Option.map (fun b ↦ 2 * encode b) (some val✝)) = encode (Option.map Sum.inl (some val✝))

Tactic:
rfl

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

Goal state before:
pp: case true.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) none) = encode (Option.map Sum.inr none)

Tactic:
rfl

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

Goal state before:
pp: case true.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : β
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) (some val✝)) = encode (Option.map Sum.inr (some val✝))

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
⊢ encode (none.bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a) =
    encode (none.bind fun x ↦ if h : p x then some ⟨x, h⟩ else none)

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : p a
⊢ encode a = encode ⟨a, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ fin.toEncodable = Fin.encodable n

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode none = encode (Option.map Subtype.val none)

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
a : α
h : p a
⊢ encode (some ⟨a, h⟩) = encode (Option.map Subtype.val (some ⟨a, h⟩))

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a ↦ ↑(f a)) none) = encode (Option.map f none)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s ↦ bif p (a, b, s).1 (a, b, s).2.1 then 0 else (a, b, s).2.2.succ) 0 (f a) =
    List.findIdx (p a) (f a)

Tactic:
by dsimp; induction f a <;> simp [List.findIdx_cons, *]

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

Goal state before:
pp: case zero
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
⊢ Nat.rec (some [])
      (fun n IH ↦
        (a, n, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      0 =
    some (List.map (f a) (List.range 0))

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
a : α
⊢ encode ↑(f a) = encode (f a)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a // a < n } := Primcodable.subtype ⋯
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec fun a ↦ ↑(Fin.equivSubtype (f a))

Tactic:
rfl

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:
grind

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode false) (g a) fun b ↦ f (a, b).1) = bif false then f a else g a

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case true
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode true) (g a) fun b ↦ f (a, b).1) = bif true then f a else g a

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn Option.none Option.none (g a) = Option.none.bind (g a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ Option.casesOn (Option.some val✝) Option.none (g a) = (Option.some val✝).bind (g a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn Option.none (g a) fun b ↦ b) = Option.none.getD (g a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
val✝ : β
⊢ (Option.casesOn (Option.some val✝) (g a) fun b ↦ b) = (Option.some val✝).getD (g a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some [])
      (fun y IH ↦
        (a, y, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      0 =
    Option.some ((fun a n ↦ List.map (f a) (List.range n)) a.1 0)

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
⊢ (List.casesOn ([], b).1 [] fun b_1 l ↦ g (([], b), b_1, l).1.2 (([], b), b_1, l).2.1 :: (([], b), b_1, l).2.2) =
    List.modifyHead (g b) []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
head✝ : α
tail✝ : List α
⊢ (List.casesOn (head✝ :: tail✝, b).1 [] fun b_1 l ↦
      g ((head✝ :: tail✝, b), b_1, l).1.2 ((head✝ :: tail✝, b), b_1, l).2.1 :: ((head✝ :: tail✝, b), b_1, l).2.2) =
    List.modifyHead (g b) (head✝ :: tail✝)

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
h : [].length = n
⊢ (List.Vector.toList ⟨[], h⟩).tail = (List.Vector.tail ⟨[], h⟩).toList

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = n
⊢ (List.Vector.toList ⟨head✝ :: tail✝, h⟩).tail = (List.Vector.tail ⟨head✝ :: tail✝, h⟩).toList

Tactic:
rfl

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

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH ↦ y) 0 = 0 - 1

Tactic:
rfl

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

Goal state before:
pp: case succ
v : List.Vector ℕ (Nat.succ 0)
n✝ : ℕ
⊢ Nat.rec 0 (fun y IH ↦ y) (n✝ + 1) = n✝ + 1 - 1

Tactic:
rfl

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

Goal state before:
pp: v : List.Vector ℕ 0
⊢ 0 = encode nil

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
m : ℕ := n.div2.div2
⊢ m < n + 4

Tactic:
simp only [m, div2_val]
      exact
        lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
          (Nat.succ_le_succ (Nat.le_add_right _ _))

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

Goal state before:
pp: case pos
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).1

Tactic:
rfl

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

Goal state before:
pp: case neg
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).1

Tactic:
rfl

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

Goal state before:
pp: case pos
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).2

Tactic:
rfl

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

Goal state before:
pp: case neg
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h✝ : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt - (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).2

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2.inr
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α
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
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, k.succ ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
grind

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
n : ℕ
⊢ (max (f n) (g n) + 1) ^ 2 ≤ (ack (max a b) n + 1) ^ 2

Tactic:
by rw [max_ack_left]; gcongr; exacts [(ha n).le, (hb n).le]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case prec
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
this : ∀ {m n : ℕ}, rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n ↦ rec (f z) (fun y IH ↦ g (pair z (pair y IH))) n) n < ack m n

Tactic:
exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
⊢ Primrec pappAck

Tactic:
convert! this using 2 with n

Goal state after:
this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
n : ℕ
⊢ pappAck n = Nat.rec succ (fun x c ↦ pappAck.step c) n
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 [] = some (F a zero)

Tactic:
rfl

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

Goal state before:
pp: ⊢ (fun n ↦ 1) =o[atTop] fun n ↦ log ↑n ^ 2

Tactic:
calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc✝ : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hnxb : x ≠ b
hxa : Gmax.Adj ↑↑x ↑↑a
hxb : Gmax.Adj ↑↑a ↑↑b
hnadjxb : ¬Gmax.Adj ↑↑x ↑↑b
c : V
hc : ↑↑a ≠ c ∧ ¬Gmax.Adj (↑↑a) c
hbnec : ↑↑b ≠ c
⊢ ¬?m.314 ≤ Gmax

Tactic:
rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
      simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb]

Goal state after: