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

Goal state before:
pp: case inr.refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : ((f a).tail.copy h1 ⋯).length = (f b).length
⊢ a = b

pp: case inr.refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
⊢ (fun p ↦ p.IsPath) ((f a).tail.copy h1 ⋯)

Tactic:
· rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
        lia

Goal state after:
case inr.refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
⊢ (fun p ↦ p.IsPath) ((f a).tail.copy h1 ⋯)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
⊢ {t} ⊆ G.neighborFinset u

Tactic:
simp [h.symm]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
a✝ b✝ : α
⊢ ¬h.setoid a✝ b✝ ↔ G.Adj a✝ b✝

Tactic:
change ¬¬ G.Adj _ _ ↔ _

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
a✝ b✝ : α
⊢ ¬¬G.Adj a✝ b✝ ↔ G.Adj a✝ b✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).2 ≤ ↑v.2

pp: case a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 ≤ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).2

Tactic:
· rw [Nat.div_le_iff_le_mul_add_pred v.1.pos, mul_comm r ↑v.2]
        exact Nat.add_le_add_left (Nat.le_pred_of_lt v.1.prop) (↑v.2 * r)

Goal state after:
case a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 ≤ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ (SimpleGraph.turanGraph (r * t) r).Adj
      ({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
          right_inv := ⋯ }
        v)
      ({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
          right_inv := ⋯ }
        w) ↔
    (completeEquipartiteGraph r t).Adj v w

Tactic:
turanGraph_adj,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ ↑({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
              right_inv := ⋯ }
            v) %
        r ≠
      ↑({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
              right_inv := ⋯ }
            w) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
n : ℕ
hn : 3 ≤ n
⊢ G.CliqueFree n

Tactic:
by
  refine not_cliqueFree_iff_top_isContained n |>.not_right.mpr fun hle ↦ ?_
  exact isAcyclic_iff_free_cycleGraph.mp h n hn <| hle.trans' <| .of_le le_top

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

Goal state before:
pp: case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
⊢ (turanGraph (Fintype.card V) r).Adj (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) a)
      (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) b) ↔
    G.Adj a b

Tactic:
turanGraph_adj,

Goal state after:
case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
⊢ ↑(((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) a) % r ≠ ↑(((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) b) % r ↔ G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
have n'r : n = n' + r := by lia

Goal state after:
case inr.inr
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case ha
n r : ℕ
⊢ 0 ≤ n % r

Tactic:
exact Nat.zero_le _

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

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

Tactic:
simp_rw [zero_tsub, mul_zero, Nat.mod_zero, Nat.div_zero, zero_add]

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
⊢ G.egirth ≤ ↑w.length

Tactic:
by
  classical
  by_contra! hlg
  let w' : G.Walk a a := w.cycleBypass
  have hwc' : w'.IsCycle := hwc.isCycle_cycleBypass
  have hwlg' : w'.length < G.egirth := by
    grw [w.length_cycleBypass_le_length]
    exact hlg
  exact not_le_of_gt hwlg' (SimpleGraph.egirth_le_length hwc')

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #t = #u) → Even #s

Tactic:
by
    rintro ⟨t, u, rfl, hdtu, hctu⟩
    simp_all

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ t'.choose t ^ r * t ≤ #(filter K t)

Tactic:
refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt ht_lt_t')

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ t'.choose t ^ r * t * (t' - t) ≤ #(filter K t) * (t' - t)
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
hG : G.IsHamiltonian
v : α
⊢ ∃ p, p.IsHamiltonianCycle

Tactic:
obtain ⟨u, p, hp⟩ := hG Fintype.one_lt_card.ne'

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
hG : G.IsHamiltonian
v u : α
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ ∃ p, p.IsHamiltonianCycle
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
⊢ Even (Fintype.card ↑c.supp)

Tactic:
#adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
  some instances that use the chain of coercions
  `[SetLike X], X → Set α → Sort _` are
  blocked by the discrimination tree. This can be fixed by redeclaring the instance for `X`
  using the double coercion but the proper fix seems to avoid the double coercion. -/

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
⊢ Even (Fintype.card ↑c.supp)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
⊢ (completeGraph V).Adj v u

Tactic:
simp [h.symm]

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ ⋯.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
generalize_proofs h

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.toPartition.parts.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.toPartition.parts.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
change Set.Finite (Coloring.colorClasses C) at h

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)
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' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
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'
hr_ne_1 : r ≠ 1
⊢ (1 - 1 / (↑r - 1) + (1 / (↑r - 1) - 1 / ↑r) + ε) * ↑n = (1 - 1 / ↑(r - 1) + ε') * ↑n

Tactic:
rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div
                (sub_ne_zero_of_ne (mod_cast hr_ne_1)) (mod_cast hr_pos.ne'),
                sub_sub_cancel, mul_one, one_div_mul_one_div_rev, mul_comm (r : ℝ) _,
                ← Nat.cast_pred hr_pos, add_assoc]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
by
  have ⟨f, hf⟩ := h
  obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists H
  have := H.isIndepSet_iff_isAntichain_adj.mp <| isIndepSet_compl_iff_isVertexCover.mpr hs₂
  have : IsAntichain G.Adj (f ⁻¹' sᶜ) := this.preimage hf (fun _ _ hadj ↦ f.map_rel' hadj)
  have : G.IsVertexCover (f ⁻¹' s) :=
    isIndepSet_compl_iff_isVertexCover.mp <| G.isIndepSet_iff_isAntichain_adj.mpr this
  grw [this.vertexCoverNum_le, ← hs₁]
  exact Function.Embedding.encard_le <| Function.Embedding.mk f hf |>.subtypeMap (by simp)

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

Goal state before:
pp: μ ν : YoungDiagram
⊢ IsLowerSet ↑(μ.cells ∩ ν.cells)

Tactic:
Finset.coe_inter

Goal state after:
μ ν : YoungDiagram
⊢ IsLowerSet (↑μ.cells ∩ ↑ν.cells)
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ μ.rowLen i1 < μ.rowLen i1

Tactic:
← mem_iff_lt_rowLen

Goal state after:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ (i1, μ.rowLen i1) ∈ μ
Module: Mathlib.Combinatorics.Young.YoungDiagram

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

Tactic:
← mem_iff_lt_rowLen

Goal state after:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ μ.transpose
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; induction p.unpair.2 <;> simp [*, Nat.pow_succ]

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.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 (decode (Nat.unpair n).1)) =
    encode ((decode (Nat.unpair n).1).bind fun a ↦ some (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (Nat.unpair n).2))

Tactic:
rcases @decode α _ n.unpair.1 with - | a

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

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ 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 (some a)) =
    encode ((some a).bind fun a ↦ some (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (Nat.unpair n).2))
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
      ((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)

Tactic:
rcases @decode α _ n.unpair.1 with - | a

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

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

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) = (unpair (f v)).1

Tactic:
simp [Nat.unpair]

Goal state after:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).1
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (unpair (f v)).2

Tactic:
simp [Nat.unpair]

Goal state after:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v ↦ (f v).sqrt
fss : Primrec' fun v ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).2
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 2 ^ 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
gcongr <;> lia

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m₁ m₂ : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) 0 < ack (m₂ + 1) 0

Tactic:
simpa using ack_strict_mono_left' 1 ((add_lt_add_iff_right 1).1 h)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
⊢ DifferentiableOn ℝ q (Set.Ioi 1)

Tactic:
refine DifferentiableOn.mul
        (DifferentiableOn.mono (differentiableOn_rpow_const _) fun z hz => ?_)
        differentiableOn_one_add_smoothingFn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
z : ℝ
hz : z ∈ Set.Ioi 1
⊢ z ∈ {0}ᶜ
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < (1 - ε ↑n) * asympBound g a b n

Tactic:
filter_upwards [R.eventually_asympBound_pos, eventually_one_sub_smoothingFn_pos] with n hn hn₂
    positivity

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ f u + g u ≤ f u + ‖g u‖

Tactic:
gcongr; exact le_norm_self (g u)

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u + g u ≤ f u + ‖g u‖

Tactic:
gcongr; exact le_norm_self (g u)

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case head
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ ∃ p q, Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q

Tactic:
| head s =>

Goal state after: