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

Goal state before:
pp: case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v : Fin n
hv : v ∈ ↑p'
w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_mem : w' ∈ s
hw'_eq : ↑w' = w
hp' : ∃ a, y ↑a ⋯ = p'
⊢ G.Adj v w

Tactic:
Subtype.exists

Goal state after:
case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v : Fin n
hv : v ∈ ↑p'
w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_mem : w' ∈ s
hw'_eq : ↑w' = w
hp' : ∃ a, ∃ (h : a ∈ K.parts), y a ⋯ = p'
⊢ G.Adj v w
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: x✝ : ℕ × ℕ
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ∅

Tactic:
simp

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

Goal state before:
pp: μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ μ.transpose.transpose.cells ↔ x ∈ μ.cells

Tactic:
simp

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

Goal state before:
pp: case mp
μ : YoungDiagram
⊢ μ = μ.transpose.transpose

Tactic:
simp

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

Goal state before:
pp: case mpr
ν : YoungDiagram
⊢ ν.transpose.transpose = ν

Tactic:
simp

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

Goal state before:
pp: μ ν : YoungDiagram
⊢ μ = ν.transpose.transpose ↔ μ = ν

Tactic:
simp

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

Goal state before:
pp: μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ ν = ν.transpose.transpose

Tactic:
simp

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

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

Tactic:
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:
simp

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

Goal state before:
pp: μ : YoungDiagram
j : ℕ
⊢ (fun i ↦ (i, j) ∉ μ.cells) = fun j_1 ↦ (j, j_1) ∉ μ.transpose

Tactic:
simp

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

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ μ.transpose

Tactic:
simp

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

Goal state before:
pp: case e'_3
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 = μ.transpose.rowLen j2

Tactic:
simp

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

Goal state before:
pp: case e'_4
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j1 = μ.transpose.rowLen j1

Tactic:
simp

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

Goal state before:
pp: case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.out groupElts • ↑(↑ps index)).Nonempty ↔ (↑(↑ps index)).Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.out groupElts • ↑(↑ps index)).Finite ↔ (↑(↑ps index)).Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case h
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
i✝ : ιₚ
gx✝ : G
⊢ 1 • { index := i✝, groupElts := ↑gx✝ } = { index := i✝, groupElts := ↑gx✝ }

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g⁻¹ • ↑pt ↔ g • x ∈ ↑pt

Tactic:
Set.mem_inv_smul_set_iff

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

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

Tactic:
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:
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:
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:
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:
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:
simp

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

Goal state after:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2
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:
simp

Goal state after:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
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:
simp

Goal state after:
p : ℕ
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
Module: Mathlib.Data.Nat.PSub

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

Tactic:
simp

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

Goal state after:
p : ℕ
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
Module: Mathlib.Data.Nat.PSub

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

Tactic:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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 none

Tactic:
simp

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

Goal state before:
pp: case h
n✝ n : ℕ
⊢ 2 ≤ n + 2

Tactic:
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:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
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:
simp

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

Goal state before:
pp: case none
α : 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 none) =
    encode (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))

Tactic:
simp

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

Goal state before:
pp: case some.none
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ Nat.rec 0 (fun n_1 n_ih ↦ (Nat.pair n n_1).succ) (encode none)) (encode (some val✝)) =
    encode ((some val✝).bind fun a ↦ Option.map (Prod.mk a) none)

Tactic:
simp

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

Goal state before:
pp: case some.some
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ Nat.rec 0 (fun n_1 n_ih ↦ (Nat.pair n n_1).succ) (encode (some val✝))) (encode (some val✝¹)) =
    encode ((some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝))

Tactic:
simp

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

Goal state before:
pp: case none
α : 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 none) =
    encode (Option.map Prod.fst (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ 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 (some val✝)) =
    encode (Option.map Prod.fst ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
simp

Goal state after:
case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ encode val✝ + 1) (encode (decode (Nat.unpair n).2)) =
    encode (Option.map (Function.const β val✝) (decode (Nat.unpair n).2))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some.none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ encode val✝ + 1) (encode none) = encode (Option.map (Function.const β val✝) none)

Tactic:
simp

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

Goal state before:
pp: case some.some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ encode val✝¹ + 1) (encode (some val✝)) =
    encode (Option.map (Function.const β val✝¹) (some val✝))

Tactic:
simp

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

Goal state before:
pp: case none
α : 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 none) =
    encode (Option.map Prod.snd (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2))) (encode (some val✝)) =
    encode (Option.map Prod.snd ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
simp

Goal state after:
case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ n + 1) (encode (decode (Nat.unpair n).2)) = encode (decode (Nat.unpair n).2)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some.none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ n + 1) (encode none) = encode none

Tactic:
simp

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

Goal state before:
pp: case some.some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ n + 1) (encode (some val✝)) = encode (some val✝)

Tactic:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
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:
simp

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

Goal state before:
pp: case hz
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
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 : ℕ
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) 0)) =
    encode (decode 0)

Tactic:
simp

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

Goal state before:
pp: case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) (n + 1))) =
    encode (decode (n + 1))

Tactic:
simp

Goal state after:
case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
⊢ encode
      ((decode (Nat.unpair n).1).bind fun a ↦
        Option.map (List.cons (encode a))
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode (Option.map (fun x1 x2 ↦ x1 :: x2) (decode (Nat.unpair n).1) <*> decode (Nat.unpair n).2)
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:
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:
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:
simp

Goal state after: