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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
u v : V ⊕ W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) u) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj u v

Tactic:
cases u <;> cases v

Goal state after:
case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val✝¹ val✝ : V
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val✝¹ : V
val✝ : W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val✝¹ : W
val✝ : V
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val✝¹ val✝ : W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inr w₂)

Tactic:
exact ((hH w₁ w₂).map Embedding.sumInr.toHom).mono le_sup_left

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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
u v : V ⊕ W
huv : (G ⊕g H).Adj u v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) u) (Sum.elim (⇑cG) (⇑cH) v)

Tactic:
cases u <;> cases v

Goal state after:
case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : V
val✝ : W
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))

case inr.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u v : V
p : (sSup Hs).Walk u v
⊢ ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet

Tactic:
by
  induction p with
  | nil => exact ⟨hHs.some, hHs.some_mem, by simp⟩
  | @cons u v w h_adj p ih =>
    obtain ⟨H₁, hH₁, ih⟩ := ih
    obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
    obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
    simpa using ⟨H, hH, (le_iff_adj.mp h₂) _ _ h_adj, fun a ha => edgeSet_mono h₁ (ih a ha)⟩

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

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝ : ∃ G, p G
G : SimpleGraph V
hp : p G
⊢ ?m.66

Tactic:
by
    apply exists_max_image { G | p G } (#·.edgeFinset)
    use G, by simpa using hp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (Fintype.card V - 1) H

Tactic:
rw [← card_edgeFinset_induce_compl_singleton, ← @card_unique ({v} : Set V), ← card_compl_set]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ #(induce {v}ᶜ G).edgeFinset ≤ extremalNumber (Fintype.card ↑{v}ᶜ) H
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
e : Sym2 V
he : e ∈ G.edgeSet
⊢ C ⟨e, he⟩ = C' ⟨e, he⟩

Tactic:
induction e using Sym2.inductionOn

Goal state after:
case hf
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
x✝ y✝ : V
he : s(x✝, y✝) ∈ G.edgeSet
⊢ C ⟨s(x✝, y✝), he⟩ = C' ⟨s(x✝, y✝), he⟩
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ (p.concat hadj).length

Tactic:
p.length_concat

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ p.length + 1
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'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| (#K.parts - #{p}) * t'

Tactic:
← Finset.card_sdiff_of_subset (singleton_subset_iff.mpr hp),

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| #(K.parts \ {p}) * t'
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he

Goal state after:
α : Type u_1
s : Set α
he : Even s.ncard
t u : Set α
hutu : t ∪ u = s
hdtu : Disjoint t u
hctu : #↑t = #↑u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ incMatrix R G a e = (G.incidenceSet a).indicator 1 e

Tactic:
simp [incMatrix, Set.indicator]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.Adj v w
hvv' : H.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
exact halt hww' hvw.adj_sub hvv'.adj_sub

Goal state after:
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
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + #(G.commonNeighbors v w).toFinset = 2 * k

pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k

Tactic:
· simp [commonNeighbors, ← neighborFinset_def, Finset.card_union_add_card_inter,
      h.regular.degree_eq, two_mul]

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
⊢ Disjoint M1.verts (⋃ i, (complMatch i).verts)

Tactic:
Set.disjoint_iUnion_right

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
⊢ ∀ (i : G.deleteUniversalVerts.coe.ConnectedComponent), Disjoint M1.verts (complMatch i).verts
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
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
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
have hcycles := Subgraph.IsPerfectMatching.symmDiff_isCycles hM1 hM2

Goal state after:
case neg
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
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
x : ℕ
hx : x ∈ μ.rowLens
⊢ 0 < x

Tactic:
by
  rw [rowLens, List.mem_map] at hx
  obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx
  rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi

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

Goal state before:
pp: μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : T.entry = T'.entry
⊢ T = T'

Tactic:
cases T

Goal state after:
case mk
μ : YoungDiagram
T' : SemistandardYoungTableau μ
entry✝ : ℕ → ℕ → ℕ
row_weak'✝ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝ i j1 ≤ entry✝ i j2
col_strict'✝ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝ i1 j < entry✝ i2 j
zeros'✝ : ∀ {i j : ℕ}, (i, j) ∉ μ → entry✝ i j = 0
h : { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }.entry = T'.entry
⊢ { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ } = T'
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
b : β
⊢ (bif (encode (Sum.inl b)).bodd then Option.map (h a) (decode (encode (Sum.inl b)).div2)
    else Option.map (g a) (decode (encode (Sum.inl b)).div2)) =
    some (Sum.casesOn (Sum.inl b) (g a) (h a))

Tactic:
simp [Nat.div2_val, encodek]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
c : γ
⊢ (bif (encode (Sum.inr c)).bodd then Option.map (h a) (decode (encode (Sum.inr c)).div2)
    else Option.map (g a) (decode (encode (Sum.inr c)).div2)) =
    some (Sum.casesOn (Sum.inr c) (g a) (h a))

Tactic:
simp [Nat.div2_val, encodek]

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

Goal state before:
pp: ⊢ Primrec' fun v ↦ v.head - v.tail.head

Tactic:
have : @Primrec' 2 fun v ↦ (fun a b ↦ b - a) v.head v.tail.head := by
    refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_
    simp; induction v.head <;> simp [*, Nat.sub_add_eq]
  simpa using comp₂ (fun a b => b - a) this (tail head) head

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

Goal state before:
pp: H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
x y : ℕ
⊢ ℕ

Tactic:
exact if x.succ < y.succ * y.succ then y else y.succ

Goal state after:
Module: Mathlib.Computability.Ackermann

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

Tactic:
by
    rw [ack_succ_succ, ack_succ_succ]
    exact
      (ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans
        (ack_strictMono_right _ <| ack_strict_mono_left' n h)

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 - ε z) + z ^ (p - 1) / log z ^ 2) ~[atTop] fun z ↦ p * z ^ (p - 1)

Tactic:
refine IsEquivalent.add_isLittleO ?one ?two

Goal state after:
case one
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 - ε z)) ~[atTop] fun z ↦ p * z ^ (p - 1)

case two
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) / log z ^ 2) =o[atTop] fun z ↦ p * z ^ (p - 1)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / log z ^ 2) ~[atTop] fun z ↦ p * z ^ (p - 1)

Tactic:
refine IsEquivalent.add_isLittleO ?one ?two

Goal state after:
case one
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z ↦ p * z ^ (p - 1)

case two
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z ↦ p * z ^ (p - 1)
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
C : ℝ
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ ↑(r i n)

Tactic:
obtain ⟨c, hc_mem, hc⟩ := R.exists_eventually_const_mul_le_r

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
C c : ℝ
hc_mem : c ∈ Set.Ioo 0 1
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ ↑(r i n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < T n

Tactic:
R.h_rec n hn

Goal state after:
case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < ∑ i, a i * T (r i n) + g ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (deriv fun x ↦ 1 - ε x) =ᶠ[atTop] -deriv ε

Tactic:
by
      filter_upwards [eventually_gt_atTop 1] with x hx; rw [deriv_fun_sub] <;> aesop

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

Goal state before:
pp: ⊢ (deriv fun x ↦ 1 - ε x) =ᶠ[atTop] fun z ↦ -deriv ε z

Tactic:
by
      filter_upwards [eventually_gt_atTop 1] with x hx; rw [deriv_fun_sub] <;> aesop

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 : α
⊢ (fun n ↦ -log (b i) * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ 1 / log ↑n ^ 2

Tactic:
by
      have : -log (b i) ≠ 0 := by
        rw [neg_ne_zero]
        exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)
      rw [← isTheta_const_mul_right this]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2
c : Code
⊢ Nat.Partrec c.eval

Tactic:
induction c with

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 + 1 / 2 * f u

Tactic:
by
                  rw [sub_eq_add_neg]
                  gcongr
                  refine le_of_neg_le_neg ?_
                  rwa [neg_neg, ← neg_mul, ← neg_div]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.zero
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ n ≤ n + m * l

Tactic:
exact le_self_add

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.succ
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n✝ : ℕ
ih : m ^ n✝ * n ≤ l
⊢ m * l ≤ m * l + n

Tactic:
exact le_self_add

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ (comap f M).eval x = M.eval (List.map f x)

Tactic:
by
  simp [eval]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
x : List α
⊢ ((reindex g) M).eval x = g (M.eval x)

Tactic:
by
  simp [eval]

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

Goal state before:
pp: case neg
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
    refine ⟨k + 1, ⟨by rw [testBit_bit_succ, hk], fun j hj => ?_⟩⟩
    obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)
    exact (testBit_bit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: n : Num
⊢ decodeNum (encodeNum n) = n

Tactic:
obtain - | n := n <;> unfold encodeNum decodeNum

Goal state after:
case zero
⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero

case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
⊢ (fun x ↦ a :: x) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.stepSet S a)

Tactic:
by
  ext x; simp [cons_mem_acceptsFrom M]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
a : α
⊢ M.eval (x ++ [a]) = M.stepSet (M.eval x) a

Tactic:
by
  simp [eval]

Goal state after: