mathlib-initiative/mathlib-tactics huggingface dataset:
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) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)

Tactic:
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))
  rw [Nat.sub_add_cancel, ← Set.toFinset_card]
  · simp [commonNeighbors, ← neighborFinset_def, Finset.card_union_add_card_inter,
      h.regular.degree_eq, two_mul]
  · apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
    simp [h.regular.degree_eq, two_mul]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
have bdX := sum_degree_le_of_le_not_adj xcle (fun _ _ ↦ Nat.zero_le _)

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #Xᶜ * (#(s ∩ t) - 1) + #Xᶜᶜ * (#(s ∩ t) - 0)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)
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 w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w ∩ ((G.neighborFinset v)ᶜ \ {v})) = k - ℓ - 1

Tactic:
← inter_sdiff_assoc,

Goal state after:
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 w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #((G.neighborFinset w ∩ (G.neighborFinset v)ᶜ) \ {v}) = k - ℓ - 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

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

Tactic:
exact .inl (K.card_parts.resolve_right ht'_pos.ne')

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

Goal state before:
pp: case refine_4
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
v w : V
hvw : (edge x a).Adj v w
⊢ (G ⊔ edge a c).Adj v w

Tactic:
· simpa [edge_adj, adj_congr_of_sym2 _ ((adj_edge _ _).mp hvw).1.symm] using .inl hgadj

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

Goal state before:
pp: case intro.refine_2
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val✝ : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ (M ⊔ M').IsSpanning

Tactic:
· rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self

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

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
pt : PlacedTile ps
h : ∀ (i : ιₚ) (gx : G), ppt { index := i, groupElts := ↑gx }
⊢ ppt pt

Tactic:
rcases pt with ⟨i, gx⟩

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
h : ∀ (i : ιₚ) (gx : G), ppt { index := i, groupElts := ↑gx }
i : ιₚ
gx : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i)).subtype (↑ps i).symmetries
⊢ ppt { index := i, groupElts := gx }
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

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

Tactic:
apply hs_subset at hw'_mem

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

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
⊢ Option.map Prod.snd (graph b (m b + 1))[0]? = some (f b)

Tactic:
by
    have graph_eq_map_bindList (i : ℕ) (hi : i ≤ m b + 1) :
        graph b i = (bindList b (m b + 1 - i)).map fun x ↦ (x, f x) := by
      have bindList_eq_nil : bindList b (m b + 1) = [] :=
        have bindList_m_lt (k : ℕ) : ∀ b' ∈ bindList b k, m b' < m b + 1 - k := by
          induction k with simp [bindList]
          | succ k ih =>
            grind
        List.eq_nil_iff_forall_not_mem.mpr
          (by intro b' ha'; by_contra; simpa using bindList_m_lt (m b + 1) b' ha')
      have mapGraph_graph {bs bs' : List β} (has : bs' ⊆ bs) :
          mapGraph (bs.map <| fun x => (x, f x)) bs' = bs'.map f := by
        induction bs' with simp [mapGraph]
        | cons b bs' ih =>
          have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has
          rcases this with ⟨ha, has'⟩
          simpa [List.lookup_graph f ha] using ih has'
      have graph_succ : ∀ i, graph b (i + 1) =
        (bindList b (m b - i)).filterMap fun b' =>
          (g b' <| mapGraph (graph b i) (l b')).map (b', ·) := fun _ => rfl
      have bindList_succ : ∀ i, bindList b (i + 1) = (bindList b i).flatMap l := fun _ => rfl
      induction i with
      | zero => symm; simpa [graph] using bindList_eq_nil
      | succ i ih =>
        simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.le_of_lt_succ hi),
          Nat.succ_eq_add_one, bindList_succ, Nat.reduceSubDiff]
        apply List.filterMap_eq_map_iff_forall_eq_some.mpr
        intro b' ha'; simp; rw [mapGraph_graph]
        · exact H b'
        · exact (List.infix_flatMap_of_mem ha' l).subset
    simp [graph_eq_map_bindList (m b + 1) (Nat.le_refl _), bindList]

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

Goal state before:
pp: case zero
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec fun x ↦ 0

Tactic:
exact .const 0

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

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ IH + 1) 0 = 0 + v.tail.head

Tactic:
simp [*, Nat.succ_add]

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

Goal state before:
pp: case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec v.tail.head (fun y IH ↦ IH + 1) n✝ = n✝ + v.tail.head
⊢ Nat.rec v.tail.head (fun y IH ↦ IH + 1) (n✝ + 1) = n✝ + 1 + v.tail.head

Tactic:
simp [*, Nat.succ_add]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
G' : SimpleGraph V
| G'.Adj x x'

Tactic:
adj_comm

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
G' : SimpleGraph V
| G'.Adj x' x
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v ↦ (unpair (f v)).2

Tactic:
have s := sqrt.comp₁ _ hf
  have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)
  refine (if_lt fss s s (sub.comp₂ _ fss s)).of_eq fun v => ?_
  simp [Nat.unpair]; split_ifs <;> rfl

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
⊢ (∃ M, M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u

Tactic:
refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
  contrapose!
  intro h
  by_cases hvOdd : Odd (Nat.card V)
  · exact ⟨∅, .empty hvOdd⟩
  · exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
hf' : 0 ≤ᶠ[atTop] f
hg' : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
⊢ max c₂ c₄ > 0

Tactic:
by change 0 < max c₂ c₄; 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
⊢ f x + g x ≤ f x + ‖g x‖

Tactic:
gcongr; exact le_norm_self (g x)

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
⊢ f x + g x ≤ f x + ‖g x‖

Tactic:
gcongr; exact le_norm_self (g x)

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
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * ↑n * (1 - c₃) * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1)) =
    ↑n ^ p a b * ↑n * (1 - c₃) * (c₂ * g ↑n / (c₁ ^ (p a b + 1) * ↑n ^ (p a b + 1)))

Tactic:
by
          rw [Real.mul_rpow (by positivity) (by positivity)]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
n x : ℕ
h : x = 0
⊢ (∃ x, n ≤ x) ∧ 0 = x

Tactic:
| _ =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
n x : ℕ
h : x = n + 1
⊢ (∃ x, n ≤ x) ∧ n + 1 = x

Tactic:
| _ =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case left
n x : ℕ
h : x = (unpair n).1
⊢ (∃ x, n ≤ x) ∧ (unpair n).1 = x

Tactic:
| _ =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case right
n x : ℕ
h : x = (unpair n).2
⊢ (∃ x, n ≤ x) ∧ (unpair n).2 = x

Tactic:
| _ =>

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ n * l * m ≤ m

Tactic:
mul_assoc,

Goal state after:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ n * (l * m) ≤ m
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 * m ^ n✝ * n ≤ m * l + n

Tactic:
mul_assoc,

Goal state after:
case a.succ
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n✝ : ℕ
ih : m ^ n✝ * n ≤ l
⊢ m * (m ^ n✝ * n) ≤ m * l + n
Module: Mathlib.Computability.ContextFreeGrammar

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

Tactic:
rintro ⟨p, q, rfl, rfl⟩; apply rewrites_of_exists_parts

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : r.Rewrites u v
p : List (Symbol T N)
⊢ r.Rewrites (p ++ u) (p ++ v)

Tactic:
rewrites_iff

Goal state after:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : r.Rewrites u v
p : List (Symbol T N)
⊢ r.Rewrites (u ++ p) (v ++ p)

Tactic:
rewrites_iff

Goal state after:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
⊢ binaryRec z f n = ⋯ ▸ f n.bodd n.div2 (binaryRec z f n.div2)

Tactic:
rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]

Goal state after:
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
⊢ cast ⋯ (f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))) = cast ⋯ (f n.bodd n.div2 (binaryRec z f n.div2))
Module: Mathlib.Computability.DFA

Goal state before:
pp: T : Type u
L : Language T
h : L.IsRegular
σ : Type
w✝ : Fintype σ
M : DFA T σ
hM : M.accepts = L
⊢ Mᶜ.accepts = Lᶜ

Tactic:
simp [hM]

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

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)

Tactic:
have hc₁p : 0 < c₁ ^ p := Real.rpow_pos_of_pos hc₁_mem _

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)