mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ a ∈ ↑(g d)

Tactic:
rwa [hcd] at ha

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = G.degree v

Tactic:
rw [← G.card_incidenceSet_eq_degree]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = Fintype.card ↑(G.incidenceSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : G.neighborSet ↑v ⊆ s
⊢ (induce s G).degree v = G.degree ↑v

Tactic:
by
  simp_rw [← card_neighborFinset_eq_degree,
    ← map_neighborFinset_induce_of_neighborSet_subset h, card_map]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b

Tactic:
rw [sdiff_eq_bot_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X : C
i : ℤ
h : WithBotTop.coe i ≤ WithBotTop.coe (n + 1)
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n

Tactic:
simp only [WithBotTop.coe_le_coe] at h

Goal state after:
case coe
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X : C
i : ℤ
h : i ≤ n + 1
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
a b : ↥s
e : #P.parts * ↑(f a).snd + ↑(g (f a).fst) = #P.parts * ↑(f b).snd + ↑(g (f b).fst)
⊢ a = b

Tactic:
mul_comm #P.parts

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
a b : ↥s
e : ↑(f a).snd * #P.parts + ↑(g (f a).fst) = ↑(f b).snd * #P.parts + ↑(g (f b).fst)
⊢ a = b
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset β
⊢ interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab ↦ interedges r (f ab.1) (g ab.2)

Tactic:
simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
⊢ ¬G.IsUniform ε s t ↔
    ∃ s' ⊆ s, ∃ t' ⊆ t, ↑(#s) * ε ≤ ↑(#s') ∧ ↑(#t) * ε ≤ ↑(#t') ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|

Tactic:
by
  unfold IsUniform
  simp only [not_forall, not_lt, exists_prop, Rat.cast_abs, Rat.cast_sub]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case a.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∀ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ (#A / #P.parts + 1) ^ 2

pp: case a.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts.offDiag • (#A / #P.parts + 1) ^ 2 ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2

Tactic:
· simp only [Prod.forall, and_imp, mem_offDiag, sq]
    rintro U V hU hV -
    exact_mod_cast Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)

Goal state after:
case a.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts.offDiag • (#A / #P.parts + 1) ^ 2 ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#P.parts) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) = ↑(#P.parts) * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1)

Tactic:
by rw [mul_assoc]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
induction e using Sym2.ind

Goal state after:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ y✝ : ↑G'.verts
⊢ s(x✝, y✝) ∈ G'.coe.edgeSet ↔ s(x✝, y✝) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet

Tactic:
edgeSet_coe,

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Sym2.map Subtype.val '' Sym2.map Subtype.val ⁻¹' G'.edgeSet = G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
⊢ (G'.neighborSet v).toFinset.card = G'.degree v

Tactic:
rw [degree, Set.toFinset_card]

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

Goal state before:
pp: case Adj.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (x✝¹ = v ∨ x✝¹ = w) ∧ (x✝ = v ∨ x✝ = w) ∧ G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h

Goal state after:
case Adj.mpr.inl.inl
V : Type u
G : SimpleGraph V
w x✝ : V
hvw : G.Adj x✝ w
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝

case Adj.mpr.inl.inr
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha hvw : G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

case Adj.mpr.inr.inl
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha : G.Adj x✝¹ x✝
hvw : G.Adj x✝ x✝¹
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

case Adj.mpr.inr.inr
V : Type u
G : SimpleGraph V
v x✝ : V
hvw : G.Adj v x✝
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.getLast ⋯ = b

Tactic:
by
  induction p <;> simp [*]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u :: List.map (fun x ↦ x.toProd.2) p.darts = p.support

Tactic:
by
  induction p <;> simp [*]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x ↦ x.toProd.1) p.darts ++ [v] = p.support

Tactic:
by
  induction p <;> simp [*]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support.length = p.length + 1

Tactic:
by
  induction p <;> simp [*]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.darts.length = p.length

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Walk.map Hom.id p = p

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v : V
p : G.Walk u v
⊢ Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.transfer G ⋯ = p

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
GH : G ≤ H
⊢ p.transfer H hp = Walk.map (Hom.ofLE GH) p

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).edges = p.edges

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).support = p.support

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).length = p.length

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.append nil = p

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
K : SimpleGraph V
hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet
⊢ (p.transfer H hp).transfer K hp' = p.transfer K ⋯

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk w x
⊢ p.append (q.append r) = (p.append q).append r

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
⊢ (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).reverse = p.reverse.transfer H ⋯

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').darts = p.darts ++ p'.darts

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.darts = (List.map Dart.symm p.darts).reverse

Tactic:
by
  induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.1, d.toProd.2) ∈ p.edges
⊢ d.toProd.1 ∈ p.support

Tactic:
exact dart_fst_mem_support_of_mem_darts _ hd

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hadj : G.Adj v v
hp : (cons hadj nil).IsCircuit
⊢ 3 ≤ (cons hadj nil).length

Tactic:
simp at hadj

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(A.sup id)) ≤ ↑(#A) * ↑(#x) * ((↑m + 1) / ↑m)

pp: case h₂
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(B.sup id)) ≤ ↑(#B) * ↑(#y) * ((↑m + 1) / ↑m)

Tactic:
exacts [sum_card_subset_chunk_parts_le (by sz_positivity) hA hx,
          sum_card_subset_chunk_parts_le (by sz_positivity) hB hy]

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ G.Adj ((φ.setValue x s) a) ((φ.setValue x s) b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
simp only [Embedding.coeFn_mk, Embedding.setValue, not_exists.mp ms, ite_false]

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ G.Adj (if a = x then s else φ a) (if b = x then s else φ b) ↔ (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ H.IsNClique 3 {x, y, z}

Tactic:
is3Clique_triple_iff

Goal state after:
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ H.Adj x y ∧ H.Adj x z ∧ H.Adj y z
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hp : (Walk.map f p).IsCycle
⊢ p.IsCycle

Tactic:
by
  rw [isCycle_def, ne_eq, eq_nil_iff_nil]
  rw [isCycle_def, ne_eq, eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail] at hp
  exact hp.imp .of_map <| .imp_right <| .of_map f

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case hab.refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
      (↑(#(chunk hP G ε hU).parts) * ↑(#(chunk hP G ε hV).parts)) ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts

Tactic:
· rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
⊢ ∑ x, (eval x) f = 0

Tactic:
have : DecidableEq K := Classical.decEq K

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∑ x, (eval x) f = 0
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∑ x, (eval x) f = ∑ x, ∑ d ∈ f.support, coeff d f * ∏ i, x i ^ d i

Tactic:
simp only [eval_eq']

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
⊢ (eval x) F = if x ∈ S then 1 else 0

Tactic:
calc
      eval x F = ∏ i ∈ s, eval x (1 - f i ^ (q - 1)) := eval_prod s _ x
      _ = if x ∈ S then 1 else 0 := ?_

Goal state after:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
⊢ ∏ i ∈ s, (eval x) (1 - f i ^ (q - 1)) = if x ∈ S then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
this :
  ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V) * #(star hP G ε hV U)) / ↑(4 * 4) ^ #P.parts * (3 ^ 2 / 4 ^ 2) * ε ^ 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity x.1 x.2) ^ 2) / ↑(4 * 4) ^ #P.parts
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts

Tactic:
norm_num at this

Goal state after:
case refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
this :
  ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity x.1 x.2) ^ 2) / 16 ^ #P.parts
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
⊢ (eval 0) (f₁ s a) = 0 ∧ (eval 0) (f₂ s a) = 0

Tactic:
by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

Goal state after:
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ Sized r (⋃ i, f i) ↔ ∀ (i : ι), Sized r (f i)

Tactic:
by
  simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]
  exact forall_comm

Goal state after: