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

Goal state before:
pp: n r : ℕ
hr : 0 < r
⊢ (turanGraph n r).CliqueFree (r + 1)

Tactic:
rw [cliqueFree_iff]

Goal state after:
n r : ℕ
hr : 0 < r
⊢ IsEmpty ((completeGraph (Fin (r + 1))).Copy (turanGraph n r))
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
this : (↑⟨mapLe hle p, ⋯⟩).edges = (↑(Path.singleton hadj)).edges
⊢ G'.Adj u v

Tactic:
simp only [edges_map, Hom.coe_ofLE, Sym2.map_id, List.map_id_fun, id_eq] at this

Goal state after:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
this : p.edges = (↑(Path.singleton hadj)).edges
⊢ G'.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬Even p.length ↔ (c u = true ↔ c w = true)

Tactic:
have : ¬ c u = true ↔ c v = true := by
      rw [← not_iff, ← Bool.eq_iff_iff]
      exact c.valid h

Goal state after:
case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
this : ¬c u = true ↔ c v = true
⊢ ¬Even p.length ↔ (c u = true ↔ c w = true)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(Odd v ↔ Even v)

Tactic:
apply Classical.not_iff.mpr

Goal state after:
case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬Odd v ↔ Even v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(Even u ↔ Odd u)

Tactic:
apply Classical.not_iff.mpr

Goal state after:
case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬Even u ↔ Odd u
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
⊢ #((G.replaceVertex s t).neighborFinset u) = #(G.neighborFinset u) - #{t}

Tactic:
← card_sdiff_of_subset (by simp [h.symm])

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
⊢ #((G.replaceVertex s t).neighborFinset u) = #(G.neighborFinset u \ {t})
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length

Tactic:
by
  simp_rw [← Nat.not_odd_iff_even]
  constructor <;> intro h
  · intro _ w ho
    have := (w.three_le_chromaticNumber_of_odd_loop ho).trans h.chromaticNumber_le
    norm_cast
  · apply colorable_iff_forall_connectedComponent.2
    intro c
    obtain ⟨_, hv⟩ := c.nonempty_supp
    use fun a ↦ Fin.ofNat 2 (c.connected_toSimpleGraph ⟨_, hv⟩ a).some.length
    intro a b hab he
    apply h _ <| (((c.connected_toSimpleGraph ⟨_, hv⟩ a).some.concat hab).append
                 (c.connected_toSimpleGraph ⟨_, hv⟩ b).some.reverse).map c.toSimpleGraph_hom
    rw [length_map, length_append, length_concat, length_reverse, add_right_comm]
    have : ((Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ a)).length) % 2 =
        (Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ b)).length % 2 := by
      simp_rw [← Fin.val_natCast, ← Fin.ofNat_eq_cast, he]
    exact (Nat.even_iff.mpr (by lia)).add_one

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : ¬G.Adj v w
⊢ h.finpartition.part v = h.finpartition.part w

Tactic:
by rwa [← h.not_adj_iff_part_eq]

Goal state after:
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.length + 1

Tactic:
exact p.length.ne_add_one

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

Goal state before:
pp: case h
r t : ℕ
x✝ : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (i₁, x).1 ≠ (i₂, x).1

Tactic:
exact hv

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

Goal state before:
pp: r t : ℕ
⊢ ∑ v, (r - 1) * t = 2 * (r.choose 2 * t ^ 2)

Tactic:
sum_const,

Goal state after:
r t : ℕ
⊢ #univ • ((r - 1) * t) = 2 * (r.choose 2 * t ^ 2)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
c : Fin n
⊢ Nonempty (↑(C.colorClass c) ↪ Fin t)

Tactic:
Embedding.nonempty_iff_card_le,

Goal state after:
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
c : Fin n
⊢ Fintype.card ↑(C.colorClass c) ≤ Fintype.card (Fin t)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ ∑ x ∈ K.parts, t = r * t

Tactic:
sum_const,

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.parts • t = r * t
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ Nonempty (Fin r ↪ ↥K.parts)

Tactic:
Embedding.nonempty_iff_card_le,

Goal state after:
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ Fintype.card (Fin r) ≤ Fintype.card ↥K.parts
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r

Tactic:
· have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
p : ↥K.parts
⊢ Nonempty (Fin t ↪ ↥↑p)

Tactic:
Embedding.nonempty_iff_card_le,

Goal state after:
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
p : ↥K.parts
⊢ Fintype.card (Fin t) ≤ Fintype.card ↥↑p
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ G.eccent u = 0

Tactic:
simpa [eccent, edist_eq_zero_iff] using subsingleton_iff.mp ‹_› u

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ ↑C
⊢ False

Tactic:
obtain ⟨p⟩ := Gc v u

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ ↑C
p : G.Walk v u
⊢ False
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
⊢ ↑(#G.edgeFinset) * (↑n - 1) ≤ (↑n + 1) * ↑(extremalNumber n H)

Tactic:
← Nat.cast_pred (by positivity),

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
⊢ ↑(#G.edgeFinset) * ↑(n - 1) ≤ (↑n + 1) * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
⊢ ⊤.egirth ≤ 3

Tactic:
obtain ⟨s, hcard⟩ := Cardinal.exists_finset_eq_card <| Cardinal.ofNat_le_toENat.mp h

Goal state after:
α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
⊢ ⊤.egirth ≤ 3
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'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
sum_const,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ #(K.vertsᶜ \ filter K t) • (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)
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'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts) - ↑(#(filter K t))) * (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
sum_const,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts) - ↑(#(filter K t))) * (↑(#K.verts) - ↑t' + ↑t) + #(filter K t) • ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ zarankiewicz m n s t ≤ extremalNumber (m + n) (completeBipartiteGraph α β)

Tactic:
conv =>
    enter [2, 1]
    rw [← Fintype.card_fin (m + n)]
  simp_rw [zarankiewicz, Finset.sup_le_iff, mem_filter, mem_univ, true_and]
  intro B ⟨_, h⟩
  rw [(Iso.map finSumFinEquiv B).card_edgeFinset_eq]
  refine card_edgeFinset_le_extremalNumber <|
    (h.congr_left ?_).congr_right (Iso.map finSumFinEquiv B).symm
  exact completeBipartiteGraphCongr
    (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)

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

Goal state before:
pp: case refine_2.inl
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨u, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

pp: case refine_2.inr
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨v, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

Tactic:
· simp [h.toEdge_eq_of_adj huv]

Goal state after:
case refine_2.inr
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨v, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}
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
h : r ≤ k
⊢ ¬G.CliqueFree (r + 2)

Tactic:
have hs := eq_of_subset_of_card_le inter_subset_left (hw.card_inter ▸ hw.card_left ▸ h)

Goal state after:
α : 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
h : r ≤ k
hs : s ∩ t = s
⊢ ¬G.CliqueFree (r + 2)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
⊢ ∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
obtain ⟨_, _, _, s, t, hw⟩ :=
    exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hnc

Goal state after:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w✝² w✝¹ w✝ : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w✝² w✝¹ w✝ s t
⊢ ∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
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' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
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)
⊢ ↑G.minDegree < ↑n

Tactic:
conv_rhs =>
          rw [← Fintype.card_fin n]

Goal state after:
ε : ℝ
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' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
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)
⊢ ↑G.minDegree < ↑(Fintype.card (Fin n))
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' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
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'
hr_ne_1 : r ≠ 1
hδ' : ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑n
⊢ completeEquipartiteGraph r.pred.succ t' ⊑ G

Tactic:
exact ih n (hn.trans' (le_max_of_le_left (le_max_right 1 N'))) hδ'

Goal state after:
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
⊢ ⊤.IsPerfectMatching

Tactic:
Subgraph.isPerfectMatching_iff

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
⊢ ∀ (v : V), ∃! w, ⊤.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hf : G.CliqueFree (r + 1)
hd : (3 * r - 4) * ‖α‖ / (3 * r - 1) < G.minDegree
⊢ G.Colorable r

Tactic:
match r with
  | 0 | 1 => aesop
  | r + 2 =>
    classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this

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

Goal state before:
pp: μ : YoungDiagram
i x✝³ : ℕ
x✝² : x✝³ ∈ Prod.mk i ⁻¹' ↑μ.cells
x✝¹ : ℕ
x✝ : x✝¹ ∈ Prod.mk i ⁻¹' ↑μ.cells
h : (i, x✝³) = (i, x✝¹)
⊢ x✝³ = x✝¹

Tactic:
cases h
        rfl

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

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < μ.colLen j

Tactic:
rw [← rowLen_transpose, ← mem_iff_lt_rowLen]
  simp

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

Goal state before:
pp: α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode (decode n) = encode (decode n)

Tactic:
rw [decode_ofEquiv]

Goal state after:
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode (decode n) = encode (Option.map (⇑e.symm) (decode n))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x ↦ Nat.casesOn x 2 fun x ↦ 0) = encode (decode (n + 2))

Tactic:
rw [decode_ge_two]

Goal state after:
n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x ↦ Nat.casesOn x 2 fun x ↦ 0) = encode none

case h
n✝ n : ℕ
⊢ 2 ≤ n + 2
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
⊢ n ∈ rfind p

Tactic:
by
    let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩
    rcases lt_trichotomy m n with (h | h | h)
    · injection mem_unique (h₂ h) (rfind_spec hm)
    · rwa [← h]
    · injection mem_unique h₁ (rfind_min hm h)

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: 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 : ℕ
⊢ (max (f n) (g n) + 1) ^ 2 ≤ (ack (max a b) n + 1) ^ 2

Tactic:
rw [max_ack_left]; gcongr; exacts [(ha n).le, (hb n).le]

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

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖

Tactic:
refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1))
      (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case log
x : ℝ
hx : x ∈ Set.Ioi 1
⊢ x ∈ Set.Ioi 0

Tactic:
exact Set.Ioi_subset_Ioi zero_le_one hx

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

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

Tactic:
filter_upwards [hc] with _ hc; simpa only [hc]

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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < asympBound g a b (r i n)

Tactic:
by
  rw [Filter.eventually_all]
  exact fun i => (R.tendsto_atTop_r i).eventually R.eventually_asympBound_pos

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
⊢ ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
have h₁ : q (b i * n) + (b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n)
      = (b i) ^ (p a b) * n ^ (p a b) * (1 - ε n) := by
    have := R.b_pos i
    simp only [q, mul_rpow (by positivity : (0 : ℝ) ≤ b i) (by positivity : (0 : ℝ) ≤ n)]
    ring

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
⊢ ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)