mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
⊢ IsLowerSet ↑(YoungDiagram.cellsOfRowLens w)

Tactic:
by

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

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
⊢ (ofRowLens w hw).rowLens.length = w.length

Tactic:
by

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

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
i : Fin w.length
⊢ (ofRowLens w hw).rowLen ↑i = w[i]

Tactic:
by

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

Goal state before:
pp: μ : YoungDiagram
⊢ ofRowLens μ.rowLens ⋯ = μ

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
x' : V
h : x' ≠ c
⊢ ¬M2.Adj x' a

Tactic:
by

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

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

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

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

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

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

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

Goal state before:
pp: n : ℕ
⊢ Nat.casesOn n 0 id = n.pred

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ unpaired (fun z n ↦ Nat.rec (id z) (fun y IH ↦ (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.succ) n) p =
    unpaired (fun x1 x2 ↦ x1 + x2) p

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ unpaired (fun z n ↦ Nat.rec (id z) (fun y IH ↦ (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.pred) n) p =
    unpaired (fun x1 x2 ↦ x1 - x2) p

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.pred = n.ppred.getD 0

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ (m - n).ppred.getD 0 = (m.psub (n + 1)).getD 0

Tactic:
by

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

Goal state before:
pp: m : ℕ
⊢ ppred 0 = some m ↔ m.succ = 0

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ (n + 1).ppred = some m ↔ m.succ = n + 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).ppred = none ↔ n + 1 = 0

Tactic:
by

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

Goal state before:
pp: m k : ℕ
⊢ m.psub 0 = some k ↔ k + 0 = m

Tactic:
by

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

Goal state before:
pp: m n k : ℕ
⊢ m.psub (n + 1) = some k ↔ k + (n + 1) = m

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ unpaired
      (fun z n ↦
        Nat.rec 0
          (fun y IH ↦
            unpaired (fun x1 x2 ↦ x1 + x2)
              (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).1 (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2))
          n)
      p =
    unpaired (fun x1 x2 ↦ x1 * x2) p

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ m.psub n = none ↔ m < n

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ unpaired
      (fun z n ↦
        Nat.rec 1
          (fun y IH ↦
            unpaired (fun x1 x2 ↦ x1 * x2)
              (Nat.pair (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2 (unpair (Nat.pair z (Nat.pair y IH))).1))
          n)
      p =
    unpaired (fun x1 x2 ↦ x1 ^ x2) p

Tactic:
by

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

Goal state before:
pp: m n k : ℕ
⊢ m.psub (n + k) = do
    let __do_lift ← m.psub n
    __do_lift.psub k

Tactic:
by

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

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

Goal state before:
pp: α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode (decode n) = encode (decode n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (Nat.casesOn n 1 fun x ↦ 0) = encode (decode n)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ m.psub' n = m.psub n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn n 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (decode n)

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x ↦ Nat.casesOn x 2 fun x ↦ 0) = encode (decode (n + 2))

Tactic:
by

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

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

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (Option.map some (decode n))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun x_1 ↦ (encode x).succ) = encode (Option.map (fun x_1 ↦ x) (decode n))

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) (decode n))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a ↦ encode (f a)
n : ℕ
⊢ encode (Option.map (fun a ↦ encode (f a)) (decode n)) = encode (Option.map f (decode n))

Tactic:
by

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

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

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

Goal state before:
pp: α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired (fun z n ↦ Nat.casesOn n 0 fun y ↦ (Nat.pair z y).succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (decode n)

Tactic:
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]

Goal state after:
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ (Nat.pair n_1 n).succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode ((decode (Nat.unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
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.toSubgraph.Adj a ?m.488

Tactic:
by

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

Goal state before:
pp: α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired (fun z n ↦ Nat.casesOn n 0 fun y ↦ (Nat.pair z y).succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (decode n)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired (fun z n ↦ Nat.casesOn n 0 fun y ↦ (Nat.unpair (Nat.pair z y)).1.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (Option.map Prod.fst (decode n))

Tactic:
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.fst ((decode (Nat.unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired (fun z n ↦ Nat.casesOn n 0 fun y ↦ (Nat.unpair (Nat.pair z y)).1.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (Option.map Prod.fst (decode n))

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired (fun z n ↦ Nat.casesOn n 0 fun y ↦ (Nat.unpair (Nat.pair z y)).2.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (Option.map Prod.snd (decode n))

Tactic:
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.snd ((decode (Nat.unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired (fun z n ↦ Nat.casesOn n 0 fun y ↦ (Nat.unpair (Nat.pair z y)).2.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (Option.map Prod.snd (decode n))

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) (decode n))

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
a : α
l : List α
n : ℕ
⊢ (Nat.casesOn n (encode a).succ fun n ↦ encode l[ofNat ℕ n]?) = encode (a :: l)[ofNat ℕ n]?

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
⊢ f = g

Tactic:
by

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

Goal state before:
pp: ⊢ Primrec₂ Nat.pair

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α × β → σ
⊢ Primrec₂ (Function.curry f) ↔ Primrec f

Tactic:
by

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 : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a))) =
    some (List.casesOn (f a) (g a) fun b l ↦ h a (b, l))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
⊢ Primrec fun a ↦ decide (p a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
a : Option α
b : Option β
⊢ Option.map (fun p ↦ f p.1 p.2) (a.bind fun a ↦ Option.map (Prod.mk a) b) = a.bind fun a ↦ Option.map (f a) b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec₂ f ↔ Nat.Primrec (Nat.unpaired fun m n ↦ encode ((decode m).bind fun a ↦ Option.map (f a) (decode n)))

Tactic:
by

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
this : ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
⊢ Primrec fun a ↦ List.foldl (fun s b ↦ h a (s, b)) (g a) (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
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 ∈ {x, b} | x ∈ Walk.support ?m.519}.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.unpaired
      (fun z n ↦
        Nat.casesOn n 0 fun y ↦
          Nat.unpaired
            (fun z n ↦
              Nat.rec (encode (Option.map f (decode z)))
                (fun y IH ↦
                  encode
                    (Option.map (fun p ↦ g p.1 p.2)
                      (decode
                        (Nat.pair (Nat.unpair (Nat.pair z (Nat.pair y IH))).1
                          (Nat.pair (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).1
                            (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).2.pred)))))
                n)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (Nat.unpair (Nat.unpair (Nat.pair z y)).1).2))
      (Nat.pair (id n) (encode (decode (Nat.unpair n).1))) =
    Nat.unpaired
      (fun m n ↦
        encode ((decode m).bind fun a ↦ Option.map (fun n ↦ Nat.rec (f a) (fun n IH ↦ g a (n, IH)) n) (decode n)))
      n

Tactic:
by

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
⊢ Primrec fun a ↦ List.foldl (fun s b ↦ h a (s, b)) (g a) (f a)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (g a) (fun n IH ↦ h a (n, IH).2) (f a) = (h a)^[f a] (g a)

Tactic:
by

Goal state after: