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

Goal state before:
pp: 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
⊢ G.edgeFinset.card = {default}ᶜ.card

Tactic:
choose f hf hf' using (hG.existsUnique_path · default)

Goal state after:
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
⊢ G.edgeFinset.card = {default}ᶜ.card
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : AddCommMonoid α
inst✝ : One α
⊢ (adjMatrix α G).trace = 0

Tactic:
simp [Matrix.trace]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ ∀ {a b : Fin 2},
    (pathGraph n).Adj ({ toFun := fun v ↦ ⟨↑v, ⋯⟩, inj' := ⋯ } a) ({ toFun := fun v ↦ ⟨↑v, ⋯⟩, inj' := ⋯ } b) ↔
      (pathGraph 2).Adj a b

Tactic:
simp [pathGraph]

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

Goal state before:
pp: case e'_4
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ ¬G.Adj x y

Tactic:
rwa [h.not_adj_iff_part_eq]

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

Goal state before:
pp: n r c : ℕ
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
rcases r.eq_zero_or_pos with rfl | hr; · simp
  suffices #{i ∈ range r | c % r = (n + i) % r} = 1 by
    rw [← card_filter, ← this]; apply Nat.eq_sub_of_add_eq'
    rw [card_filter_add_card_filter_not, card_range]
  apply le_antisymm
  · change #{i ∈ range r | _ ≡ _ [MOD r]} ≤ 1
    rw [card_le_one_iff]; intro w x mw mx
    simp only [mem_filter, mem_range] at mw mx
    have := mw.2.symm.trans mx.2
    rw [Nat.ModEq.add_iff_left rfl] at this
    change w % r = x % r at this
    rwa [Nat.mod_eq_of_lt mw.1, Nat.mod_eq_of_lt mx.1] at this
  · rw [one_le_card]; use ((r - 1) * n + c) % r
    simp only [mem_filter, mem_range]; refine ⟨Nat.mod_lt _ hr, ?_⟩
    rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
      Nat.mul_add_mod_self_left]

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
⊢ G.radius = G.ediam

Tactic:
have ediam_eq : G.ediam = e :=
      le_antisymm (iSup_le fun u ↦ (h u).le) ((h Classical.ofNonempty) ▸ eccent_le_ediam)

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
⊢ G.radius = G.ediam
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : (induce Kᶜ G).Adj u v
q : (induce Kᶜ G).Walk v w
ih : q.IsPath → f ⋯ = f ⋯
h' : (Walk.cons a q).IsPath
⊢ f ⋯ = f ⋯

Tactic:
exact (h u.prop v.prop a).trans (ih h'.of_cons)

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
h :
  ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
    G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x
x✝¹ : SimpleGraph (V ⊕ W)
x✝ : x✝¹ ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free x✝¹
h_le : x✝¹ ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free x✝¹
⊢ #x✝¹.edgeFinset ≤ x

Tactic:
convert h h_le h_free

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ 3 ≤ G.egirth

Tactic:
simpa using fun _ _ h ↦ h.three_le_length

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

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2

Tactic:
le_div_iff₀' (by positivity),

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ 2 * ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hcy : C y = C v
hx : x = w₁
hy : y ∈ ↑t
⊢ y ∈ ↑(insert v t)

Tactic:
by simp [hy]

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
u v : α
he : G.IsBridge s(u, v)
⊢ ¬G.IsHamiltonian

Tactic:
| h u v
   => 

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
u v : α
he : G.IsBridge s(u, v)
⊢ ¬G.IsHamiltonian
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.refl
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = v'
w' : V
hw : M.Adj v w'
hw' : f v = f v
⊢ f w' = f v'

Tactic:
rw [hv'.2 w' hw]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1, incMatrix R G a_1 s(a, b) = ↑2

Tactic:
← card_pair h.ne

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1, incMatrix R G a_1 s(a, b) = ↑(#{a, b})
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = if e ∈ G.edgeSet then 2 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 2

case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(G.degree i) = ∑ j, if G.Adj i j then 1 else 0

Tactic:
unfold degree neighborFinset neighborSet
  rw [sum_boole, Set.toFinset_ofPred]

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

Goal state before:
pp: case neg.inl.inr.inl
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
hnadj : ¬G'.Adj v w'
hu' : ∀ (u' : V), u' ≠ v → G.Adj w' u' → G'.Adj w' u'
hx' : ∀ (x' : V), x' ≠ w' → G.Adj x' v → G'.Adj x' v
hadj : ¬G.Adj v w'
h2 : (v = v ∧ w' = w' ∨ v = w' ∧ w' = v) ∧ v ≠ w'
⊢ G'.Adj v w

pp: case neg.inl.inr.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
h2r1 : v = x
h2r2 : w' = u
⊢ G'.Adj v w

Tactic:
· exact (hx' _ hww' hl.symm).symm

Goal state after:
case neg.inl.inr.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
h2r1 : v = x
h2r2 : w' = u
⊢ G'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2

Tactic:
compl_neighborFinset_sdiff_inter_eq

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : 0 < n
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ

Tactic:
let := Classical.decEq V

Goal state after:
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : 0 < n
this : DecidableEq V := Classical.decEq V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ ∀ a ∈ G.neighborFinset v, #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) a) = k - ℓ - 1

pp: case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ ∀ b ∈ Gᶜ.neighborFinset v, #(bipartiteBelow G.Adj (G.neighborFinset v) b) = μ

Tactic:
· intro w hw
    rw [mem_neighborFinset] at hw
    simp_rw [bipartiteAbove, ← mem_neighborFinset, filter_mem_eq_inter]
    have s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v := by
      rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
      exact ⟨hw.symm, G.notMem_neighborFinset_self v⟩
    rw [inter_comm, neighborFinset_compl, ← inter_sdiff_assoc, ← sdiff_eq_inter_compl,
      card_sdiff_of_subset s, card_singleton, ← sdiff_inter_self_left,
      card_sdiff_of_subset inter_subset_left]
    congr
    · simp [h.regular w]
    · simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw,
        ← Set.toFinset_card]
      congr!

Goal state after:
case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ ∀ b ∈ Gᶜ.neighborFinset v, #(bipartiteBelow G.Adj (G.neighborFinset v) b) = μ
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + if decide (x = u✝ ∨ x = v✝) = true then 1 else 0) ↔
    ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
split_ifs with h

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : ¬decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝
Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
let hd := Set.disjoint_of_subset_left ht.1 h

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
hd : Disjoint t s := Set.disjoint_of_subset_left ht.left h
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum = 0 ↔ G = ⊥

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
h : G.vertexCoverNum = 0
⊢ G = ⊥
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: case refine_1
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ (completeGraph V).vertexCoverNum
⊢ ↑n ≤ ENat.card V - 1

pp: case refine_2
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
⊢ ↑n ≤ (completeGraph V).vertexCoverNum

Tactic:
· grw [hn, vertexCoverNum_le_card_sub_one]

Goal state after:
case refine_2
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
⊢ ↑n ≤ (completeGraph V).vertexCoverNum
Module: Mathlib.Combinatorics.Young.YoungDiagram

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

Tactic:
rw [← transpose_transpose μ] at h

Goal state after:
μ ν : YoungDiagram
h : μ.transpose.transpose ≤ ν
⊢ μ.transpose ≤ ν.transpose
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = m.psub n

Tactic:
split_ifs with h

Goal state after:
case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n

case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₁ o₂ : Option α
⊢ (Option.casesOn (o₁, o₂).1 (o₁, o₂).2 fun b ↦ ((o₁, o₂), b).1.1) = (fun x1 x2 ↦ x1 <|> x2) (o₁, o₂).1 (o₁, o₂).2

Tactic:
cases o₁ <;> cases o₂

Goal state after:
case none.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
⊢ (Option.casesOn (none, none).1 (none, none).2 fun b ↦ ((none, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, none).1 (none, none).2

case none.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (none, some val✝).1 (none, some val✝).2 fun b ↦ ((none, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, some val✝).1 (none, some val✝).2

case some.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (some val✝, none).1 (some val✝, none).2 fun b ↦ ((some val✝, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, none).1 (some val✝, none).2

case some.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝¹ val✝ : α
⊢ (Option.casesOn (some val✝¹, some val✝).1 (some val✝¹, some val✝).2 fun b ↦ ((some val✝¹, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝¹, some val✝).1 (some val✝¹, some val✝).2
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + 1 + m

Tactic:
Nat.add_right_comm

Goal state after:
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + m + 1
Module: Mathlib.Computability.Partrec

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec₂ fun L b ↦ filterMap (Option.guard fun a ↦ decide (R a b)) L

Tactic:
refine listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ PrimrecPred fun p ↦ (fun a ↦ decide (R a p.1.2)) p.2 = true

case refine_2
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec fun p ↦ some p.2
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun L b ↦ ∃ a ∈ L, R a b

Tactic:
by
  classical
  have h (L) (b) : (List.filter (R · b) L).length ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
  refine .of_eq (.not ?_) h
  exact Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_1.succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
      Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s)
        n✝ ∨
    ∃ b_1,
      Sum.inr b_1 ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s) n✝ ∧
        Sum.inl b ∈ f b_1
c : α
hc : Sum.inr c ∈ F a n✝
⊢ b ∈ f.fix a

Tactic:
specialize this _ _ hc

Goal state after:
case refine_1.succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
      Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s)
        n✝ ∨
    ∃ b_1,
      Sum.inr b_1 ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s) n✝ ∧
        Sum.inl b ∈ f b_1
c : α
this : b ∈ f.fix c → b ∈ f.fix a
hc : Sum.inr c ∈ F a n✝
⊢ b ∈ f.fix a
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
n : ℕ
IH : Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
⊢ (if n + 1 < (n.sqrt + 1) * (n.sqrt + 1) then n.sqrt else n.sqrt + 1) = (n + 1).sqrt

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
IH : Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
h : n + 1 < (n.sqrt + 1) * (n.sqrt + 1)
⊢ n.sqrt = (n + 1).sqrt

case neg
n : ℕ
IH : Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
h : ¬n + 1 < (n.sqrt + 1) * (n.sqrt + 1)
⊢ n.sqrt + 1 = (n + 1).sqrt
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ Tendsto (r i) atTop atTop

Tactic:
by
  rw [tendsto_atTop]
  intro b
  have := R.eventually_r_ge b
  rw [Filter.eventually_all] at this
  exact_mod_cast this i

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)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ 1 * ↑n = ↑n

Tactic:
by rw [one_mul]

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ (b : ℝ), n₀ ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (2 ^ n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (2 ^ n * max n₀ 2) (2 ^ (n + 1) * max n₀ 2), f z = f (max n₀ 2)

Tactic:
intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∑ i, a i * b i ^ p a b = 1

Tactic:
simp only [p]
  exact Function.invFun_eq (by rw [← Set.mem_range]; exact R.one_mem_range_sumCoeffsExp)

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)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ 1 * ↑n = ↑n

Tactic:
by rw [one_mul]

Goal state after: