mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ∞
⊢ n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)

Tactic:
simp [minOrder]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
u v : W
⊢ (SimpleGraph.map (⇑f) G).Adj u v ↔ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v

Tactic:
dsimp [SimpleGraph.map, Relation.Map]

Goal state after:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
u v : W
⊢ (¬u = v ∧ ∃ a b, G.Adj a b ∧ f a = u ∧ f b = v) ↔ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ u ∈ ⇑f '' G.neighborSet v → u ∈ (SimpleGraph.map (⇑f) G).neighborSet (f v)

Tactic:
exact fun ⟨u', hadj, hu⟩ ↦ ⟨hu ▸ f.injective.ne hadj.ne, v, u', hadj, rfl, hu⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (SimpleGraph.map id G).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
dsimp [SimpleGraph.map, Relation.Map]

Goal state after:
V : Type u_1
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (¬x✝¹ = x✝ ∧ ∃ a b, G.Adj a b ∧ a = x✝¹ ∧ b = x✝) ↔ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
x✝¹ x✝ : X
⊢ (SimpleGraph.map g (SimpleGraph.map f G)).Adj x✝¹ x✝ ↔ (SimpleGraph.map (g ∘ f) G).Adj x✝¹ x✝

Tactic:
dsimp [SimpleGraph.map, Relation.Map]

Goal state after:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
x✝¹ x✝ : X
⊢ (¬x✝¹ = x✝ ∧ ∃ a b, (¬a = b ∧ ∃ a_1 b_1, G.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∧ g a = x✝¹ ∧ g b = x✝) ↔
    ¬x✝¹ = x✝ ∧ ∃ a b, G.Adj a b ∧ g (f a) = x✝¹ ∧ g (f b) = x✝
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
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ ↑(g i)
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
⊢ Function.onFun Disjoint f a b

Tactic:
obtain ⟨d, hd, hb⟩ := hb

Goal state after:
α : 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)
⊢ Function.onFun Disjoint f a b
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
by_cases! h : ∀ a ∈ s, f a = b + 1

Goal state after:
case pos
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∃ a ∈ s, f a ≠ b + 1
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
classical
  rw [← card_edgeFinset_top_eq_card_choose_two]
  exact card_le_card (edgeFinset_mono le_top)

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✝ : Fintype ↑G.edgeSet
⊢ G.degree v ≤ #G.edgeFinset

Tactic:
by
  classical
  rw [← card_incidenceFinset_eq_degree]
  exact card_le_card (G.incidenceFinset_subset v)

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)

Tactic:
intro v
  rw [degree_compl, h v]

Goal state after:
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
h : G.support ⊆ s
⊢ G.edgeSet ⊆ (↑s.toFinset).sym2

Tactic:
Set.coe_toFinset

Goal state after:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeSet ⊆ s.sym2
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) = #P.parts - #s % #P.parts

Tactic:
by
  conv_rhs =>
    arg 1
    rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]
  rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∀ a ∈ P.parts, ¬#a = #s / #P.parts + 1 ↔ #a = #s / #P.parts

Tactic:
exact fun _ ha ↦ by rw [hP.card_part_eq_average_iff ha, ne_eq]

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

Goal state before:
pp: 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
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
⊢ IsIso (t.eTruncGEToGEGE a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  intro
  simp only [eTruncGEToGEGE_app]
  exact t.isIso_eTruncGE_obj_map_truncGEπ_app _ _ hab _

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 α
h : ¬G.IsUniform ε s t
⊢ G.nonuniformWitness ε s t ⊆ s

Tactic:
unfold nonuniformWitness
  split_ifs
  · exact G.left_nonuniformWitnesses_subset h
  · exact G.right_nonuniformWitnesses_subset fun i => h i.symm

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

Goal state before:
pp: α : Type u_4
r : α → α → Prop
inst✝¹ : DecidableRel r
s t : Finset α
inst✝ : Std.Symm r
x : α × α
⊢ x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2

Tactic:
exact and_left_comm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts.offDiag) ≤ 1 * ↑(#P.parts) ^ 2

Tactic:
rw [offDiag_card, one_mul]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts * #P.parts - #P.parts) ≤ ↑(#P.parts) ^ 2
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)
h : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
rw [degree, Fintype.card_eq_zero_iff, isEmpty_subtype]

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
h : v ∉ G'.verts
⊢ ∀ (x : V), x ∉ G'.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Disjoint (G.edgeFinset \ G.incidenceFinset t) (image (fun x ↦ s(x, t)) (G.neighborFinset s))

Tactic:
disjoint_iff_ne

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ a ∈ G.edgeFinset \ G.incidenceFinset t, ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), a ≠ b
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).spanningCoe = (SimpleGraph.induce s G).spanningCoe

Tactic:
induce_eq_coe_induce_top

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).spanningCoe = (⊤.induce s).coe.spanningCoe
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ G'.induce s ≤ G''.induce s'

Tactic:
constructor
  · simp [hs]
  · simp +contextual only [induce_adj, and_imp]
    intro v w hv hw ha
    exact ⟨hs hv, hs hw, hg.2 ha⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : G.Adj u v
n : ℕ
hn : n + 1 ≠ 0
⊢ (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)

Tactic:
getVert_cons_succ,

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : G.Adj u v
n : ℕ
hn : n + 1 ≠ 0
⊢ p.getVert n = p.getVert (n + 1 - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).reverse = Walk.map f nil.reverse

Tactic:
simp [map_append, *]

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

Goal state before:
pp: case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).reverse = Walk.map f p✝.reverse
⊢ (Walk.map f (cons h✝ p✝)).reverse = Walk.map f (cons h✝ p✝).reverse

Tactic:
simp [map_append, *]

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

Goal state before:
pp: case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
⊢ (if hx : u✝ = u then hx ▸ nil else cons h✝ (p✝.takeUntil u ⋯)).append
      (if hx : u✝ = u then Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) hx ⋯
      else p✝.dropUntil u ⋯) =
    cons h✝ p✝

Tactic:
split_ifs with h'

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : u✝ = u
⊢ (h' ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) h' ⋯) =
    cons h✝ p✝

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k]? = some p₁.darts[i]

pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]

Tactic:
· rw [getElem?_pos _ _ <| by grind, Option.some_inj]
    ext <;> grind [fst_darts_getElem, snd_darts_getElem]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
⊢ List.count u (if hx : u✝ = u then hx ▸ nil else cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
split_ifs with h'

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h' : u✝ = u
⊢ List.count u (h' ▸ nil).support = 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
⊢ List.count s(u, x) (if hx : u✝ = u then hx ▸ nil else cons ha (p'.takeUntil u ⋯)).edges ≤ 1

Tactic:
split_ifs with h'

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : u✝ = u
⊢ List.count s(u, x) (h' ▸ nil).edges ≤ 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
⊢ List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).support.tail ~r c.support.tail

Tactic:
simp only [rotate, tail_support_append]

Goal state after:
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : 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
| (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
rw [SimpleGraph.edgeDensity, edgeDensity, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl)]
    simp only [cast_sum, mul_sum, sum_div, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) + _)]

Goal state after:
α : 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 ∈ ((chunk hP G ε hU).ofSubset hA ⋯).parts ×ˢ ((chunk hP G ε hV).ofSubset hB ⋯).parts,
    ↑↑(#(interedges G.Adj x.1 x.2)) * ((1 + ε ^ 5 / 49) / ↑(↑(#(A.sup id)) * ↑(#(B.sup id))))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3

Tactic:
is3Clique_iff,

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ (∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔ ∃ u w, w.IsCycle ∧ w.length = 3
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
k✝ : ℕ
hl✝ : k✝ ≤ p.length
hl : k✝ = 1
⊢ p.getVert 1 = ⋯.toWalk.getVert 1

Tactic:
getVert_cons_succ,

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
k✝ : ℕ
hl✝ : k✝ ≤ p.length
hl : k✝ = 1
⊢ p.getVert 1 = Walk.nil.getVert 0
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp = q.takeUntil w hwq
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
have := ih _ (hs ▸ length_dropUntil_lt_length hwp hwu) (hp.dropUntil hwp) (hq.dropUntil hwq)
        <| by grind [take_spec]

Goal state after:
case neg
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp = q.takeUntil w hwq
this :
  (p.dropUntil w hwp).length = (p.dropUntil w hwp).length →
    ∃ u' v' p' q', p'.IsSubwalk (p.dropUntil w hwp) ∧ q'.IsSubwalk (q.dropUntil w hwq) ∧ (p'.append q'.reverse).IsCycle
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ s ×ˢ t ×ˢ u |
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}))

Tactic:
classical
  have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
  have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
  let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
  have : X'.biUnion _ ⊆ (s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c :=
    triangle_split_helper _
  refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
  rw [card_biUnion, Nat.cast_sum]
  · apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
    rw [nsmul_eq_mul]
    have := hst.pos.le
    suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
    have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
    rw [sub_mul, one_mul, card_sdiff_of_subset i, Nat.cast_sub (card_le_card i),
      sub_le_sub_iff_left, mul_assoc, mul_comm ε, two_mul]
    refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
    rw [Nat.cast_add]
    gcongr
  rintro a _ b _ t
  rw [Function.onFun, Finset.disjoint_left]
  simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
  aesop

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ z ∈ t, x ∈ toTriangle z ∧ y ∈ toTriangle z

Tactic:
cases hxy <;> exact ⟨_, ‹_›, by simp⟩

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ False

Tactic:
rw [Nat.floor_lt' (by positivity), inv_lt_iff_one_lt_mul₀' (by positivity)] at hG

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).LocallyLinear

Tactic:
refine ⟨?_, fun x y hxy ↦ ?_⟩
  · unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]
  · obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
    exact ⟨_, toTriangle_is3Clique hz, hxy⟩

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty
  · simp
  · exact div_mul_cancel₀ _ (by positivity)

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty
  · simp
  · exact div_mul_cancel₀ _ (by positivity)

Goal state after:
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2 ≤ #u * ∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2

Tactic:
simpa using sum_mul_sq_le_sq_mul_sq (R := ℕ) _ 1 _

Goal state after:
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
s : Finset α
⊢ IsClosed (s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x})

Tactic:
exact (isClosed_discrete _).preimage (by fun_prop)

Goal state after: