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

Goal state before:
pp: ε : ℝ
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
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
refine ⟨univ.map ⟨fun p : K.parts ↦ y p.val p.prop, fun p₁ p₂ (heq : y p₁ _ = y p₂ _) ↦ ?_⟩,
        ?_, fun {p} hp ↦ ?_, fun p₁ hp₁ p₂ hp₂ hne v₁ hv₁ v₂ hv₂ ↦ ?_⟩
      · have hy₁' := mem_powersetCard.mp (hy p₁.val p₁.prop)
        have hy₂' := mem_powersetCard.mp (hy p₂.val p₂.prop)
        rw [← heq] at hy₂'
        obtain ⟨v, hv⟩ : (y p₁ _).Nonempty := by
          rw [← Finset.card_pos, hy₁'.right]
          exact ht_pos
        by_contra! hne
        absurd K.isCompleteBetween p₁.prop p₂.prop
          (Subtype.ext_iff.ne.mp hne) (hy₁'.left hv) (hy₂'.left hv)
        exact G.loopless.irrefl v
      · simp_rw [card_map, card_univ, card_coe]
        exact .inl (K.card_parts.resolve_right ht'_pos.ne')
      · simp_rw [univ_eq_attach, Finset.mem_map, mem_attach,
          Function.Embedding.coeFn_mk, true_and, Subtype.exists] at hp
        replace ⟨p, hp, hyp⟩ := hp
        rw [← hyp]
        have hy' := mem_powersetCard.mp (hy p hp)
        exact hy'.right
      · simp_rw [univ_eq_attach, coe_map, Function.Embedding.coeFn_mk,
          Set.mem_image, mem_coe, mem_attach, true_and, Subtype.exists] at hp₁ hp₂
        replace ⟨p₁, hp₁, hyp₁⟩ := hp₁
        rw [← hyp₁] at hv₁ hne
        have hy₁' := mem_powersetCard.mp (hy p₁ hp₁)
        replace ⟨p₂, hp₂, hyp₂⟩ := hp₂
        rw [← hyp₂] at hv₂ hne
        have hy₂' := mem_powersetCard.mp (hy p₂ hp₂)
        refine K.isCompleteBetween hp₁ hp₂ ?_ (hy₁'.left hv₁) (hy₂'.left hv₂)
        by_contra! heq
        simp [← heq] at hne

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
⊢ G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b

Tactic:
grind

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

Goal state before:
pp: case refl
μ : YoungDiagram
i x✝² : ℕ
x✝¹ x✝ : x✝² ∈ Prod.mk i ⁻¹' ↑μ.cells
⊢ x✝² = x✝²

Tactic:
rfl

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

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
h : (i, j) ∈ μ
x✝ : ℕ
hmj : x✝ ≤ j
⊢ i ≤ i

Tactic:
rfl

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

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
h : ∀ m ≤ j, (i, m) ∈ μ
⊢ j ≤ j

Tactic:
rfl

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

Goal state before:
pp: μ : YoungDiagram
a b : ℕ
⊢ b < μ.rowLen a ↔ b < μ.rowLen a

Tactic:
rfl

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

Goal state before:
pp: μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ μ.rowLen i1 ≤ μ.rowLen i1

Tactic:
rfl

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

Goal state before:
pp: case refine_2.index
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index

Tactic:
rfl

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

Goal state before:
pp: μ : YoungDiagram
a b : ℕ
⊢ a < μ.colLen b ↔ a < μ.colLen b

Tactic:
rfl

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

Goal state before:
pp: case refine_2.index
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
i₁ : ιₚ
g₁ g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₂ }.groupElts}
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₂ }.groupElts}
⊢ { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index

Tactic:
rfl

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

Goal state before:
pp: w : List ℕ
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ (h : c.1 < w.length), c.2 < w[c.1]

Tactic:
induction w generalizing c

Goal state after:
case nil
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens [] ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens (head✝ :: tail✝) ↔ ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]
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 ιₚ
g : G
i✝ : ιₚ
gx✝ : G
⊢ (g • { index := i✝, groupElts := ↑gx✝ }).index = { index := i✝, groupElts := ↑gx✝ }.index

Tactic:
rfl

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

Goal state before:
pp: μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
⊢ T i j1 ≤ T i j2

Tactic:
rcases eq_or_lt_of_le hj with h | h
  · rw [h]
  · exact T.row_weak h cell

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

Goal state before:
pp: μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ i✝ ≤ i✝

Tactic:
rfl

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

Goal state before:
pp: μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ j✝ ≤ j✝

Tactic:
rfl

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

Goal state before:
pp: case inl
w : List ℕ
hw : w.SortedGE
j2 i1 j1 : ℕ
hj : j1 ≤ j2
hi : i1 ≤ i1
h1 : (i1, j2).1 < w.length
h2 : (i1, j2).2 < w[(i1, j2).1]
⊢ w[i1] ≤ w[i1]

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ pred 0 = (ppred 0).getD 0

Tactic:
rfl

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (n✝ + 1).pred = (n✝ + 1).ppred.getD 0

Tactic:
rfl

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

Goal state before:
pp: case none
m n : ℕ
⊢ (none.getD 0).ppred.getD 0 = (none >>= ppred).getD 0

Tactic:
rfl

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

Goal state before:
pp: case some
m n val✝ : ℕ
⊢ ((some val✝).getD 0).ppred.getD 0 = (some val✝ >>= ppred).getD 0

Tactic:
rfl

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

Goal state before:
pp: case mp
n : ℕ
⊢ n.succ = n + 1

Tactic:
rfl

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

Goal state before:
pp: case mpr
n : ℕ
⊢ (n + 1).ppred = some n

Tactic:
rfl

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

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

Tactic:
rfl

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:
cases @decode α _ n

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ encode none = encode (Option.map encode none)

case some
α : Type u_1
inst✝ : Primcodable α
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map encode (some val✝))
Module: Mathlib.Computability.Primrec.Basic

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

Tactic:
rfl

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

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

Tactic:
rfl

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:
cases @decode α _ n

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

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✝))
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:
cases @decode α _ n

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

case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x : σ
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun x_1 ↦ (encode x).succ) = encode (Option.map (fun x_1 ↦ x) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

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

Tactic:
rfl

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

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

Tactic:
rfl

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:
cases @decode α _ n

Goal state after:
case none
α : 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 none) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) none)

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) (some val✝))
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:
cases @decode α _ n

Goal state after:
case none
α : 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)) none) = encode (Option.map f none)

case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a ↦ encode (f a)
n : ℕ
val✝ : α
⊢ encode (Option.map (fun a ↦ encode (f a)) (some val✝)) = encode (Option.map f (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : 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)) none) = encode (Option.map f none)

Tactic:
rfl

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

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

Tactic:
rfl

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:
cases @decode α _ n

Goal state after:
case none
α : 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 none) 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)) none)

case some
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 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)) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

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

Tactic:
by simp [Primrec₂, Primrec]; constructor

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 fun p ↦ f p.1 p.2) ↔ Primrec₂ f

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

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 β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih ↦
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH ↦
            encode
              (Option.map (fun p ↦ g p.1 p.2)
                ((decode n_1).bind fun a ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode none) =
    encode (none.bind fun a ↦ some (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (Nat.unpair n).2))

Tactic:
rfl

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

Goal state before:
pp: case zero
α : 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
a : α
l : List β
x : σ
⊢ (G a)^[0] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take 0 l), List.drop 0 l)

Tactic:
rfl

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:
induction f a <;> simp [*, -Function.iterate_succ, Function.iterate_succ']

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (none.bind fun b ↦ some (g x b)) = Option.map (g x) none

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
val✝ : β
⊢ ((some val✝).bind fun b ↦ some (g x b)) = Option.map (g x) (some val✝)

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
a : α
⊢ (Option.casesOn ((fun a x ↦ a) (none, a).1 (none, a).2) ((fun x b ↦ b) (none, a).1 (none, a).2) fun b ↦ b) =
    (none, a).1.getD (none, a).2

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
a val✝ : α
⊢ (Option.casesOn ((fun a x ↦ a) (some val✝, a).1 (some val✝, a).2) ((fun x b ↦ b) (some val✝, a).1 (some val✝, a).2)
      fun b ↦ b) =
    (some val✝, a).1.getD (some val✝, a).2

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
⊢ (Option.casesOn (id none) false fun b ↦ true) = none.isSome

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
inst✝ : Primcodable α
val✝ : α
⊢ (Option.casesOn (id (some val✝)) false fun b ↦ true) = (some val✝).isSome

Tactic:
rfl

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

Goal state before:
pp: case false
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec 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.Primrec.Basic

Goal state before:
pp: case true
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec 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.Primrec.List

Goal state before:
pp: case hi.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)
⊢ encode
      (none.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) none <*> decode (Nat.unpair n).2)

Tactic:
rfl

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

Goal state before:
pp: case false
α : Type u_1
inst✝ : Primcodable α
f : Bool → α
⊢ (bif id false then f true else f false) = f false

Tactic:
rfl

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

Goal state before:
pp: case true
α : Type u_1
inst✝ : Primcodable α
f : Bool → α
⊢ (bif id true then f true else f false) = f true

Tactic:
rfl

Goal state after: