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

Goal state before:
pp: case neg
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
refine ⟨univ.map ⟨fun i ↦ univ.map ⟨fun j ↦ f (i, j), fun _ _ h ↦ ?_⟩, fun i₁ i₂ h ↦ ?_⟩,
      ?_, fun h ↦ ?_, fun _ h₁ _ h₂ hne _ h₁' _ h₂' ↦ ?_⟩
    · simpa using f.injective h
    · simp_rw [Finset.ext_iff] at h
      have : NeZero t := ⟨ht⟩
      obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)
      apply f.injective at heq
      rw [Prod.mk.injEq] at heq
      exact heq.left
    · simp
    · simp_rw [mem_map, mem_univ, Embedding.coeFn_mk, true_and] at h
      replace ⟨_, h⟩ := h
      simp [← h]
    · simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁ h₂
      replace ⟨_, h₁⟩ := h₁
      replace ⟨_, h₂⟩ := h₂
      rw [← h₁] at h₁'
      rw [← h₂] at h₂'
      simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁' h₂'
      replace ⟨_, h₁'⟩ := h₁'
      replace ⟨_, h₂'⟩ := h₂'
      rw [← h₁', ← h₂']
      apply f.toHom.map_adj
      simp_rw [completeEquipartiteGraph_adj]
      contrapose hne with heq
      simp_rw [← h₁, ← h₂, heq]

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

Goal state before:
pp: case neg.refine_1
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
⊢ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

pp: case neg.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)

Tactic:
· obtain ⟨parts, hparts_sub, hparts_card⟩ := K'.parts.exists_subset_card_eq (Nat.pred_le _)
      let K : G.CompleteEquipartiteSubgraph r t := by
        refine ⟨parts, ?_, fun h ↦ K'.card_mem_parts (hparts_sub h),
          fun _ h₁ _ h₂ hne ↦ K'.isCompleteBetween (hparts_sub h₁) (hparts_sub h₂) hne⟩
        rw [hparts_card, K'.card_parts.resolve_right ht]
        exact .inl (Nat.pred_succ r)
      obtain ⟨s, nhs_mem, hs⟩ : ∃ s ∉ K.parts, insert s K.parts = K'.parts := by
        refine exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩
        rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]
      have hs_mem : s ∈ K'.parts := by simp [← hs]
      exact ⟨K, s, K'.card_mem_parts hs_mem,
        fun _ h ↦ K'.isCompleteBetween (hparts_sub h) hs_mem (ne_of_mem_of_not_mem h nhs_mem)⟩

Goal state after:
case neg.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
⊢ False

Tactic:
let Ddis := D.disjoint_right

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑(K ∪ Cfin.toFinset) ↑D := ComponentCompl.disjoint_right D
⊢ False
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
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
⊢ zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
let K := completeBipartiteGraph (Fin s) (Fin t)

Goal state after:
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
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
⊢ zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
| (n + 1) * extremalNumber n H

Tactic:
rw [← Fintype.card_fin (n + 1), ← card_univ]

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
| #univ * extremalNumber n H
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
⊢ AntitoneOn (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) (Set.Ici 2)

Tactic:
apply antitoneOn_nat_Ici_of_succ_le
  intro n hn
  conv_lhs =>
    enter [1, 1]
    rw [← Fintype.card_fin (n + 1)]
  rw [div_le_iff₀ (mod_cast Nat.choose_pos (by linarith)),
    extremalNumber_le_iff_of_nonneg H (by positivity)]
  intro G _ h
  rw [mul_comm, ← mul_div_assoc, le_div_iff₀' (mod_cast Nat.choose_pos hn), Nat.cast_choose_two,
    Nat.cast_choose_two, Nat.cast_add_one, add_sub_cancel_right (n : ℝ) 1,
    mul_comm _ (n - 1 : ℝ), ← mul_div (n - 1 : ℝ), mul_comm _ (n / 2 : ℝ), mul_assoc,
    mul_comm (n - 1 : ℝ), ← mul_div (n + 1 : ℝ), mul_comm _ (n / 2 : ℝ), mul_assoc,
    mul_le_mul_iff_right₀ (by positivity), ← Nat.cast_pred (by positivity), ← Nat.cast_mul,
    ← Nat.cast_add_one, ← Nat.cast_mul, Nat.cast_le]
  conv_rhs =>
    rw [← Fintype.card_fin (n + 1), ← card_univ]
  -- double counting `(v, e) ↦ v ∉ e`
  apply card_nsmul_le_card_nsmul' (r := fun v e ↦ v ∉ e)
  -- counting `e`
  · intro e he
    simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]
  -- counting `v`
  · intro v hv
    simpa [edgeFinset_deleteIncidenceSet_eq_filter]
      using! card_edgeFinset_deleteIncidenceSet_le_extremalNumber h v

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst✝¹ : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ↑(#(G.overFin ⋯).edgeFinset) ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H ⊑ G.overFin ⋯

Tactic:
apply Nat.find_spec <| eventually_atTop.mp <| eventually_isContained_of_card_edgeFinset H hε_pos

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst✝¹ : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ Nat.find ⋯ ≤ Fintype.card V
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ univ), (s i).encard

Tactic:
← finite_univ.encard_biUnion (fun a _ b _ hab ↦ hs hab)

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).encard = (⋃ i ∈ univ, s i).encard
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
⊢ #s = r

Tactic:
simp [← Nat.succ_inj, ← hw.isNClique_left.2, hw.notMem_left]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
e : Sym2 α
he : G.IsBridge e
⊢ ¬G.IsHamiltonian

Tactic:
induction e with | 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
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
⊢ y = w'

Tactic:
obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩)

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
⊢ y = w'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsCycles

Tactic:
intro v
  obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
  obtain ⟨w', hw'⟩ := hM'.1 (hM'.2 v)
  simp only [symmDiff_def, Set.ncard_eq_two, ne_eq, imp_iff_not_or, Set.not_nonempty_iff_eq_empty,
    Set.eq_empty_iff_forall_notMem, SimpleGraph.mem_neighborSet, SimpleGraph.sup_adj, sdiff_adj,
    spanningCoe_adj, not_or, not_and, not_not]
  by_cases hww' : w = w'
  · simp_all [← imp_iff_not_or]
  · right
    use w, w'
    aesop

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
this : Fintype ↑P.parts
⊢ G.Colorable n

Tactic:
rw [Set.Finite.card_toFinset hf] at hc

Goal state after:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
this : Fintype ↑P.parts
hc : Fintype.card ↑P.parts ≤ n
⊢ G.Colorable n
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 : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
u : V
⊢ u = w ∨ u = v → ¬G.Adj v u ∧ ¬G.Adj w u

Tactic:
rintro (rfl | rfl)

Goal state after:
case inl
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v u : V
ha : v ≠ u ∧ ¬G.Adj v u
hne : v ≠ u
⊢ ¬G.Adj v u ∧ ¬G.Adj u u

case inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
w u : V
ha : u ≠ w ∧ ¬G.Adj u w
hne : u ≠ w
⊢ ¬G.Adj u u ∧ ¬G.Adj w u
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 v ∩ G.neighborFinset w) = k - ℓ - 1

Tactic:
inter_comm,

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) = k - ℓ - 1
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3.e_a.e_a
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) = ℓ

Tactic:
inter_comm,

Goal state after:
case convert_3.e_a.e_a
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 v ∩ G.neighborFinset w) = ℓ
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w' : V
hw' : y ≠ w' ∧ G'.Adj v w'
⊢ M.Adj v y ↔ ¬M.Adj v w'

Tactic:
simpa using hG' hw'.1 hr.1 hw'.2

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w✝⁴ w✝³ w✝² : α
w✝¹ w✝ : Finset α
hw : H.IsFiveWheelLike (r + 1) k w✝⁴ w✝³ w✝² w✝¹ w✝
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (?m.355 + 2).succ * ((2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)) * (3 * r + 4).succ ≤
    (?m.355 + 2).succ * ((3 * r + 2) * ‖α‖)

Tactic:
mul_comm (2 * r + 2 + k + 3),

Goal state after:
α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w✝⁴ w✝³ w✝² : α
w✝¹ w✝ : Finset α
hw : H.IsFiveWheelLike (r + 1) k w✝⁴ w✝³ w✝² w✝¹ w✝
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (2 * r + 2 + k + 3) * (3 * r + 4).succ ≤
    (2 * r + 2 + k + 2).succ * ((3 * r + 2) * ‖α‖)
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover ∅ ↔ G = ⊥

Tactic:
by
  simp [IsVertexCover, eq_bot_iff_forall_not_adj]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
a✝ : Nontrivial V
x : V
n : ℕ
hn : ↑n ≤ G.vertexCoverNum
⊢ ↑n ≤ ENat.card V - 1

Tactic:
simp only [vertexCoverNum, le_iInf_iff] at hn

Goal state after:
V : Type u_1
G : SimpleGraph V
a✝ : Nontrivial V
x : V
n : ℕ
hn : ∀ (i : Set V), G.IsVertexCover i → ↑n ≤ i.encard
⊢ ↑n ≤ ENat.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ G.vertexCoverNum + 1 ≤ ENat.card V

Tactic:
grw [vertexCoverNum_le_card_sub_one, ENat.card_eq_coe_natCard]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ ↑(Nat.card V) - 1 + 1 ≤ ↑(Nat.card V)
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ↑n ≤ G.vertexCoverNum
⊢ ↑n ≤ G.edgeSet.encard

Tactic:
simp only [vertexCoverNum, le_iInf_iff] at hn

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V), G.IsVertexCover i → ↑n ≤ i.encard
⊢ ↑n ≤ G.edgeSet.encard
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
⊢ μ.transpose = ν.transpose ↔ μ = ν

Tactic:
by
  rw [transpose_eq_iff_eq_transpose]
  simp

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

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ ⟦Quotient.out pt₁.groupElts⟧ = pt₁.groupElts

Tactic:
Quotient.out_eq

Goal state after:
case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ pt₁.groupElts = pt₁.groupElts
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
h : pt₁ = pt₂
⊢ pt₁.index = pt₂.index ∧ ∃ g, ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts

Tactic:
subst h
    simp only [and_self, true_and]
    refine ⟨pt₁.groupElts.out, ?_⟩
    rw [Quotient.out_eq]

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

Goal state before:

Tactic:
j1 ≤ j2 := hj
      _ < w[i2] := h2
      _ ≤ w[i1] := by
        obtain rfl | h := eq_or_lt_of_le hi
        · rfl
        · exact hw.getElem_ge_getElem_of_le h.le

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

Goal state before:
pp: R : ℕ → ℕ → Prop
s : ℕ
inst✝ : DecidableRel R
hf : PrimrecRel R
⊢ Primrec fun n ↦ filterMap (Option.guard fun y ↦ decide (R y n)) (range s)

Tactic:
refine listFilterMap (.const (range s)) ?_

Goal state after:
R : ℕ → ℕ → Prop
s : ℕ
inst✝ : DecidableRel R
hf : PrimrecRel R
⊢ Primrec₂ fun n ↦ Option.guard fun y ↦ decide (R y n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case pair
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
n : ℕ
⊢ (fun n ↦ pair (f n) (g n)) n < ack (max a b + 3) n

Tactic:
calc
      pair (f n) (g n) < (max (f n) (g n) + 1) ^ 2 := pair_lt_max_add_one_sq ..
      _ ≤ (ack (max a b) n + 1) ^ 2 := by rw [max_ack_left]; gcongr; exacts [(ha n).le, (hb n).le]
      _ ≤ ack (max a b + 3) n := ack_add_one_sq_lt_ack_add_three ..

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

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

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx
    rw [deriv_fun_mul]
    · exact differentiableAt_rpow_const_of_ne _ (by positivity)
    · exact differentiableAt_one_sub_smoothingFn hx

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

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
⊢ (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ |f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : 0 ≤ f x
hx₂ : 0 ≤ g x
⊢ f x * g x = |f x| * |g x|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
⊢ (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ -|f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
x : ℝ
hx₁ : 0 ≤ f x
hx₂ : g x ≤ 0
⊢ f x * g x = -|f x| * |g x|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
⊢ (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ -|f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : f x ≤ 0
hx₂ : 0 ≤ g x
⊢ f x * g x = -|f x| * |g x|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
⊢ (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ |f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
x : ℝ
hx₁ : f x ≤ 0
hx₂ : g x ≤ 0
⊢ f x * g x = |f x| * |g x|
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a : ℕ
⊢ (cf.prec cg).eval (Nat.pair a 0) = cf.eval a

Tactic:
by
  rw [eval, Nat.unpaired, Nat.unpair_pair]
  rw [Nat.rec_zero]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.refine_2
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m y))

Tactic:
· exact hg _ _ h₂

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'.succ
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
use (max k₁ k₂).succ

Goal state after:
case h
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
    ∃ a,
      evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)