mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert j t

Tactic:
rw [r₁]; apply mem_insert_self

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₁ s * 0 + f₁ s * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₁ s * 0 + f₁ s * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
· rw [mul_zero, zero_add]
      refine (h ‹_› ‹_›).trans <| mul_le_mul ?_ (le_collapse_of_insert_mem ‹_› h₄
        (union_insert _ _ _) <| union_mem_sups ‹_› ‹_›) (h₄ _) <| collapse_nonneg h₃ _
      exact le_collapse_of_mem (notMem_mono inter_subset_left ‹_›) h₃
        (inter_insert_of_notMem ‹_›) <| inter_mem_infs ‹_› ‹_›

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₁ s * 0 + f₁ s * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring α
⊢ (G.recolorOfEmbedding f.symm.toEmbedding) ((G.recolorOfEmbedding f.toEmbedding) C) = C

Tactic:
ext v
    apply Equiv.symm_apply_apply

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ False

Tactic:
have hb' : ∀ p : G.Walk w v, s(w, v) ∈ p.edges := by
      intro p
      simpa [Sym2.eq_swap] using hb p.reverse

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
w : V
hwp : w ∈ p.support
hws : w ∉ s
⊢ False

Tactic:
exact hp.not_mem_support_of_subsingleton_neighborSet (by grind) (by grind) (hs _ hws) hwp

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.neighborFinset v ⊆ t

Tactic:
by
  classical
  rw [isBipartiteWith_neighborFinset h hv]
  exact filter_subset (G.Adj v ·) t

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk✝ : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < ↑k
⊢ ((G.deleteEdges {e}).deleteEdges s).Reachable u v

Tactic:
deleteEdges_deleteEdges,

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk✝ : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < ↑k
⊢ (G.deleteEdges ({e} ∪ s)).Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Tactic:
rename_i x y z
    have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
      ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩
    simp [ih, or_assoc, this]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ p✝.toSubgraph ⊔ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝) = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph

Tactic:
sup_comm

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ ⊔ p✝.toSubgraph = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]

Goal state after:
case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑(p.append q).length
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
⊢ G.Connected

Tactic:
have := (nonempty_prod.1 h.nonempty).1
  have := (nonempty_prod.1 h.nonempty).2
  exact ⟨h.preconnected.ofBoxProdLeft⟩

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H) → H.Preconnected

