mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case nil.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ : U
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ →
    ⟨u, Path.nil⟩ = ⟨u, Path.nil⟩

pp: case nil.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₂, p₂.cons e₂⟩ →
    ⟨u, Path.nil⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
· intro; rfl

Goal state after:
case nil.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨y₂, p₂.cons e₂⟩ →
    ⟨u, Path.nil⟩ = ⟨y₂, p₂.cons e₂⟩
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
⊢ ∀ x ∈ Finset.antidiagonal t, coeff x.1 (h i) * coeff x.2 (∏ r ∈ S i, (X i - C r)) = 0

Tactic:
rintro ⟨p, q⟩ hpq

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : (p, q) ∈ Finset.antidiagonal t
⊢ coeff (p, q).1 (h i) * coeff (p, q).2 (∏ r ∈ S i, (X i - C r)) = 0
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
⊢ {b}.truncatedInf a = if b ≤ a then b else ⊥

Tactic:
simp only [truncatedInf, coe_singleton, upperClosure_singleton, UpperSet.mem_Ici_iff,
    id_eq]

Goal state after:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
⊢ (if h : b ≤ a then {b ∈ {b} | b ≤ a}.inf' ⋯ fun x ↦ x else ⊥) = if b ≤ a then b else ⊥
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
hℬ : s ∉ lowerClosure ↑ℬ
⊢ #(𝒜.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #⊤

Tactic:
truncatedSup_infs_of_notMem fun h ↦ hℬ h.2

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
hℬ : s ∉ lowerClosure ↑ℬ
⊢ #(𝒜.truncatedSup s) + #⊤ = #(𝒜.truncatedSup s) + #⊤
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
hℬ : s ∈ upperClosure ↑ℬ
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
rw [truncatedInf_union h𝒜 hℬ, truncatedInf_sups h𝒜 hℬ]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
hℬ : s ∈ upperClosure ↑ℬ
⊢ #(𝒜.truncatedInf s ⊓ ℬ.truncatedInf s) + #(𝒜.truncatedInf s ⊔ ℬ.truncatedInf s) =
    #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s

Tactic:
refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩

Goal state after:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s) → s ∈ ∂⁺ ^[0] 𝒜
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b : α
⊢ lift a < lift b ↔ lift a ≤ lift b ∧ ¬lift b ≤ lift a

Tactic:
by simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b : α
⊢ comp a < comp b ↔ comp a ≤ comp b ∧ ¬comp b ≤ comp a

Tactic:
by simp [lt_iff_le_not_ge]

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

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ ↑s ∪ compl '' ↑s = univ

Tactic:
image_eq_preimage_of_inverse compl_compl compl_compl

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ ↑s ∪ compl ⁻¹' ↑s = univ
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 β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)

Tactic:
exact le_add_of_nonneg_right <| hf _

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

pp: case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
h : ∃ t, (↑t).Intersecting ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
· exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩

Goal state after:
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
h : ∃ t, (↑t).Intersecting ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k → s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
· rintro ⟨⟨t, ht, hst⟩, hs⟩
    by_cases h : s ∈ 𝒜
    · exact Or.inl ⟨h, hs⟩
    obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_notMem h).symm)
    refine Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, ?_⟩, a, mem_insert_self _ _, erase_insert ha⟩
    rw [card_insert_of_notMem ha, hs]

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

Goal state before:
pp: V : Type u
⊢ ⊥.Connected ↔ Subsingleton V ∧ Nonempty V

Tactic:
by
  simp [preconnected_bot_iff_subsingleton, connected_iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : G.connectedComponentMk a = j✝
⊢ False

Tactic:
rw [hsx] at hsy

Goal state after:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : i✝ = j✝
⊢ False
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.degree v ≤ #t

Tactic:
← card_neighborFinset_eq_degree

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.degree w ≤ #s

Tactic:
← card_neighborFinset_eq_degree

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ #(G.neighborFinset w) ≤ #s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ x ∈ s.attach, G.degree ↑x = ∑ x ∈ t.attach, G.degree ↑x

Tactic:
← card_neighborFinset_eq_degree

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ x ∈ s.attach, #(G.neighborFinset ↑x) = ∑ x ∈ t.attach, #(G.neighborFinset ↑x)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : ↑H.verts
inst✝ : Fintype ↑(H.neighborSet ↑v)
⊢ H.degree ↑v = 0 ↔ H.verts.Subsingleton

Tactic:
refine ⟨fun hv ↦ Set.not_nontrivial_iff.mp fun hn ↦ ?_, (degree_eq_zero_of_subsingleton H _ ·)⟩

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : ↑H.verts
inst✝ : Fintype ↑(H.neighborSet ↑v)
hv : H.degree ↑v = 0
hn : H.verts.Nontrivial
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n m : ℕ
h : m + 1 < n + 3
⊢ (cycleGraph (n + 3)).Adj ⟨m + 1, h⟩ ⟨m, ⋯⟩

Tactic:
simp [cycleGraph_adj, Fin.ext_iff, Fin.sub_val_of_le]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : ↑G'.verts
hu : u ∈ G''.verts
hfu : f u = u'
v' : V
v : ↑G'.verts
hv : v ∈ G''.verts
hfv : f v = v'
⊢ (Subgraph.map f G'').coe.Reachable ⟨u', ⋯⟩ ⟨v', ⋯⟩

Tactic:
← hfu,

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : ↑G'.verts
hu : u ∈ G''.verts
hfu : f u = u'
v' : V
v : ↑G'.verts
hv : v ∈ G''.verts
hfv : f v = v'
⊢ (Subgraph.map f G'').coe.Reachable ⟨f u, ⋯⟩ ⟨v', ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

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

Tactic:
← Set.sdiff_union_inter s {1}

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

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝² : ∃ G, p G
G : SimpleGraph V
hp✝ : p G
G' : SimpleGraph V
hp' : G' ∈ {G | p G}
h : ∀ x' ∈ {G | p G}, #x'.edgeFinset ≤ #G'.edgeFinset
x✝¹ : SimpleGraph V
x✝ : DecidableRel x✝¹.Adj
hp : p x✝¹
⊢ #x✝¹.edgeFinset ≤ #G'.edgeFinset

Tactic:
convert! h _ (by simpa using hp)

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : DecidableEq V
inst✝ : Ring α
⊢ adjMatrix α ⊤ = of fun i j ↦ if i = j then 0 else 1

Tactic:
by
  ext i j
  cases eq_or_ne i j <;> simp [‹_›]

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 : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
h : G.CliqueFree r
⊢ False

Tactic:
obtain ⟨K, _, rfl⟩ := exists_subset_card_eq hn

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
K : Finset V
left✝ : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
hacyc : (G ⊔ edge u v).IsAcyclic
hreach : G.Reachable u v
⊢ False

Tactic:
refine isAcyclic_iff_forall_isBridge.mp (e := s(u, v)) hacyc (by simp [huv]) ?_

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
hacyc : (G ⊔ edge u v).IsAcyclic
hreach : G.Reachable u v
⊢ ((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e
⊢ (F ⊔ fromEdgeSet {e}).deleteEdges {e} = F

Tactic:
simpa using heF

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

Goal state before:
pp: V : Type u_1
inst✝ : Nonempty V
T : SimpleGraph V
⊢ Maximal IsAcyclic T ↔ T.IsTree

Tactic:
simp [← connected_top.maximal_le_isAcyclic_iff_isTree le_top]

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
hEven : Even n
⊢ (cycleGraph n).chromaticNumber = 2

Tactic:
have hc := (cycleGraph.bicoloring_of_even n hEven).colorable

Goal state after:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber = 2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_2
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
⊢ ↑v / r < t

Tactic:
· exact Nat.div_lt_of_lt_mul v.prop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2

Tactic:
by
  refine ⟨fun h _ _ hne he ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨w, hw⟩ := exists_isCycle_of_two_le_isEdgeReachable hne le_rfl he
    exact h w hw
  · rw [isAcyclic_iff_forall_isBridge]
    rintro ⟨u, v⟩ huv
    exact (isBridge_iff_not_isEdgeReachable_two huv).mpr (h huv.ne)

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

Goal state before:
pp: case inl
α : Type u_1
h✝ : Subsingleton α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

pp: case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

Tactic:
· exact Or.inl ediam_eq_zero_of_subsingleton

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.ediam.toNat = 1

Tactic:
ediam_top,

Goal state after:
α : Type u_1
inst✝ : Nontrivial α
⊢ ENat.toNat 1 = 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
⊢ ⊤.center = Set.univ

Tactic:
by
  cases subsingleton_or_nontrivial α
  · exact center_eq_univ_of_subsingleton
  · rw [Set.eq_univ_iff_forall]
    intro u
    rw [mem_center_iff, eccent_top, radius_top]

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

Goal state before:
pp: case neg.refine_2.refine_3
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
⊢ ∀ {p : Finset V}, p ∈ cons s K.parts ⋯ → #p = t

Tactic:
simp_rw [mem_cons, forall_eq_or_imp]
        exact ⟨hs, fun p ↦ K.card_mem_parts⟩

Goal state after:
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
D : G.ComponentCompl K
⊢ hom h C = D ↔ ¬Disjoint ↑C ↑D

Tactic:
by
  rw [Set.not_disjoint_iff]
  constructor
  · rintro rfl
    refine C.ind fun x xnL => ?_
    exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩
  · refine C.ind fun x xnL => ?_
    rintro ⟨x, ⟨_, e₁⟩, _, rfl⟩
    rw [← e₁]
    rfl

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ ↑(extremalNumber n H) / ↑(n.choose 2) ≤ ↑(extremalNumber m H) / ↑(m.choose 2)

Tactic:
exact antitoneOn_extremalNumber_div_choose_two H hm (hm.trans hn) hn

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ v, #(G.neighborFinset v ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)

Tactic:
← union_compl X,

Goal state after:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ x ∈ X ∪ Xᶜ, #(G.neighborFinset x ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
⊢ G.Reachable a b

Tactic:
have a_mem := hp.mem_support a

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
a_mem : a ∈ p.support
⊢ G.Reachable a b
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : MulZeroOneClass R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
a : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a

Tactic:
convert! one_ne_zero.ite_eq_left_iff
  infer_instance

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
h1_le_rε : 1 / ↑r - ε ≤ 0
⊢ ↑n ≤ ↑G.minDegree

Tactic:
← le_sub_self_iff 1,

Goal state after:
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
h1_le_rε : 1 ≤ 1 - (1 / ↑r - ε)
⊢ ↑n ≤ ↑G.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v w : V
hw : M.Adj v w
⊢ v ∈ M.verts

Tactic:
exact M.edge_vert hw

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : Set V
hc : G.IsClique u
hu : u.Finite
⊢ (∃ M, M.verts = u ∧ M.IsMatching) → Even u.ncard

Tactic:
rintro ⟨M, rfl, hMr⟩
    simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset,
      ← Set.toFinset_card] using! @hMr.even_card _ _ _ hu.fintype

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
⊢ False

Tactic:
have hMmatch : (M.induce c.val.supp).IsMatching := by
    intro v hv
    obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
    obtain ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ := hv
    use w
    have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
    refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
    apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
    simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_sdiff, Set.mem_univ, true_and,
      Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
      and_true] at hv' ⊢
    trivial

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
hMmatch : (M.induce (Subtype.val '' (↑c).supp)).IsMatching
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₁ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₁ z}) ≤ 2
haj : ¬G.Adj w₁ a
hbj : ¬G.Adj w₁ b
hcj : ¬G.Adj w₁ a
hdj : ¬G.Adj w₁ b
hax : ¬w₁ = a
⊢ False

Tactic:
· exact haj <| hw.isNClique_fst_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax

Goal state after: