mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: 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
p : G.Walk w v
⊢ s(w, v) ∈ p.edges

Tactic:
simpa [Sym2.eq_swap] using hb p.reverse

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

Goal state before:
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 ∉ 𝒜
⊢ (0 + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
add_zero,

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 ∉ 𝒜
⊢ 0 * collapse ℬ a f₂ t ≤ 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 : ℕ
hc : G.Colorable n
s : Finset V
h : G.IsClique ↑s
hm : n < s.card
⊢ False

Tactic:
exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ G.neighborSet w ⊆ s

Tactic:
by
  rw [isBipartiteWith_neighborSet' h hw]
  exact Set.sep_subset s (G.Adj · w)

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

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

Tactic:
induction p with
  | nil => simp
  | cons _ _ _ =>
    simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
    rw [sup_comm]
    congr
    ext <;> simp [-Set.bot_eq_empty]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ x✝ : V
w✝¹ : α
left✝¹ : w✝¹ ∈ univ
hl : { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹ = x✝¹
w✝ : β
left✝ : w✝ ∈ univ
hr : { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝ = x✝
⊢ G.Adj ({ toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹) x✝

Tactic:
← hr

Goal state after:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ x✝ : V
w✝¹ : α
left✝¹ : w✝¹ ∈ univ
hl : { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹ = x✝¹
w✝ : β
left✝ : w✝ ∈ univ
hr : { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝ = x✝
⊢ G.Adj ({ toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹) ({ toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : v' ∈ w.toSubgraph.verts
⊢ v' ∈ G'.verts

Tactic:
rw [mem_verts_toSubgraph, mem_support_iff_exists_mem_edges_of_not_nil hnil] at hv'

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
⊢ v' ∈ G'.verts
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
⊢ #s * #t ≤ #(s ⊼ t) * #(s ⊻ t)

Tactic:
simpa using four_functions_theorem (1 : α → ℕ) 1 1 1 zero_le_one zero_le_one zero_le_one
    zero_le_one (fun _ _ ↦ le_rfl) s t

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

Goal state before:
pp: case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
this : (∑ a, g a) * ∑ a, (μ * f) a ≤ (∑ a ∈ univ ⊼ univ, f a) * ∑ a ∈ univ ⊻ univ, (μ * g) a
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a

Tactic:
simpa [hfg, sum_pos hg] using this

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = G.dist v u

Tactic:
dist,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ (G.edist u v).toNat = G.dist v u
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ (G.edist u v).toNat = G.dist v u

Tactic:
dist,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ (G.edist u v).toNat = (G.edist v u).toNat
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = 1 ↔ G.Adj u v

Tactic:
dist,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ (G.edist u v).toNat = 1 ↔ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
⊢ (cons x w').length = (cons x w').ofBoxProdLeft.length + (cons x w').ofBoxProdRight.length

Tactic:
unfold ofBoxProdLeft ofBoxProdRight

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
⊢ (cons x w').length =
    (Or.by_cases x (fun hG ↦ cons ⋯ w'.ofBoxProdLeft) fun hH ↦ ⋯ ▸ w'.ofBoxProdLeft).length +
      (⋯.by_cases (fun hH ↦ cons ⋯ w'.ofBoxProdRight) fun hG ↦ ⋯ ▸ w'.ofBoxProdRight).length
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_2.refine_2
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
⊢ ∀ {a_1 b : Fin n}, (cycleGraph n).Adj a_1 b → G.Adj p.support[a_1.succ] p.support[b.succ]

Tactic:
intro ⟨x, hx⟩ ⟨y, hy⟩ hab

Goal state after:
case refine_2.refine_2
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: case mp
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) → ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a

Tactic:
intro h g hg a ha
    exact h (a * g) a ha g hg (Or.inr rfl)

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})

Tactic:
mulCayley_union

Goal state after:
M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : Group M
⊢ mulCayley {1}ᶜ = ⊤

Tactic:
by
  simp [Set.compl_eq_univ_sdiff]

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

Goal state before:
pp: V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
⊢ (sSup Hs).IsAcyclic

Tactic:
rcases Hs.eq_empty_or_nonempty with rfl | hnemp

Goal state after:
case inl
V : Type u_1
h_acyc : ∀ H ∈ ∅, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ (sSup ∅).IsAcyclic

case inr
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
⊢ (sSup Hs).IsAcyclic
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A.compl.compl = A

Tactic:
ext
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `simp`. This is probably a problem at Mathlib's end rather than `grind`'s,
  as we are relying on seeing through the definition of `Matrix`, and `of`. The original proof was:
  `grind [of, compl, IsAdjMatrix]` -/
  simp [compl]; grind [compl, IsAdjMatrix]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : Zero α
inst✝ : One α
⊢ adjMatrix α ⊥ = 0

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(Fintype.card ↑{p | p.length = n})

Tactic:
card_set_walk_length_eq

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u 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
r : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
⊢ ¬G.CliqueFree r

Tactic:
rintro h

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
h : G.CliqueFree r
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

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

Tactic:
apply colorable_iff_forall_connectedComponent.2

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
⊢ ∀ (c : G.ConnectedComponent), c.toSimpleGraph.Colorable 2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : 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)
⊢ G ⊑ completeEquipartiteGraph n t

Tactic:
have F (c : Fin n) := Classical.arbitrary (C.colorClass c ↪ Fin t)

Goal state after:
α : 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
⊢ G ⊑ completeEquipartiteGraph n t
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ r ≤ #K.parts

Tactic:
K.card_parts.resolve_right ht

Goal state after:
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ r ≤ r
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_1
α : 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
i : Fin r
x✝¹ x✝ : Fin t
h : (fun j ↦ f (i, j)) x✝¹ = (fun j ↦ f (i, j)) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using f.injective h

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

Goal state before:
pp: case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ G.dist u v = G.ediam.toNat

Tactic:
dist,

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ (G.edist u v).toNat = G.ediam.toNat
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
⊢ (ComponentCompl.supp (↑e K)).Infinite

Tactic:
by
  refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)
  change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h
  exact ⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
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)

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

Goal state before:
pp: case neg.refine_2.refine_1
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
hs_mem : s ∈ K.parts
⊢ False

Tactic:
obtain ⟨v, hv⟩ : s.Nonempty := by
          rw [← Finset.card_pos, hs]
          exact Nat.pos_of_ne_zero ht

Goal state after:
case neg.refine_2.refine_1
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
hs_mem : s ∈ K.parts
v : V
hv : v ∈ s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ #K.parts + 1 = r + 1 ∨ t = 0

Tactic:
K.card_parts.resolve_right ht

Goal state after:
case neg.refine_2.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ r + 1 = r + 1 ∨ t = 0
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
⊢ ↑C ⊆ ↑(hom h C)

Tactic:
rintro c ⟨cL, rfl⟩
  exact ⟨fun h' => cL (h h'), rfl⟩

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

Goal state before:
pp: case neg.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)

Tactic:
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.Finsubgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
by
  rw [iSup, coe_sSup, iSup_range]

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : G.Finsubgraph
h : G'' ≤ G'
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
  refine ⟨fun ⟨v, hv⟩ => f.toFun ⟨v, h.1 hv⟩, ?_⟩
  rintro ⟨u, hu⟩ ⟨v, hv⟩ huv
  exact f.map_rel' (h.2 huv)

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| K.verts

Tactic:
unfold CompleteEquipartiteSubgraph.verts

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| K.parts.disjiUnion id ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst✝¹ : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ↑(#(G.overFin ⋯).edgeFinset) ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H ⊑ G

Tactic:
isContained_congr Iso.refl (G.overFinIso rfl)

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst✝¹ : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ↑(#(G.overFin ⋯).edgeFinset) ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H ⊑ G.overFin ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M₁ : G.Subgraph
h₁ : M₁ ∈ Set.ofPred IsMatching
M₂ : G.Subgraph
h₂ : M₂ ∈ Set.ofPred IsMatching
h : M₁.edgeSet = M₂.edgeSet
⊢ M₁.verts = M₂.verts

Tactic:
rw [h₁.verts_eq_biUnion_edgeSet, h₂.verts_eq_biUnion_edgeSet, h]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply,
    Set.indicator_apply, Pi.one_apply, sum_boole]
  convert! @Nat.cast_one R _
  convert! card_singleton s(a, b)
  rw [← coe_eq_singleton, coe_filter_univ]
  exact G.incidenceSet_inter_incidenceSet_of_adj h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ M, M.IsPerfectMatching

Tactic:
simp_rw [← @not_forall_not _ Subgraph.IsPerfectMatching]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ c, g c • G.lapMatrix_ker_basis_aux c) = fun i ↦ g (G.connectedComponentMk i)

Tactic:
simp only [lapMatrix_ker_basis_aux, SetLike.mk_smul_mk]

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ c, ⟨g c • fun i ↦ if G.connectedComponentMk i = c then 1 else 0, ⋯⟩) = fun i ↦ g (G.connectedComponentMk i)
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ G.ediam ≤ 2

Tactic:
ediam_le_iff

Goal state after:
case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ ∀ (u v : V), G.edist u v ≤ 2
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
hne : v ≠ w
ha : ¬G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ

Tactic:
rw [← h.of_not_adj hne ha]

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
hne : v ≠ w
ha : ¬G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this : IsAntichain H.Adj sᶜ
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
have : IsAntichain G.Adj (f ⁻¹' sᶜ) := this.preimage hf (fun _ _ hadj ↦ f.map_rel' hadj)

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this✝ : IsAntichain H.Adj sᶜ
this : IsAntichain G.Adj (⇑f ⁻¹' sᶜ)
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: ⊢ ↑⊥ = ∅

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
j : ℕ
⊢ ∃ i, (i, j) ∉ μ.cells

Tactic:
convert! μ.transpose.exists_notMem_row j using 1
  simp

Goal state after: