mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 * √(log ↑N) ≤ log ↑N

Tactic:
← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _),

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 ≤ log ↑N / √(log ↑N)

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ -2 ≤ -(2 / ↑n * √(log ↑N))

pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)

Tactic:
neg_le_neg_iff,

Goal state after:
case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 2 / ↑n * √(log ↑N) ≤ 2

case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case inr
N : ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
· exact lower_bound_le_one' hN hN'

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ (A ^ m ∩ B ^ n) ^ 2 ⊆ A ^ (2 * m) ∩ B ^ (2 * n)

Tactic:
calc
      (A ^ m ∩ B ^ n) ^ 2 ⊆ (A ^ m) ^ 2 ∩ (B ^ n) ^ 2 := Set.inter_pow_subset
      _ = A ^ (2 * m) ∩ B ^ (2 * n) := by simp [pow_mul']

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G✝ : SimpleGraph V
G' : SimpleGraph W
u v : V
f : V → W
G : SimpleGraph V
a b : W
⊢ (Ne ⊓ Relation.Map G.Adj f f) a b → (Ne ⊓ Relation.Map G.Adj f f) b a

Tactic:
aesop (add norm unfold Relation.Map) (add forward safe Adj.symm)

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]
  grind [SimpleGraph.Adj.ne]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < k + k
⊢ 0 < k

Tactic:
← two_mul,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hh : 0 < 2 * k
⊢ 0 < k
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (g '' ↑s).PairwiseDisjoint f

Tactic:
exact hs.image_of_le hf

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ (I.sup fun x ↦ (P x).parts.sup id) = I.sup a

Tactic:
exact sup_congr rfl fun i _ => (P i).sup_parts

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥↑t
e : α
⊢ e ∈ ↑((fun x ↦ ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x ↦ ⟨↑x.snd, ⋯⟩) x)).fst ↔ e ∈ ↑x.fst

pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥↑t
⊢ ↑((fun x ↦ ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x ↦ ⟨↑x.snd, ⋯⟩) x)).snd = ↑x.snd

Tactic:
· obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x
      dsimp only at mf ⊢
      rw [P.part_eq_of_mem mp mf]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥↑t
⊢ ↑((fun x ↦ ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x ↦ ⟨↑x.snd, ⋯⟩) x)).snd = ↑x.snd
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
ht : t.Nonempty
⊢ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n

Tactic:
hn₃

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
ht : t.Nonempty
⊢ #s - n = #s - n
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
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * (↑(#A) + ↑(#P.parts)) ^ 2 ≤ ε * (↑(#A) + ↑(#A)) ^ 2

Tactic:
by gcongr; exact P.card_parts_le_card

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 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ε * (↑(#A) + ↑(#P.parts)) ^ 2 ≤ ε * (↑(#A) + ↑(#A)) ^ 2

Tactic:
by gcongr; exact P.card_parts_le_card

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
obtain rfl | hUV := eq_or_ne U V

Goal state after:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
hV : U ∈ P.parts
hy : y ∈ U
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
⊢ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n

Tactic:
hn₃

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
⊢ #s - n = #s - n
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∉ G.incidenceFinset x ↔ x ∉ x✝

Tactic:
rw [incidenceFinset, Set.mem_toFinset, incidenceSet,
    Set.mem_ofPred_eq, not_and, Classical.imp_iff_right_iff]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∈ G.edgeSet ∨ x ∉ x✝
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - Fintype.card ↑{x}

Tactic:
← Set.toFinset_card,

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ #(G.deleteIncidenceSet x).support.toFinset ≤ #G.support.toFinset - #{x}.toFinset
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
v w : V
s : Set V
G : SimpleGraph ↑s
hadj : G.spanningCoe.Adj v w
⊢ v ∈ s

Tactic:
by aesop

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

Goal state before:
pp: case mp.verts
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
x✝ : V
⊢ x✝ ∈ M'.verts ↔ x✝ ∈ ⊥.verts

Tactic:
grind [verts_bot]

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

Goal state before:
pp: case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ ∀ ⦃v w : W⦄, (Subgraph.map f H₁).Adj v w → (Subgraph.map f H₂).Adj v w

Tactic:
rintro _ _ ⟨u, v, ha, rfl, rfl⟩

Goal state after:
case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
u v : V
ha : H₁.Adj u v
⊢ (Subgraph.map f H₂).Adj (f u) (f v)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ Fintype.card ↑G.edgeSet - G.copyCount H = Fintype.card ↑G.edgeSet - Fintype.card { G' // Nonempty (H ≃g G'.coe) }

Tactic:
← Set.toFinset_card,

Goal state after:
case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeSet.toFinset - G.copyCount H = #G.edgeSet.toFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
by aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

Tactic:
by aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.getVert i ∈ p.support

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

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s✝ s : Set V
x✝ : ↑(G'.deleteVerts s).verts
v : V
hv : v ∈ (G'.deleteVerts s).verts
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∉ s}

Tactic:
by aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
h₁ : ¬p.Nil
h₂ : 0 < p.darts.length
⊢ p.firstDart h₁ = p.darts[0]

Tactic:
simp [Dart.ext_iff, firstDart_toProd, darts_getElem_eq_getVert]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : p.darts ≠ []
⊢ p.darts.getLast hnil = p.lastDart ⋯

Tactic:
grind [lastDart_eq, not_nil_iff_lt_length]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hnil : ¬p.Nil
⊢ p.lastDart hnil = p.darts.getLast ⋯

Tactic:
grind [lastDart_eq, not_nil_iff_lt_length]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 - ε ^ 5 / 50 ≤ 1 - 2 * (1 / (↑m + 1)) + (1 / (↑m + 1)) ^ 2

Tactic:
refine le_trans ?_ (le_add_of_nonneg_right <| sq_nonneg _)

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 - ε ^ 5 / 50 ≤ 1 - 2 * (1 / (↑m + 1))
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
i : ℕ
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
by
  induction p generalizing i <;> cases i <;> 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
q : G.Walk v w
i : ℕ
⊢ (p.append q).getVert i = if i ≤ p.length then p.getVert i else q.getVert (i - p.length)

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

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ (1 + 1 / ↑m) ^ 2 ≤ (1 + ε ^ 5 / 100) ^ 2

Tactic:
gcongr (1 + ?_) ^ 2
      rw [← one_div_div (100 : ℝ)]
      exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)

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

Goal state before:
pp: case refine_2.refine_3
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 ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      List.drop (s.length + p₁.length + 1) (s ++ p₁.support ++ t)

Tactic:
List.drop_append,

Goal state after:
case refine_2.refine_3
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 ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      (List.drop (s.length + p₁.length + 1) (s ++ p₁.support) ++
        List.drop (s.length + p₁.length + 1 - (s ++ p₁.support).length) t)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_2.refine_3
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 ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      (List.drop (s.length + p₁.length + 1) (s ++ p₁.support) ++
        List.drop (s.length + p₁.length + 1 - (s ++ p₁.support).length) t)

Tactic:
List.drop_append,

Goal state after:
case refine_2.refine_3
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 ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      (List.drop (s.length + p₁.length + 1) s ++ List.drop (s.length + p₁.length + 1 - s.length) p₁.support ++
        List.drop (s.length + p₁.length + 1 - (s ++ p₁.support).length) t)
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 : ℕ
⊢ (p.drop n).drop m = (p.drop (n + m)).copy ⋯ ⋯

Tactic:
by
  apply ext_support
  simp_rw [support_copy, drop_support_eq_support_drop_min, drop_length, List.drop_drop]
  grind

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ((cons h✝ p✝).concat h).dropLast = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
· rw! [concat_cons, dropLast_cons_of_not_nil] <;>
      simp [*, ← length_eq_zero_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
u : α
hu : u ∈ s
v : α
hv : v ∈ s
hne : u ≠ v
⊢ G.Adj u v

pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤

Tactic:
· simpa [← induce_adj (u := ⟨u, hu⟩) (v := ⟨v, hv⟩), h]

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : ⇑f '' s = ↑t
⊢ (⇑f '' s).Finite

Tactic:
by simp [hst]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) → (SimpleGraph.map (⇑f) G).IsClique ↑t

Tactic:
rintro ⟨s, hs, rfl⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
ht : (map f s).Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑(map f s)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Tactic:
← not_lt

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ↔ ¬1 < #t ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a e ∧ G.Adj b e ∧ {a, b, e} = {a, b, e}

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ G.Adj a d ∧ G.Adj b d ∧ {a, d, b} = {a, b, d}

Tactic:
by aesop

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsNClique n s ∧ map f s = t) → (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n

Tactic:
rintro ⟨s, hs, rfl⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
f : α ↪ β
s : Finset α
hs : G.IsNClique n s
⊢ (∃ s_1, G.IsClique ↑s_1 ∧ map f s_1 = map f s) ∧ #(map f s) = n