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

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (({b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}).sup' ⋯ fun x ↦ id x) =
    ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun i ↦ id i.1 ⊓ id i.2

Tactic:
simp_rw [← image_inf_product]

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 ↦ x1 ⊓ x2) ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b})).sup' ⋯ fun x ↦ id x) =
    ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun i ↦ id i.1 ⊓ id i.2
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ s ∧ compress u v a ∈ s ∨ a ∈ image (compress u v) s ∧ a ∉ s ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Tactic:
mem_image,

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ s ∧ compress u v a ∈ s ∨ (∃ a_1 ∈ s, compress u v a_1 = a) ∧ a ∉ s ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ a_1 ∈ s, compress u v a_1 = a
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜

Tactic:
simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
  aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ i ∈ 𝒜, t ∈ image (fun a ↦ insert a i) iᶜ) ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t

Tactic:
mem_image,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ i ∈ 𝒜, ∃ a ∈ iᶜ, insert a i = t) ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
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)

pp: case neg
α : 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_right h𝒜 hℬ, truncatedInf_of_notMem h𝒜,
      truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1, add_comm]

Goal state after:
case neg
α : 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)
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
hu : u = ⊥
hv : v = ⊥
⊢ (compress ⊥ v b ⊔ ⊥) \ v ∈ s

Tactic:
hv,

Goal state after:
case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
hu : u = ⊥
hv : v = ⊥
⊢ (compress ⊥ ⊥ b ⊔ ⊥) \ ⊥ ∈ s
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case ind.inr.zero
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
hm : 0 = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < 0 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

pp: case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
n✝ : ℕ
hm : n✝ + 1 = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < n✝ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
· cases h𝒜₁.card_pos.ne hm

Goal state after:
case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
n✝ : ℕ
hm : n✝ + 1 = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < n✝ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
⊢ t ∈ image (fun t ↦ s ∩ t) 𝒜 ↔ t ∈ s.powerset

Tactic:
mem_image,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
⊢ (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ∈ s.powerset
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ 0 < #U - 1

Tactic:
tsub_pos_iff_lt

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ 1 < #U
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr.refine_3
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ 0 < #U - 1

Tactic:
tsub_pos_iff_lt

Goal state after:
case inr.refine_3
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ 1 < #U
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ 𝒜.vcDim ≤ ℬ.vcDim

Tactic:
by unfold vcDim; gcongr

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ (∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp

Tactic:
refine ⟨fun ⟨_, ⟨hi, hi'⟩⟩ ↦ hi hi', ?_⟩

Goal state after:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ c'.supp → ∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
⊢ c = (puw.append pwv).append pvu

Tactic:
simp [puw, pwv, pvu]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
⊢ 2 ≤ G.chromaticNumber

Tactic:
refine le_of_not_gt fun h ↦ ?_
  obtain ⟨c⟩ := chromaticNumber_le_iff_colorable.mp (Order.le_of_lt_add_one h)
  exact c.valid hadj (Subsingleton.elim (c u) (c v))

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber ≤ ↑1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V

Tactic:
← Nat.cast_zero,

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber ≤ ↑1 ∧ ¬G.chromaticNumber ≤ ↑0 ↔ G = ⊥ ∧ ¬IsEmpty V
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, #(bipartiteAbove G.Adj t x) = ∑ w ∈ t.attach, #(bipartiteBelow G.Adj s ↑w)

Tactic:
sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ x ∈ s, #(bipartiteAbove G.Adj t x) = ∑ x ∈ t, #(bipartiteBelow G.Adj s x)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support ⊆ ↑s ∪ ↑t
⊢ ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset

Tactic:
← coe_union,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support ⊆ ↑(s ∪ t)
⊢ ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsEdgeConnected 2 ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).Preconnected

Tactic:
by
  simp [isEdgeConnected_add_one]

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
e : Sym2 V
⊢ e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u✝ : V
⊢ e ∈ nil.toSubgraph.edgeSet ↔ e ∈ nil.edges

case cons
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : e ∈ p✝.toSubgraph.edgeSet ↔ e ∈ p✝.edges
⊢ e ∈ (cons h✝ p✝).toSubgraph.edgeSet ↔ e ∈ (cons h✝ p✝).edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).toSubgraph = nil.toSubgraph ⊔ q.toSubgraph

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✝
p_ih✝ : ∀ (q : G.Walk w✝ w), (p✝.append q).toSubgraph = p✝.toSubgraph ⊔ q.toSubgraph
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).toSubgraph = (cons h✝ p✝).toSubgraph ⊔ q.toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
p : G.Walk u v
⊢ (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph

Tactic:
induction p

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u✝ : V
⊢ (Walk.map f nil).toSubgraph = Subgraph.map f nil.toSubgraph

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).toSubgraph = Subgraph.map f p✝.toSubgraph
⊢ (Walk.map f (cons h✝ p✝)).toSubgraph = Subgraph.map f (cons h✝ p✝).toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
← hi.1,

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (induce {u, v} G).Connected

Tactic:
by
  rw [connected_induce_iff]
  exact Subgraph.top_induce_pair_connected_of_adj huv

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

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
⊢ (G ⊕g H).neighborSet (Sum.inl v) = Sum.inl '' G.neighborSet v

Tactic:
ext (v' | w')

Goal state after:
case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inl v' ∈ Sum.inl '' G.neighborSet v

case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inr w' ∈ Sum.inl '' G.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
⊢ (G ⊕g H).neighborSet (Sum.inr w) = Sum.inr '' H.neighborSet w

Tactic:
ext (v' | w')

Goal state after:
case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inl v' ∈ Sum.inr '' H.neighborSet w

case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inr w' ∈ Sum.inr '' H.neighborSet w
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
x✝¹ x✝ : Fin (cycle n).tail.support.length
i : ℕ
hi✝ : i < (cycle n).tail.support.length
hi : i < (cycle n).support.tail.length
j : ℕ
hj✝ : j < (cycle n).tail.support.length
hj : j < (cycle n).support.tail.length
hij : (cycle n).getVert (i + 1) = (cycle n).getVert (j + 1)
⊢ ⟨i, hi✝⟩ = ⟨j, hj✝⟩

Tactic:
grind [← Nat.mod_eq_of_lt, cycleGraph.getVert_cycle]

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

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

Tactic:
ha

Goal state after:
case mp
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
h : ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
g : M
hg : g ∈ s
a : M
ha : ¬a * g = a
⊢ G.Adj (a * g) a
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : Group M
⊢ mulCayley Set.univ = ⊤

Tactic:
ext _ _
  simp [mulCayley_adj]

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
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
⊢ ∀ (ha₁ : a ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a = a₂

Tactic:
ha

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
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
⊢ ∀ (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a = a₂
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : DecidableEq α
inst✝¹ : AddMonoid α
inst✝ : One α
⊢ 1 + adjMatrix α G + (adjMatrix α G).compl = of 1

Tactic:
by
  aesop (add simp [add_assoc])

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)

Tactic:
by
  by_cases huv : u = v
  · grind [sup_eq_left, edge_le, Sym2.mem_diagSet, Sym2.mk_isDiag_iff]
  by_cases hadj : G.Adj u v
  · grind [sup_eq_left, edge_le, mem_edgeSet]
  refine ⟨?_, fun ⟨hacyc, hreach⟩ ↦ hacyc.sup_edge_of_not_reachable <| by grind⟩
  refine fun hacyc ↦ ⟨hacyc.anti le_sup_left, fun hreach ↦ False.elim ?_⟩
  refine isAcyclic_iff_forall_isBridge.mp (e := s(u, v)) hacyc (by simp [huv]) ?_
  convert! hreach
  simp [deleteEdges_sup, hadj]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
⊢ a ∈ s → a ∉ c.supp

Tactic:
ha

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
ha : a ∈ s
⊢ a ∉ c.supp
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a.e_a.e_a
n r : ℕ
⊢ (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = n * (r - 1)

Tactic:
conv_rhs => rw [← card_range n, ← smul_eq_mul, ← sum_const]

Goal state after:
case e_a.e_a.e_a
n r : ℕ
⊢ (∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) = ∑ _x ∈ range n, (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case h
α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
w : α
hw : G.eccent w = G.radius
v : α
hv : G.edist w v = G.eccent w
⊢ G.edist w v = G.radius

Tactic:
hv,

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
w : α
hw : G.eccent w = G.radius
v : α
hv : G.edist w v = G.eccent w
⊢ G.eccent w = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : ⨅ a, ⨅ x, ↑(↑x).length ≠ ⊤
⊢ ∃ a w, w.IsCycle ∧ ⨅ a, ⨅ x, ↑(↑x).length = ↑w.length

Tactic:
iInf_sigma',

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
h : ⨅ x, ↑(↑x.snd).length ≠ ⊤
⊢ ∃ a w, w.IsCycle ∧ ⨅ x, ↑(↑x.snd).length = ↑w.length
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case hb
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : completeBipartiteGraph (Fin s) (Fin t) ⊑ G.bipartiteDoubleCover
⊢ completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t)

Tactic:
exact completeBipartiteGraphCongr
      (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)

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

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ (⋃ i_1 ∈ insert i (t \ {i}), s i_1).encard = ∑ᶠ (i_1 : ι) (_ : i_1 ∈ insert i (t \ {i})), (s i_1).encard

Tactic:
finsum_mem_insert _ (notMem_sdiff_of_mem <| mem_singleton i) ht.sdiff

Goal state after:
case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ (⋃ i_1 ∈ insert i (t \ {i}), s i_1).encard = (s i).encard + ∑ᶠ (i_1 : ι) (_ : i_1 ∈ t \ {i}), (s i_1).encard
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'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
p : Finset (Fin n)
hp : p ∈ K.parts
⊢ t ≤ #p

Tactic:
K.card_mem_parts hp

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
p : Finset (Fin n)
hp : p ∈ K.parts
⊢ t ≤ t'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : M.IsMatching
⊢ Even M.verts.toFinset.card

Tactic:
by
  classical
  rw [isMatching_iff_forall_degree] at h
  use M.coe.edgeFinset.card
  rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
  simp [h, Finset.card_univ]

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

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ x ⬝ᵥ (degMatrix R G *ᵥ x - adjMatrix R G *ᵥ x) = (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
dotProduct_sub,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ x ⬝ᵥ degMatrix R G *ᵥ x - x ⬝ᵥ adjMatrix R G *ᵥ x = (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
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
hMmatch : (M.induce (Subtype.val '' (↑c).supp)).IsMatching
⊢ False

Tactic:
apply Nat.not_even_iff_odd.2 c.prop

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
⊢ Even (↑c).supp.ncard