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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u' : V
⊢ nil.copy ⋯ ⋯ = nil

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u' w' : V
h : G.Adj u' v
p : G.Walk v w'
⊢ (cons h p).copy ⋯ ⋯ = cons ⋯ (p.copy ⋯ ⋯)

Tactic:
rfl

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 v' w'
h : G.Adj u v'
⊢ cons h (p.copy ⋯ ⋯) = (cons ⋯ p).copy ⋯ ⋯

Tactic:
rfl

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'
q : G.Walk v' w'
⊢ (p.copy ⋯ ⋯).append (q.copy ⋯ ⋯) = (p.append q).copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List V
head✝ : V
hne : [head✝] ≠ []
hchain : List.IsChain G.Adj [head✝]
⊢ (ofSupport [head✝] hne hchain).support = [head✝]

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List G.Dart
head✝ : G.Dart
hne : [head✝] ≠ []
hchain : List.IsChain G.DartAdj [head✝]
⊢ (ofDarts [head✝] hne hchain).darts = [head✝]

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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.copy ⋯ ⋯).reverse = p.reverse.copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.reverse = nil

Tactic:
rfl

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.copy ⋯ ⋯).length = p.length

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ : V
⊢ nil.reverse.getVert i = nil.getVert (nil.length - i)

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length + p₁.length ≤ p₂.length

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₁.support.length ≤ s.length + p₁.length + 1 - s.length

Tactic:
grind

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

Goal state before:
pp: 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]
⊢ p₁.darts.length + k ≤ p₂.darts.length

Tactic:
grind

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

Goal state before:
pp: 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]
⊢ p₁.support.length + k ≤ p₂.support.length

Tactic:
grind

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ nil.support
⊢ (nil.takeUntil u✝ h).append (nil.dropUntil u✝ h) = nil

Tactic:
rfl

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

Goal state before:
pp: case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝

Tactic:
· simp only [concat_nil, concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he).symm).elim

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

Goal state before:
pp: 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
⊢ i + k < p₂.darts.length

Tactic:
grind

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w ≠ a
⊢ List.idxOf w (cons h✝ p).support ≠ 0

Tactic:
grind

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w ≠ a
⊢ (if hx : a = w then Eq.ndrec (motive := fun u ↦ u ∈ (cons h✝ p).support → G.Walk u w✝) (fun h ↦ cons h✝ p) hx h
      else p.dropUntil w ⋯).support =
    ((p.drop (List.idxOf w (cons h✝ p).support - 1)).copy ⋯ ⋯).support

Tactic:
grind

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

Goal state before:
pp: 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
⊢ i + k < p₂.support.length

Tactic:
grind

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.copy ⋯ ⋯).support = p.support

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support.dropLast ++ [u] = nil.support

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ p.support.tail ++ p'.support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail

Tactic:
List.mem_append

Goal state after:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ ofSupport nil.support ⋯ ⋯ = nil.copy ⋯ ⋯

Tactic:
rfl

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
w : V
h : G.Adj u w
⊢ ofSupport (cons h nil).support ⋯ ⋯ = (cons h nil).copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: 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
h'' : (u✝, v✝) = (u, x) ∨ (u✝, v✝) = (u, x).swap
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

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

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

case pos.inr
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
p' : G.Walk (u, x).1 w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
ha : G.Adj (u, x).2 (u, x).1
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1
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.copy ⋯ ⋯).darts = p.darts

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).takeUntil u h = (p.takeUntil u ⋯).copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ ⋯

Tactic:
rfl

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
hp : ¬p.Nil
w : V
h : G.Adj u w
x✝ : ¬(cons h nil).Nil
⊢ ofDarts (cons h nil).darts ⋯ ⋯ = (cons h nil).copy ⋯ ⋯

Tactic:
rfl

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.copy ⋯ ⋯).edges = p.edges

Tactic:
rfl

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

Goal state before:
pp: case base
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
⊢ (p.take n).IsSubwalk (p.take n)

Tactic:
rfl

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

Goal state before:
pp: case base
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
⊢ (p.drop n).IsSubwalk (p.drop n)

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ (p.takeUntil u h).length

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsTrail ↔ p.IsTrail

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsPath ↔ p.IsPath

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCircuit ↔ p.IsCircuit

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCycle ↔ p.IsCycle

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
this : ((p.take (min (p.length - 1) n)).copy ⋯ ⋯).IsPath
⊢ (p.take n).IsPath

Tactic:
isPath_copy,

Goal state after:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
this : (p.take (min (p.length - 1) n)).IsPath
⊢ (p.take n).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

Tactic:
grind [support_copy, support_take]

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
n m : ℕ
⊢ List.drop (min n p.length + min m (p.length - n)) p.support = List.drop (min (n + m) p.length) p.support

Tactic:
grind

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).tail = nil.copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h (cons h✝ p✝)).tail = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
t u v u✝ : V
h : G.Adj u✝ t
⊢ (nil.concat h).dropLast = nil.copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v u✝ v✝ : V
hadj : G.Adj u✝ v✝
hind : ∀ (hp : G.Adj nil.penultimate v✝), nil.dropLast.concat hp = nil
hp : G.Adj (cons hadj nil).penultimate v✝
⊢ (cons hadj nil).dropLast.concat hp = cons hadj nil

Tactic:
rfl

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.copy ⋯ ⋯).Nil = p.Nil

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
w x : V
i : ℕ
p : G.Walk w x
⊢ (p.copy ⋯ ⋯).getVert i = p.getVert i

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.tail.support ~ nil.dropLast.support

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support.tail ~ nil.support.dropLast

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.IsNClique n ∅ ↔ n = 0

Tactic:
simp [isNClique_iff, eq_comm]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
a : α
⊢ G.IsNClique n {a} ↔ n = 1

Tactic:
simp [isNClique_iff, eq_comm]

Goal state after:
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
⊢ A.product B = A ×ˢ B

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
this✝ : List.count v c.support.tail = 1
this : c.support.head? = some v
⊢ List.count v c.support = 2

Tactic:
grind

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this✝¹ : u = c.support.head ⋯ ∨ u ∈ c.support.tail
this✝ : List.count u c.support.tail = 1
this : c.support.head? = some v
⊢ List.count u c.support = 1

Tactic:
grind

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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
he : s(u, v✝) ∈ (p.takeUntil u hup).edges
⊢ False

Tactic:
exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset_edges hup he

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
h : Walk.nil.IsPath
⊢ ⟨Walk.nil, h⟩ = Path.nil

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G H : SimpleGraph α
ε δ : 𝕜
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
⊢ ((G.cliqueSet 3).Pairwise fun x y ↦ ∀ a ∈ x ∩ y, ∀ b ∈ x ∩ y, a = b) ↔
    (G.cliqueSet 3).Pairwise fun x y ↦ (↑(x ∩ y)).Subsingleton

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
this : Fintype α
⊢ BddAbove {n | ∃ s, G.IsNClique n s}

Tactic:
use card α

Goal state after:
case h
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
this : Fintype α
⊢ Fintype.card α ∈ upperBounds {n | ∃ s, G.IsNClique n s}
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).bypass = p.bypass.copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal G.IsIndepSet ↑s

Tactic:
← isMaximalClique_compl

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal Gᶜ.IsClique ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ toDeleteEdges s (p.copy ⋯ ⋯) h = (toDeleteEdges s p ⋯).copy ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
A✝ : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
A : Finset (G × G)
x₁ x₂ : G
⊢ (x₁, x₂) = (x₁, x₂)

Tactic:
rfl

Goal state after:
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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
    (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
t : ℝ := ↑(G.edgeDensity U V)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ ε ^ 5 / 49
hqt : |q - t| ≤ ε ^ 5 / 49
hε' : ε ^ 5 ≤ ε
⊢ 3 / 4 * ε ≤ |p - q|

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s : Finset α
⊢ Eₘ[s, univ] = Fintype.card α * #s ^ 2

Tactic:
rw [mulEnergy_comm, mulEnergy_univ_left]

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 σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
⊢ ↑(e a) (e' (Sum.inl default)) ^ d (e' (Sum.inl default)) * ∏ a₂, ↑(e a) (e' (Sum.inr a₂)) ^ d (e' (Sum.inr a₂)) =
    ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j

Tactic:
rfl

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 σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }

Tactic:
by
  let F : Unit → MvPolynomial σ K := fun _ => f
  have : (∑ i : Unit, (F i).totalDegree) < Fintype.card σ := h
  convert! char_dvd_card_solutions_of_sum_lt p this
  aesop

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 < x
⊢ (#A + 1).choose 2 < #A.subsetSum

Tactic:
by
  induction A using induction_on_max with
  | empty => simp
  | insert a A A_lt_a ih =>
    have A_pos' : ∀ x ∈ A, 0 < x := fun x hx => A_pos x (mem_insert_of_mem hx)
    grw [card_insert_of_notMem fun ha => (A_lt_a a ha).false, Nat.choose_succ_left _ _ (by lia),
      Nat.choose_one_right, add_right_comm, add_assoc, Nat.add_one_le_iff.2 (ih A_pos')]
    exact card_add_card_subsetSum_lt_card_subsetSum_insert_max A_pos' A_lt_a <| A_pos a <|
      mem_insert_self a A

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun x ↦ x - (a + 1)) L).SortedLT

pp: case refine_2
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ L = map (fun x ↦ x + a + 1) (map (fun x ↦ x - (a + 1)) L)

Tactic:
· rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]
      simp only [and_congr_right_iff]
      exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]

Goal state after:
case refine_2
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ L = map (fun x ↦ x + a + 1) (map (fun x ↦ x - (a + 1)) L)
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ (mk K v.rep ⋯).submodule = K ∙ v.rep

Tactic:
rfl

Goal state after: