mathlib-initiative/mathlib-tactics huggingface dataset:
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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) ≤ ↑(#s')
ht : ↑(#t) ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1

Tactic:
eq_of_subset_of_card_le hs' (Nat.cast_le.1 hs),

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) ≤ ↑(#s')
ht : ↑(#t) ≤ ↑(#t')
⊢ |↑(G.edgeDensity s t') - ↑(G.edgeDensity s t)| < 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case pos
α : 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
h₂ : G.IsUniform (ε / 8) 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

Tactic:
exact Or.inr <| Or.inr ⟨U, V, hU, hV, hUV, h' _ hU _ hV hx hy hUV h₂, hx, hy, h⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
⊢ G.deleteEdges s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'

Tactic:
deleteEdges,

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
⊢ G \ fromEdgeSet s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s

Tactic:
deleteEdges,

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G \ fromEdgeSet s = G ↔ Disjoint G.edgeSet s
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x : V
⊢ (G.deleteEdges (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x

Tactic:
deleteEdges,

Goal state after:
V : Type u_1
G : SimpleGraph V
x : V
⊢ (G \ fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
⊢ Disjoint H.verts H'.verts

Tactic:
S

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
⊢ S ⊆ H.verts → S ⊆ H'.verts → S ⊆ ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(P.energy G) + ε ^ 5 / 4 ≤ ↑((increment hP G ε).energy G)

Tactic:
by
  calc
    _ = (∑ x ∈ P.parts.offDiag, (G.edgeDensity x.1 x.2 : ℝ) ^ 2 +
          #P.parts ^ 2 * (ε ^ 5 / 4) : ℝ) / #P.parts ^ 2 := by
        rw [coe_energy, add_div, mul_div_cancel_left₀]; positivity
    _ ≤ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x,
          G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ #P.parts) / #P.parts ^ 2 := ?_
    _ = (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x,
          G.edgeDensity i.1 i.2 ^ 2 : ℝ) / #(increment hP G ε).parts ^ 2 := by
        rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm,
          div_mul_eq_div_div_swap, ← sum_div]; norm_num
    _ ≤ _ := by
        rw [coe_energy]
        gcongr
        rw [← sum_biUnion pairwiseDisjoint_distinctPairs]
        exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _
  gcongr
  rw [Finpartition.IsUniform, not_le, mul_tsub, mul_one, ← offDiag_card] at hPG
  calc
    _ ≤ ∑ x ∈ P.parts.offDiag, (edgeDensity G x.1 x.2 : ℝ) ^ 2 +
        (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := ?_
    _ = ∑ x ∈ P.parts.offDiag, ((G.edgeDensity x.1 x.2 : ℝ) ^ 2 +
        ((if G.IsUniform ε x.1 x.2 then (0 : ℝ) else ε ^ 4 / 3) - ε ^ 5 / 25) : ℝ) := by
        rw [sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, sum_ite, sum_const_zero,
          zero_add, sum_const, nsmul_eq_mul, ← Finpartition.nonUniforms, ← add_sub_assoc,
          add_sub_right_comm]
    _ = _ := (sum_attach ..).symm
    _ ≤ _ := sum_le_sum fun i _ ↦ le_sum_distinctPairs_edgeDensity_sq i hε₁ hPα hPε
  gcongr
  calc
    _ = (6 / 7 * #P.parts ^ 2) * ε ^ 5 * (7 / 24) := by ring
    _ ≤ #P.parts.offDiag * ε ^ 5 * (22 / 75) := by
        gcongr ?_ * _ * ?_
        · rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
          norm_cast
          rw [tsub_mul]
          refine le_tsub_of_add_le_left ?_
          nlinarith
        · norm_num
    _ = (#P.parts.offDiag * ε * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by ring
    _ ≤ (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by gcongr

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
⊢ Subgraph.map e.toHom ⊤ = ⊤

Tactic:
by
  ext <;> simp [Relation.Map, ← e.eq_symm_apply, ← e.map_rel_iff]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ H.Free (G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some}))

Tactic:
deleteEdges,

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ H.Free (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some}))
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
⊢ (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) ≤ ↑(#((star hP G ε hU V).biUnion id))

Tactic:
have hP₁ : 0 < #P.parts := Finset.card_pos.2 ⟨_, hU⟩

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) ≤ ↑(#((star hP G ε hU V).biUnion id))
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
hunion : (equitabilise h✝).parts = {u ∈ (equitabilise h✝).parts | #u = m} ∪ {u ∈ (equitabilise h✝).parts | #u = m + 1}
x : Finset α → Prop
ha : x ≤ fun u ↦ #u = m
hb : x ≤ fun u ↦ #u = m + 1
i : Finset α
h : x i
⊢ ⊥ i

Tactic:
apply succ_ne_self m _

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h✝).parts = {u ∈ (equitabilise h✝).parts | #u = m} ∪ {u ∈ (equitabilise h✝).parts | #u = m + 1}
x : Finset α → Prop
ha : x ≤ fun u ↦ #u = m
hb : x ≤ fun u ↦ #u = m + 1
i : Finset α
h : x i
⊢ m.succ = m
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H = G.singletonSubgraph v
⊢ H.verts = {v}

Tactic:
rw [h, singletonSubgraph_verts]

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

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (G.singletonSubgraph v).verts

Tactic:
rw [h, singletonSubgraph_verts]

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

Goal state before:
pp: case Adj.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (G.subgraphOfAdj hvw).Adj x✝¹ x✝
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff] at h

Goal state after:
case Adj.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : v = x✝¹ ∧ w = x✝ ∨ v = x✝ ∧ w = x✝¹
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ Walk.map (Hom.ofLE ⋯) (toDeleteEdges s p hp) = p

Tactic:
rw [← transfer_eq_map_ofLE, transfer_transfer, transfer_self]

Goal state after:
case hp
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet
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
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have := h.elim adj_of_infix_support (adj_of_infix_support · |>.symm)
    simpa [← isSubwalk_toWalk_iff_mem_edges this, isSubwalk_iff_support_isInfix]
  · have := (isSubwalk_toWalk_iff_mem_edges <| p.adj_of_mem_edges h).mpr h
    simpa [isSubwalk_iff_support_isInfix]

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

Goal state before:
pp: case succ
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
u : V
p : G.Walk u v
⊢ (p.drop (n✝ + 1 + 1)).IsSubwalk (p.drop (n✝ + 1))

Tactic:
| succ _ ih =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p✝ : G.Walk v✝ u
hp : (cons h p✝).IsCircuit
⊢ G ≠ ⊥

Tactic:
by rintro rfl; exact h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.snd = p.penultimate

Tactic:
by
  simpa using getVert_reverse p 1

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.penultimate = p.snd

Tactic:
by
  cases p <;> simp [snd, getVert_append]

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

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

Tactic:
simpa using hs.map (f := f)

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
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

Tactic:
simp [hs.card_eq, hs.isClique]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hab : a = b <;> by_cases hbc : b = c <;> by_cases hac : a = c

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h' : G.Adj u v✝
p : G.Walk v✝ u
x✝ : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
⊢ (cons h' p).IsCycle

Tactic:
refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h' : G.Adj u v✝
p : G.Walk v✝ u
x✝ : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v✝) ∈ p.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

Tactic:
eq_self_iff_true,

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ True
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ t, G.IsNClique n t
⊢ completeGraph (Fin n) ↪g induce (↑h.choose) G

Tactic:
rw [G.induce_eq_top.mpr h.choose_spec.isClique]

Goal state after:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ t, G.IsNClique n t
⊢ completeGraph (Fin n) ↪g ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

Tactic:
classical
  have (a b) (hab : a ≠ b) : {s ∈ (G.cliqueSet 3 : Set (Finset α)) | s(a, b) ∈ (s : Finset α).sym2}
    = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}} := by
    ext s
    simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq,
      mem_cliqueSet_iff, Set.mem_ofPred_eq,
      is3Clique_iff]
    constructor
    · rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, hab⟩
      simp only [mem_insert, mem_singleton] at hab
      obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
      any_goals
        simp only [*, adj_comm, true_and, Ne, not_true] at *
      any_goals
        first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩
    · rintro ⟨hab, c, hac, hbc, rfl⟩
      refine ⟨⟨a, b, c, ?_⟩, ?_⟩ <;> simp [*]
  constructor
  · rw [Sym2.forall]
    rintro hG a b hab
    simp only [Sym2.mk_isDiag_iff] at hab
    rw [this _ _ (Sym2.mk_isDiag_iff.not.2 hab)]
    rintro _ ⟨hab, c, hac, hbc, rfl⟩ _ ⟨-, d, had, hbd, rfl⟩
    refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩) <;>
      simp [is3Clique_triple_iff, *]
  · simp only [EdgeDisjointTriangles, is3Clique_iff, Set.Pairwise, mem_cliqueSet_iff, Ne,
      forall_exists_index, and_imp, ← Set.not_nontrivial_iff (s := _ ∩ _), not_imp_not,
      Set.Nontrivial, Set.mem_inter_iff, mem_coe]
    rintro hG _ a b c hab hac hbc rfl _ d e f hde hdf hef rfl g hg₁ hg₂ h hh₁ hh₂ hgh
    refine hG (Sym2.mk_isDiag_iff.not.2 hgh) ⟨⟨a, b, c, ?_⟩, by simpa using And.intro hg₁ hh₁⟩
      ⟨⟨d, e, f, ?_⟩, by simpa using And.intro hg₂ hh₂⟩ <;> simp [*]

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ ∀ (x y : α),
    G.Adj x y →
      x = a ∨ x = b ∨ x = c → y = a ∨ y = b ∨ y = c → s(x, y) = s(a, b) ∨ s(x, y) = s(a, c) ∨ s(x, y) = s(b, c)

Tactic:
rintro d e hde (rfl | rfl | rfl) (rfl | rfl | rfl) <;> simp [*] at *

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

Goal state before:
pp: α : Type u_1
R : Type u_2
s : Finset α
a : α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
hs : a ∈ s
⊢ ↑(#(s.erase a)) = ↑(#s) - 1

Tactic:
by
  rw [← card_erase_add_one hs, cast_add, cast_one, eq_sub_iff_add_eq]

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

Goal state before:
pp: case inl.refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ ε ^ 5 / 50 ≤ ε ^ 5 / 25

Tactic:
· exact div_le_div_of_nonneg_left (by sz_positivity) (by simp) (by norm_num)

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 : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ False

Tactic:
let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

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

Tactic:
← mul_assoc

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

Goal state before:
pp: ⊢ bitIndices 0 = []

Tactic:
simp [bitIndices]

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

Goal state before:
pp: ⊢ bitIndices 1 = [0]

Tactic:
simp [bitIndices]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
classical
  let s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
  have ⟨b, hb, hbmax⟩ := s'.exists_maximal ⟨a, by simp [s', has, hat]⟩
  simp only [s', mem_filter, and_imp] at hb hbmax
  have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1
  by_cases hcu : c ∈ u
  · exact ⟨c, hcu, hcs, hb.2.2.trans hbc⟩
  have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu
  have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd
  refine ⟨d, hdu, fun hds ↦ not_lt_iff_le_imp_ge.2 (hbmax hds hdt had) ?_, had⟩
  exact hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ + m₂✝) 1 * n✝ 2 - (m₁✝ + m₂✝) 2 * n✝ 1, (m₁✝ + m₂✝) 2 * n✝ 0 - (m₁✝ + m₂✝) 0 * n✝ 2,
      (m₁✝ + m₂✝) 0 * n✝ 1 - (m₁✝ + m₂✝) 1 * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1, m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2, m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0] +
      ![m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1, m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2, m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0]

Tactic:
vec3_add,

Goal state after:
case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ + m₂✝) 1 * n✝ 2 - (m₁✝ + m₂✝) 2 * n✝ 1, (m₁✝ + m₂✝) 2 * n✝ 0 - (m₁✝ + m₂✝) 0 * n✝ 2,
      (m₁✝ + m₂✝) 0 * n✝ 1 - (m₁✝ + m₂✝) 1 * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1 + (m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1),
      m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2 + (m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2),
      m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0 + (m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0)]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ + n₂✝) 2 - m✝ 2 * (n₁✝ + n₂✝) 1, m✝ 2 * (n₁✝ + n₂✝) 0 - m✝ 0 * (n₁✝ + n₂✝) 2,
      m✝ 0 * (n₁✝ + n₂✝) 1 - m✝ 1 * (n₁✝ + n₂✝) 0] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1, m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2, m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0] +
      ![m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1, m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2, m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0]

Tactic:
vec3_add,

Goal state after:
case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ + n₂✝) 2 - m✝ 2 * (n₁✝ + n₂✝) 1, m✝ 2 * (n₁✝ + n₂✝) 0 - m✝ 0 * (n₁✝ + n₂✝) 2,
      m✝ 0 * (n₁✝ + n₂✝) 1 - m✝ 1 * (n₁✝ + n₂✝) 0] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1 + (m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1),
      m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2 + (m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2),
      m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0 + (m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0)]