Tactic:
intro hw
    rw [Subgraph.preconnected_iff]
    rintro ⟨u, hu⟩ ⟨v, hv⟩
    obtain ⟨p, h⟩ := hw hu hv
    exact Reachable.map (Subgraph.inclusion h)
      (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ (induce (⋃₀ S) G).Connected

Tactic:
apply G.induce_connected_of_patches _ (Set.subset_sUnion_of_mem sS vs)

Goal state after:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ ∀ {v_1 : V}, v_1 ∈ ⋃₀ S → ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : v_1 ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨v_1, hv'⟩
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ (u v : V), Subsingleton (G.Path u v)

Tactic:
by
  refine ⟨fun h u v ↦ ⟨fun p q ↦ ?_⟩, fun h v c hc ↦ ?_⟩
  · have := p.isPath.exists_isCycle_of_ne q.isPath
    grind [IsAcyclic, Subtype.coe_inj]
  · have := h _ v |>.elim ⟨_, hc.isPath_tail⟩ ⟨_, .of_adj <| c.adj_snd hc.not_nil |>.symm⟩
    grind [length_cons, length_nil, hc.three_le_length, c.length_tail_add_one hc.not_nil]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ q.support

Tactic:
rw [← Subtype.mk.inj <| hG.subsingleton_path u w |>.elim ⟨p₀, hp₀⟩ ⟨q, hq⟩]

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ p₀.support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
by
  classical
  simp_rw [isTree_iff, isAcyclic_iff_subsingleton_path, subsingleton_iff]
  constructor
  · rintro ⟨hc, hu⟩
    refine ⟨hc.nonempty, ?_⟩
    intro v w
    let q := (hc v w).some.toPath
    use q
    simp only [true_and, Path.isPath]
    intro p hp
    specialize hu v w ⟨p, hp⟩ q
    exact Subtype.ext_iff.mp hu
  · rintro ⟨hV, h⟩
    refine ⟨Connected.mk ?_, ?_⟩
    · intro v w
      obtain ⟨p, _⟩ := h v w
      exact p.reachable
    · rintro v w ⟨p, hp⟩ ⟨q, hq⟩
      simp only [ExistsUnique.unique (h v w) hp hq]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
have : Finset.card ({default} : Finset V)ᶜ + 1 = Fintype.card V := by
    rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
⊢ G.edgeFinset.card + 1 = Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : extremalNumber (Fintype.card V) H < #G.edgeFinset
⊢ H ⊑ G

Tactic:
by
  contrapose h; push Not
  exact card_edgeFinset_le_extremalNumber h

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : Fintype V
R : Type u_3
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ ⌊m⌋₊ < extremalNumber (Fintype.card V) H ↔ ∃ G x, H.Free G ∧ ⌊m⌋₊ < #G.edgeFinset

Tactic:
exact lt_extremalNumber_iff H ⌊m⌋₊

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t

Tactic:
IsTuranMaximal,

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsExtremal fun x ↦ x.CliqueFree (r + 1)
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
⊢ ¬G.Adj t u

Tactic:
IsTuranMaximal,

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsExtremal fun x ↦ x.CliqueFree (r + 1)
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
⊢ ¬G.Adj t u
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.Connected
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Tactic:
by
  obtain hV | hV := (finite_or_infinite V).symm
  · simp
  have := Fintype.ofFinite
  obtain ⟨T, hle, hT⟩ := h.exists_isTree_le
  rw [Nat.card_eq_fintype_card, ← hT.card_edgeFinset, add_le_add_iff_right,
    Nat.card_eq_fintype_card, ← edgeFinset_card]
  exact Finset.card_mono <| by simpa

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
⊢ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length

Tactic:
intro _ w ho
    have := (w.three_le_chromaticNumber_of_odd_loop ho).trans h.chromaticNumber_le
    norm_cast

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (C.labelGraph k).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k

Tactic:
by
  rw [EdgeLabeling.labelGraph]
  simp only [mem_edgeSet, fromEdgeSet_adj, Set.mem_ofPred_eq, Ne.eq_def]
  grind [Adj.ne]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x y : V
⊢ (EdgeLabeling.labelGraph G.toTopEdgeLabeling 1).Adj x y ↔ G.Adj x y

Tactic:
simpa [imp_false] using G.ne_of_adj

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := ⋯
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ ¬G.IsTuranMaximal r

Tactic:
IsTuranMaximal,

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ ¬G.IsExtremal fun x ↦ x.CliqueFree (r + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := ⋯
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ¬G.IsTuranMaximal r

Tactic:
IsTuranMaximal,

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ¬G.IsExtremal fun x ↦ x.CliqueFree (r + 1)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ t * r * (r - 1) * t = r * (r - 1) * t ^ 2

Tactic:
mul_assoc t _ _,

Goal state after:
r t : ℕ
⊢ t * (r * (r - 1)) * t = r * (r - 1) * t ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case h₁
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⋯
⊢ ⇑(F c₁) ≍ ⇑(F c₂)

pp: case h₂
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⋯
⊢ v₁ ≍ v₁'

Tactic:
· rw [hc]

Goal state after:
case h₂
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⋯
⊢ v₁ ≍ v₁'
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ G.IsExtremal ⊤.Free ↔ G.IsTuranMaximal (Fintype.card α - 1)

Tactic:
IsTuranMaximal,

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ G.IsExtremal ⊤.Free ↔ G.IsExtremal fun x ↦ x.CliqueFree (Fintype.card α - 1 + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
v : Fin (n + r)
| ∑ i, if ↑v % r ≠ ↑i % r then 1 else 0

Tactic:
rw [Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0, sum_range_add]

Goal state after:
n r : ℕ
v : Fin (n + r)
| (∑ x ∈ range n, if ↑v % r ≠ x % r then 1 else 0) + ∑ x ∈ range r, if ↑v % r ≠ (n + x) % r then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Finite α
inst✝ : Nontrivial α
⊢ G.ediam ≠ ⊤ ↔ G.diam ≠ 0

Tactic:
not_iff_not,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : Finite α
inst✝ : Nontrivial α
⊢ G.ediam = ⊤ ↔ G.diam = 0
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
x✝¹ x✝ : V
w✝³ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝³
w✝² : Fin r
h₂ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝²
w✝¹ : Fin t
h₁' : f (w✝³, w✝¹) = x✝¹
w✝ : Fin t
h₂' : f (w✝², w✝) = x✝
heq : w✝³ = w✝²
⊢ x✝³ = x✝²

Tactic:
simp_rw [← h₁, ← h₂, heq]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
⊢ completeEquipartiteGraph (r + 1) t ⊑ G ↔ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Tactic:
· rw [completeEquipartiteGraph_isContained_iff]
    refine ⟨fun ⟨K'⟩ ↦ ?_, fun ⟨K, s, hs, hadj⟩ ↦ ?_⟩
    · obtain ⟨parts, hparts_sub, hparts_card⟩ := K'.parts.exists_subset_card_eq (Nat.pred_le _)
      let K : G.CompleteEquipartiteSubgraph r t := by
        refine ⟨parts, ?_, fun h ↦ K'.card_mem_parts (hparts_sub h),
          fun _ h₁ _ h₂ hne ↦ K'.isCompleteBetween (hparts_sub h₁) (hparts_sub h₂) hne⟩
        rw [hparts_card, K'.card_parts.resolve_right ht]
        exact .inl (Nat.pred_succ r)
      obtain ⟨s, nhs_mem, hs⟩ : ∃ s ∉ K.parts, insert s K.parts = K'.parts := by
        refine exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩
        rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]
      have hs_mem : s ∈ K'.parts := by simp [← hs]
      exact ⟨K, s, K'.card_mem_parts hs_mem,
        fun _ h ↦ K'.isCompleteBetween (hparts_sub h) hs_mem (ne_of_mem_of_not_mem h nhs_mem)⟩
    · refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
      · intro hs_mem
        obtain ⟨v, hv⟩ : s.Nonempty := by
          rw [← Finset.card_pos, hs]
          exact Nat.pos_of_ne_zero ht
        exact G.irrefl <| hadj s hs_mem hv hv
      · rw [Finset.card_cons, K.card_parts.resolve_right ht]
        exact .inl rfl
      · simp_rw [mem_cons, forall_eq_or_imp]
        exact ⟨hs, fun p ↦ K.card_mem_parts⟩
      · rw [coe_cons]
        have : Std.Symm G.IsCompleteBetween := by simp [symm_def, isCompleteBetween_comm]
        exact K.isCompleteBetween.insert_of_symm fun p hp _ ↦ hadj p hp |>.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ 2 * r * #(turanGraph n r).edgeFinset ≤ (r - 1) * n ^ 2

Tactic:
grw [card_edgeFinset_turanGraph, mul_add, Nat.mul_div_le]

Goal state after:
n r : ℕ
⊢ (n ^ 2 - (n % r) ^ 2) * (r - 1) + 2 * r * (n % r).choose 2 ≤ (r - 1) * n ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
by
  rcases r.eq_zero_or_pos with rfl | hr
  · rw [cliqueFree_one, ← Fintype.card_eq_zero_iff] at cf
    simp_rw [zero_tsub, mul_zero, Nat.mod_zero, Nat.div_zero, zero_add]
    exact card_edgeFinset_le_card_choose_two
  · obtain ⟨H, _, maxH⟩ := exists_isTuranMaximal (V := V) hr
    convert! maxH.2 cf
    rw [((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,
      card_edgeFinset_turanGraph]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : (⋃ i ∈ t, s i).Finite
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
← this.cast_ncard_eq,

Goal state after:
case pos
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : (⋃ i ∈ t, s i).Finite
⊢ ↑(⋃ i ∈ t, s i).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl.inr
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hcy : C y = C v
hx : x = w₁
hy : y ∈ ↑t
⊢ False

Tactic:
| inr hy =>

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M ⊔ M').Adj v w

Tactic:
sup_comm

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M' ⊔ M).Adj v w