mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg
α : 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
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
left✝ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
ha : ¬0 < a
⊢ t ∉ {i ∈ R.parts | #i = m + 1}

Tactic:
intro H

Goal state after:
case neg
α : 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
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
left✝ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
ha : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj x w ↔ H.Adj w x

Tactic:
Subgraph.adj_comm

Goal state after:
case inr
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj w x ↔ H.Adj w x
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)

Tactic:
rintro e he

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
⊢ e ∈ Set.range (Sym2.map Subtype.val)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
⊢ Monotone (Subgraph.comap f)

Tactic:
intro H

Goal state after:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G'.Subgraph
⊢ ∀ ⦃b : G'.Subgraph⦄, H ≤ b → Subgraph.comap f H ≤ Subgraph.comap f b
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
h : H ≤ H'
⊢ ∀ ⦃v w : V⦄, (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w

Tactic:
intro v

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
h : H ≤ H'
v : V
⊢ ∀ ⦃w : V⦄, (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
hv : ¬G.IsIsolated v
⊢ G.degree v ≤ (induce s G).degree ⟨v, ⋯⟩

Tactic:
degree_induce_of_neighborSet_subset <| G.neighborSet_subset_support v |>.trans h

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
hv : ¬G.IsIsolated v
⊢ G.degree v ≤ G.degree ↑⟨v, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg
α : 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
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
h : ¬0 < a
⊢ t ∉ {i ∈ R.parts | #i = m + 1}

Tactic:
intro H

Goal state after:
case neg
α : 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
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
h : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False
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)
inst✝ : Fintype ↑(G'.spanningCoe.neighborSet v)
⊢ G'.spanningCoe.degree v = G'.degree v

Tactic:
by
  rw [← card_neighborSet_eq_degree, Subgraph.degree]
  congr!

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst✝¹ : Fintype ↑((toSubgraph H h).neighborSet v)
inst✝ : Fintype ↑(H.neighborSet v)
⊢ Fintype.card ↑((toSubgraph H h).neighborSet v) = H.degree v

Tactic:
refine (Finset.card_eq_of_equiv_fintype ?_).symm

Goal state after:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst✝¹ : Fintype ↑((toSubgraph H h).neighborSet v)
inst✝ : Fintype ↑(H.neighborSet v)
⊢ ↥(H.neighborFinset v) ≃ ↑((toSubgraph H h).neighborSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ Disjoint ({x ∈ (equitabilise h).parts | #x = m}) ({x ∈ (equitabilise h).parts | #x = m + 1})

Tactic:
aesop (add norm disjoint_filter)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ G.singletonSubgraph v ≤ H ↔ v ∈ H.verts

Tactic:
by
  refine ⟨fun h ↦ h.1 (Set.mem_singleton v), ?_⟩
  intro h
  constructor
  · rwa [singletonSubgraph_verts, Set.singleton_subset_iff]
  · exact fun _ _ ↦ False.elim

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ n * (#s / n) + #s % n = #s

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ #s % n + n * (#s / n) = #s
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ w = u ↔ u = w

Tactic:
eq_comm

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ u = w ↔ u = w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).coe ≤ G'.coe

Tactic:
intro v

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v : ↑(G'.deleteEdges s).verts
⊢ ∀ ⦃w : ↑(G'.deleteEdges s).verts⦄, (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
⊢ H.spanningCoe ≤ G

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v : V
⊢ ∀ ⦃w : V⦄, H.spanningCoe.Adj v w → G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
intro v

Goal state after:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v : V
⊢ ∀ ⦃w : V⦄, v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
⊢ (⊤.deleteVerts u).coe ≤ (⊤.deleteVerts u).coe

Tactic:
intro v

Goal state after:
V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
v : ↑(⊤.deleteVerts u).verts
⊢ ∀ ⦃w : ↑(⊤.deleteVerts u).verts⦄, (⊤.deleteVerts u).coe.Adj v w → (⊤.deleteVerts u).coe.Adj v w
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 = {u} + ↑p.support.tail

Tactic:
by cases p <;> rfl

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

Goal state before:
pp: case pos
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
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

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
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

Tactic:
· subst h'
      simp [dropUntil_first]

Goal state after:
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
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: 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

Tactic:
eq_comm

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
h' : u = u✝
⊢ List.count u (h'✝ ▸ nil).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: 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

Tactic:
eq_comm

Goal state after:
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
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1
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
h : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
⊢ s(u', v') ∈ p.edges

Tactic:
have := h.elim adj_of_infix_support (adj_of_infix_support · |>.symm)
    simpa [← isSubwalk_toWalk_iff_mem_edges this, isSubwalk_iff_support_isInfix]

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

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.append q).IsTrail ↔ p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges

Tactic:
by
  simp [Walk.isTrail_def, List.nodup_append']

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.tail.support

Tactic:
rw [support_tail_of_not_nil q hq]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.tail.support

Tactic:
rw [support_tail_of_not_nil q hq]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : w✝¹ ≠ w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)

Tactic:
← top_adj,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : ⊤.Adj w✝¹ w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ (∃ a, s = {a}) → G.IsClique ↑s

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique ↑{a}
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
⊢ p.snd ≠ p.penultimate

Tactic:
by
  intro h
  have := hp.three_le_length
  apply hp.getVert_injOn (by simp; lia) (by simp; lia) at h
  lia

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

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
v w : Fin n
hn : v ≠ w
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Tactic:
← top_adj,

Goal state after:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
v w : Fin n
hn : ⊤.Adj v w
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
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
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

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
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
· classical
    have ⟨w, hwp, hwq, hwu, hwv⟩ := hw
    by_cases! p.takeUntil w hwp ≠ q.takeUntil w hwq
    · have := ih _ (hs ▸ length_takeUntil_lt_length hwp hwv) (hp.takeUntil hwp) (hq.takeUntil hwq)
      grind [isSubwalk_takeUntil, IsSubwalk.trans]
    · have := ih _ (hs ▸ length_dropUntil_lt_length hwp hwu) (hp.dropUntil hwp) (hq.dropUntil hwq)
        <| by grind [take_spec]
      grind [isSubwalk_dropUntil, IsSubwalk.trans]

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
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
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 : V
p : G.Walk u v
hinj : Injective ⇑f
⊢ (List.map (Sym2.map ⇑f) p.edges).Nodup ↔ p.edges.Nodup

Tactic:
List.nodup_map_iff <| Sym2.map.injective hinj

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
⊢ p.edges.Nodup ↔ p.edges.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
⊢ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
intro H

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
⊢ ∀ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 < 1

Tactic:
calc
    _ ≤ (2 * ⌈4 / ε⌉₊ ^ 3 : ℝ)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 := by gcongr; exact min_le_left _ _
    _ = 2⁻¹ := by rw [mul_inv, inv_mul_cancel_right₀]; positivity
    _ < 1 := by norm_num

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

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n + n % k < k * (n / k) + n

Tactic:
add_comm,

Goal state after:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n % k + n < k * (n / k) + n
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ False

Tactic:
refine hG.not_ge (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(a = x ∧ c = z)

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(b = y ∧ c = z)

Tactic:
· rintro ⟨rfl, rfl⟩
    exact this rfl (ExplicitDisjoint.inj₁ habc hxyz) rfl

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(b = y ∧ c = z)
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A)
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ Set.InjOn (Prod.map Nat.cast Nat.cast) ↑A

Tactic:
have : Set.InjOn Nat.cast (range n) :=
        (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono (by simp; lia)

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A)
this✝² : ↑A = Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A
this✝¹ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this✝ : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
this : Set.InjOn Nat.cast ↑(range n)
⊢ Set.InjOn (Prod.map Nat.cast Nat.cast) ↑A