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
⊢ ∃ x' ∈ {x, b}, ∃ p, p.IsPath ∧ p.toSubgraph.Adj a c ∧ ¬p.toSubgraph.Adj x b

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Primrec fun a ↦ ↑a.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
ps : List (α × β)
⊢ (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
by

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
x' : V
hx' : x' ∈ {x, b}
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
⊢ ¬p.toSubgraph.spanningCoe.Adj x b

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
⊢ n ∈ rfind p

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ → Bool
m : ℕ
pm : p m = true
this : true ∈ ↑p m
n : ℕ
hn : n ∈ rfind ↑p
h : m < n
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
⊢ true ∈ (fun n ↦ ↑(Option.some (f n).isSome)) (Nat.find h')

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
⊢ (rfindOpt f).Dom

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
⊢ a ∈ rfindOpt f

Tactic:
by

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

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Nat.Partrec ↑f

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: x✝² x✝¹ : ℕ
x✝ : x✝¹ ∈ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> (↑fun x ↦ 1) (Nat.pair x✝² n)
h : (Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> (↑fun x ↦ 1) (Nat.pair x✝² n)).Dom
h✝ : (Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> (↑fun x ↦ 1) (Nat.pair x✝² n)).get h = x✝¹
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: f g h : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
hh : Nat.Partrec h
a s : ℕ
⊢ (s ∈
      Nat.pair <$> Part.some a <*> f a >>=
        unpaired fun a n ↦
          Nat.rec (g a)
            (fun y IH ↦ do
              let i ← IH
              h (Nat.pair a (Nat.pair y i)))
            n) ↔
    s ∈
      (f a).bind fun n ↦
        Nat.rec (g a)
          (fun y IH ↦ do
            let i ← IH
            h (Nat.pair a (Nat.pair y i)))
          n

Tactic:
by

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

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
by

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

Goal state before:
pp: β : 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 : ℕ
⊢ ∀ b' ∈ bindList b k, m b' < m b + 1 - k

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ (do
      let n ← (↑fun n ↦ encode (Option.map f (decode n))) n
      ↑n.ppred) =
    (↑(decode n)).bind fun a ↦ map encode (↑f a)

Tactic:
by

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
x' : V
hx' : x' ∈ {x, b}
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
⊢ p.toSubgraph.spanningCoe ≤ G ⊔ edge a c

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑(decode n)).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> (↑(decode n)).bind fun a ↦ map encode (↑f a)) <*> (↑(decode n)).bind fun a ↦ map encode (↑g a)) =
    (↑(decode n)).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = (↑(decode n)).bind fun a ↦ map encode ((fun x ↦ Part.none) a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑(decode n)).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑(decode n)).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β → σ
hf : Partrec f
hg : Computable₂ g
⊢ Partrec fun a ↦ Part.map (g a) (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β → σ
hf : Partrec f
hg : Computable₂ g
⊢ Partrec fun a ↦ Part.map (g a) (f a)

Tactic:
by
  simpa [bind_some_eq_map] using Partrec.bind (g := fun a x => some (g a x)) hf hg

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

Goal state before:
pp: β : 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
bindList_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
⊢ ∀ (a : β), a ∉ bindList b (m b + 1)

Tactic:
by

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

Goal state before:
pp: β : 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
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
⊢ b ∈ bs ∧ bs' ⊆ bs

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
⊢ (((↑(decode n)).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑(decode n)).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a ↦ Part.map encode (↑g a)
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ f (g a)) a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: f : ℕ →. ℕ
⊢ Partrec f ↔ Nat.Partrec f

Tactic:
by

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

Goal state before:
pp: β : 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
bindList_eq_nil : bindList b (m b + 1) = []
bs bs' : List β
has : bs' ⊆ bs
⊢ mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : ℕ → ℕ →. α
h : Partrec (Nat.unpaired f)
⊢ Partrec₂ f

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
⊢ (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)) =
    (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)

Tactic:
by

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
x'✝ : V
hx'✝ : x'✝ ∈ {x, b}
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
x' : V
hx' : x' ∈ {x, b}
c' : V
hc : c' ≠ a
hadj : p.toSubgraph.Adj c' x'
⊢ M2.Adj c' x'

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
⊢ ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) m).Dom

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH ↦ IH.bind fun i ↦ h (a, y, i).1 (f (a, y, i).1).pred) (f a) =
    Nat.casesOn (f a) (Part.some (g a)) (h a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
h : Nat.Partrec fun n ↦ (↑(decode₂ α n)).bind fun a ↦ Part.map encode (f a)
⊢ Partrec fun a ↦ Part.map encode (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a ↦ Vector.mOfFn fun i ↦ f i a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
⊢ ((↑(decode n)).bind fun a ↦
      map encode
        ((fun a ↦
            (do
                  let n ← (↑fun n ↦ encode (decode n)) a.2
                  ↑n.ppred).bind
              ↑fun b ↦ (fun a n ↦ (decode n).bind (f a)) (a, b).1.1 (a, b).1.2)
          a)) =
    (↑(decode n)).bind fun a ↦ map encode ((↑fun p ↦ f p.1 p.2) a)

Tactic:
by

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

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
⊢ Computable₂ fun a n ↦ (decode n).bind (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Computable₂ fun a n ↦ Option.map (f a) (decode n)) ↔ Computable₂ f

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH ↦ IH.bind fun i ↦ ↑(h a) (y, i)) (f a) =
    (↑fun a ↦ Nat.rec (g a) (fun y IH ↦ h a (y, IH)) (f a)) a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : 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 (c a)) (g a) fun b ↦ f (a, b).1) = bif c a then f a else g a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (o a) (f a) (g a))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : 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 (f a) Option.none (g a) = (f a).bind (g a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
⊢ Computable fun a ↦ Option.map (g a) (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
by

Goal state after: