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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
⊢ ∃ a b c d,
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s

Tactic:
obtain ⟨b, hb, hbj⟩ := hw.isNClique_snd_right.exists_not_adj_of_cliqueFree_succ hcf x

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
b : α
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
⊢ ∃ a b c d,
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

Tactic:
by
  by_cases! h : IsEmpty α
  · exact h.elim' a
  refine ⟨fun h ↦ ⟨h.isPath, h.length_eq⟩, fun ⟨hp, h⟩ ↦ ?_⟩
  have := p.isPath_iff_injective_get_support.mp hp
  refine isHamiltonian_iff_support_get_bijective.mpr ⟨this, this.surjective_of_finite ?_⟩
  refine (Fintype.equivFinOfCardEq ?_).symm
  simp_rw [length_support, h, Nat.sub_one_add_one Fintype.card_ne_zero]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ {v w : V}, ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) → G.Adj v w

Tactic:
by
      intro v w h
      obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h
      · exact hadj ⟨v, _⟩
      · exact (hadj ⟨w, _⟩).symm

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ ↑(#{x | x ∈ G.incidenceSet a ∩ G.incidenceSet b}) = 1

Tactic:
convert! @Nat.cast_one R _

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ #{x | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = 1
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
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
⊢ y = w'

Tactic:
simp_rw [← SimpleGraph.mem_neighborSet] at *

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
Subgraph.adj_comm,

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ p.toSubgraph.Adj (p.getVert n) v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
⊢ G.Adj w v ∧ ¬p.toSubgraph.Adj w v

Tactic:
exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩

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

Goal state before:
pp: case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
⊢ ∑ i, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i = x

Tactic:
ext j

Goal state after:
case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ i, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i) j = ↑x j
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
⊢ ∀ v ∈ p.toSubgraph.verts, ∀ (w : V), G.Adj v w → p.toSubgraph.Adj v w

Tactic:
by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      have : (G.neighborSet v).Nonempty := by
        rw [Walk.mem_verts_toSubgraph] at hv
        refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)
        rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]
        lia
      refine @Classical.ofNonempty _ ?_
      rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(s ∩ t) + 1 = k + 1

Tactic:
hw.card_inter

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ k + 1 = 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) = k

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:
· simp [h.regular w]

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 w ∩ G.neighborFinset v) = ℓ
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})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + (k + 3)) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w

Tactic:
add_comm k,

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) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + (3 + k)) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.degree x = List.countP (fun e ↦ decide (x ∈ e)) p.edges

Tactic:
rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).card = (Multiset.filter (fun e ↦ x ∈ e) ↑p.edges).card
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_4
ε : ℝ
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
p₁✝ p₂ : Finset (Fin n)
hne : p₁✝ ≠ p₂
v₁ : Fin n
hv₁ : v₁ ∈ ↑p₁✝
v₂ : Fin n
hv₂ : v₂ ∈ ↑p₂
hp₂ : ∃ a, ∃ (h : a ∈ K.parts), y a ⋯ = p₂
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ K.parts
hyp₁ : y p₁ ⋯ = p₁✝
⊢ G.Adj v₁ v₂

Tactic:
rw [← hyp₁] at hv₁ hne

Goal state after:
case refine_4
ε : ℝ
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
p₁✝ p₂ : Finset (Fin n)
v₁ v₂ : Fin n
hv₂ : v₂ ∈ ↑p₂
hp₂ : ∃ a, ∃ (h : a ∈ K.parts), y a ⋯ = p₂
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ K.parts
hne : y p₁ ⋯ ≠ p₂
hv₁ : v₁ ∈ ↑(y p₁ ⋯)
hyp₁ : y p₁ ⋯ = p₁✝
⊢ G.Adj v₁ v₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_4
ε : ℝ
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
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ ↑(Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ)
p₂ : Finset (Fin n)
hp₂ : p₂ ∈ ↑(Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ)
hne : p₁ ≠ p₂
v₁ : Fin n
hv₁ : v₁ ∈ ↑p₁
v₂ : Fin n
hv₂ : v₂ ∈ ↑p₂
⊢ G.Adj v₁ v₂

Tactic:
· simp_rw [univ_eq_attach, coe_map, Function.Embedding.coeFn_mk,
          Set.mem_image, mem_coe, mem_attach, true_and, Subtype.exists] at hp₁ hp₂
        replace ⟨p₁, hp₁, hyp₁⟩ := hp₁
        rw [← hyp₁] at hv₁ hne
        have hy₁' := mem_powersetCard.mp (hy p₁ hp₁)
        replace ⟨p₂, hp₂, hyp₂⟩ := hp₂
        rw [← hyp₂] at hv₂ hne
        have hy₂' := mem_powersetCard.mp (hy p₂ hp₂)
        refine K.isCompleteBetween hp₁ hp₂ ?_ (hy₁'.left hv₁) (hy₂'.left hv₂)
        by_contra! heq
        simp [← heq] at hne

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

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

Tactic:
by
  constructor <;>
    · rintro rfl
      simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y

Tactic:
rcases r with ⟨rfl, a⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun a b ↦ f a = b
⊢ Primrec f

Tactic:
by
  rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩
  refine (nat_findGreatest pg h₂).of_eq fun n => ?_
  exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ
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)
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y

Tactic:
rcases r with ⟨rfl, a⟩

Goal state after:
case succ
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
⊢ Acc (lbp p) (k + 1)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a) =
    (f a, List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) (f a))

Tactic:
induction f a <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (f a) = List.map (g a) (f a)

Tactic:
induction f a <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (f a) = List.map (g a) (f a)

Tactic:
by induction f a <;> simp [*]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) (f a) =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) (f a))

Tactic:
induction f a <;> simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ Primrec fun a ↦ (a.1 ::ᵥ a.2).toList

Tactic:
by simpa using list_cons.comp fst (vector_toList_iff.2 snd)

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 2 (2 ^ (n + 3) - 3) = 2 ^ (n + 1 + 3) - 3

Tactic:
ack_two,

Goal state after:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * (2 ^ (n + 3) - 3) + 3 = 2 ^ (n + 1 + 3) - 3
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2
α : 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
h : b ∈ f.fix a
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n

Tactic:
· suffices ∀ a', b ∈ PFun.fix f a' → ∀ k, Sum.inr a' ∈ F a k →
        ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m by
      rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩
      exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩
    intro a₁ h₁
    apply @PFun.fixInduction _ _ _ _ _ _ h₁
    intro a₂ h₂ IH k hk
    rcases PFun.mem_fix_iff.1 h₂ with (h₂ | ⟨a₃, am₃, _⟩)
    · refine ⟨k.succ, ?_, fun m mk km => ⟨a₂, ?_⟩⟩
      · simpa [F] using Or.inr ⟨_, hk, h₂⟩
      · rwa [le_antisymm (Nat.le_of_lt_succ mk) km]
    · rcases IH _ am₃ k.succ (by simpa [F] using ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer),
      the `clear_value F` was not required here. -/
      clear_value F
      grind

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

Goal state before:
pp: ⊢ (fun n ↦ ↑n * 1⁻¹) = fun n ↦ ↑n

Tactic:
by ext; simp

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

Goal state before:

Tactic:
(fun z => p * z ^ (p - 1) * (1 - ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_sub_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) / 1) = fun z ↦ z ^ (p - 1)

Tactic:
by ext; simp

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

Goal state before:
pp: case hbc
α : 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 : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * ↑n ≤ ↑(r i n)
i : α
h₁ : 0 < c
⊢ C / c ≤ ↑⌈C / c⌉₊

Tactic:
simp [Nat.le_ceil]

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 : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn : ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
⊢ ↑(r i n) ≤ c * ↑n

Tactic:
Real.norm_of_nonneg (by positivity)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn : ↑n / log ↑n ^ 2 ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
⊢ ↑(r i n) ≤ c * ↑n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u = c₂ * f x
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, f x = c

Tactic:
rw [eventually_atTop] at h

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
h : ∃ a, ∀ (b : ℝ), a ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, f x = c
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
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n

Tactic:
filter_upwards [eventually_gt_atTop 0] with n hn using R.asympBound_pos n hn

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

Goal state before:
pp: c : ℝ
⊢ GrowsPolynomially fun x ↦ c

Tactic:
refine fun _ _ => ⟨1, by norm_num, 1, by norm_num, ?_⟩
  filter_upwards [] with x
  simp

Goal state after: