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

Goal state before:
pp: case inr.inr.refine_1
α : 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
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Tactic:
[

Goal state after:
case inr.inr.refine_1
α : 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
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
⊢ ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right

Tactic:
[

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
⊢ ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : v = p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2

Tactic:
have : G.dist v w ≤ p.tail.tail.length := by
      simpa [hv, p.getVert_tail] using dist_le p.tail.tail

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this✝¹ : p.tail.tail.length < p.tail.length
this✝ : p.tail.length < p.length
hv : v = p.getVert 2
this : G.dist v w ≤ p.tail.tail.length
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ y ∈ (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯ ↔
    (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ y ∈ (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯ ↔
    (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G.neighborFinset x.1 ×ˢ {x.2}).card + ({x.1} ×ˢ H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G.neighborFinset x.1 ×ˢ {x.2}).card + ({x.1} ×ˢ H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊓ H).verts.Nonempty

Tactic:
exact ⟨u, by simp [uH]⟩

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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
⊢ (G ⊕g H).LocallyFinite

Tactic:
by
  rintro (v | w) <;> simp only [neighborSet_sum_inl, neighborSet_sum_inr] <;>
    infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ (hasse (α × β)).Adj x y ↔ (hasse α □ hasse β).Adj x y

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ (hasse (α × β)).Adj x y ↔ (hasse α □ hasse β).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph n).Copy G
this : n = n - 3 + 3
⊢ ∃ v p, p.IsCycle ∧ p.length = n

Tactic:
this

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph (n - 3 + 3)).Copy G
this : n = n - 3 + 3
⊢ ∃ v p, p.IsCycle ∧ p.length = n
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:
[

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 ⟨u', ⋯⟩ ⟨v', ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
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⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
[

Goal state after:
case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
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⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
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⟩
hne : x ≠ y
hle : x > y
hab : n + ↑⟨y, hy⟩ - ↑⟨x, hx⟩ = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
[

Goal state after:
case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
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⟩
hne : x ≠ y
hle : x > y
hab : n + ↑⟨y, hy⟩ - ↑⟨x, hx⟩ = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_2.refine_3
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
hlen : p.tail.support.length = n
this : ∀ (m : Fin n), p.support[m.succ] = p.tail.support[m]
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.support[n_1.succ], map_rel' := ⋯ }

Tactic:
[

Goal state after:
case refine_2.refine_3
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
hlen : p.tail.support.length = n
this : ∀ (m : Fin n), p.support[m.succ] = p.tail.support[m]
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.support[n_1.succ], map_rel' := ⋯ }
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_2.refine_3
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
hlen : p.tail.support.length = n
this : ∀ (m : Fin n), p.support[m.succ] = p.tail.support[m]
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.support[n_1.succ], map_rel' := ⋯ }

Tactic:
this

Goal state after:
case refine_2.refine_3
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
hlen : p.tail.support.length = n
this : ∀ (m : Fin n), p.support[m.succ] = p.tail.support[m]
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.tail.support[n_1], map_rel' := ⋯ }
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
⊢ ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right

Tactic:
[

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
⊢ ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
i : V ⊕ V
hi : i ∈ ↑(map Function.Embedding.inl left)
j : V ⊕ V
hj : j ∈ ↑(map Function.Embedding.inr right)
⊢ G.bipartiteDoubleCover.Adj i j

Tactic:
[

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
i : V ⊕ V
hi : i ∈ ↑(map Function.Embedding.inl left)
j : V ⊕ V
hj : j ∈ ↑(map Function.Embedding.inr right)
⊢ G.bipartiteDoubleCover.Adj i j
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case cons
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u✝ v✝ u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
ih : ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet

Tactic:
| @cons u v w h_adj p ih =>

Goal state after:
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:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath
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:
simp_rw [isTree_iff, isAcyclic_iff_subsingleton_path, subsingleton_iff]

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ (G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m

Tactic:
[

Goal state after:
V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ m < extremalNumber (Fintype.card V) H ↔ ∃ G x, H.Free G ∧ m < #G.edgeFinset

Tactic:
[

Goal state after:
V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ m < extremalNumber (Fintype.card V) H ↔ ∃ G x, H.Free G ∧ m < #G.edgeFinset
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
⊢ ↑(extremalNumber (Fintype.card V) H) ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → ↑(#G.edgeFinset) ≤ m

Tactic:
[

Goal state after:
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
⊢ ↑(extremalNumber (Fintype.card V) H) ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → ↑(#G.edgeFinset) ≤ m
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:
[

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq V
⊢ Matrix.compl 0 = adjMatrix α (completeGraph V)

Tactic:
by simp [← IsAdjMatrix.compl_inj]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
⊢ adjMatrix α h.toGraph = A

Tactic:
by
  ext i j
  obtain h' | h' := h.zero_or_one i j <;> simp [h']

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

Goal state before:
pp: n r : ℕ
⊢ turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r

Tactic:
[

Goal state after:
n r : ℕ
⊢ turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r
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
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
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset s ↔ v ∈ G.neighborFinset s

Tactic:
[

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
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
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset s ↔ v ∈ G.neighborFinset s
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
⊢ G.IsAcyclic

Tactic:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
⊢ G.IsAcyclic
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
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
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset u ↔ v ∈ G.neighborFinset u \ {t}

Tactic:
[

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
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
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset u ↔ v ∈ G.neighborFinset u \ {t}
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length

Tactic:
[

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ (Nonempty.some ⋯).length % 2 = (Nonempty.some ⋯).length % 2

Tactic:
[

Goal state after:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ (Nonempty.some ⋯).length % 2 = (Nonempty.some ⋯).length % 2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α},
    (completeMultipartiteGraph fun c ↦ { x // h.setoid c.out x }).Adj
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩, invFun := fun x ↦ ↑x.snd, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩, invFun := fun x ↦ ↑x.snd, left_inv := ⋯, right_inv := ⋯ } b) ↔
      G.Adj a b

Tactic:
[

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α},
    (completeMultipartiteGraph fun c ↦ { x // h.setoid c.out x }).Adj
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩, invFun := fun x ↦ ↑x.snd, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩, invFun := fun x ↦ ↑x.snd, left_inv := ⋯, right_inv := ⋯ } b) ↔
      G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
⊢ G.Adj
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        a✝)
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        b✝) ↔
    (pathGraph 3)ᶜ.Adj a✝ b✝

Tactic:
[

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
⊢ G.Adj
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        a✝)
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        b✝) ↔
    (pathGraph 3)ᶜ.Adj a✝ b✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| r * t

Tactic:
← Nat.sub_one_add_one_eq_of_pos v.2.pos,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| r * (t - 1 + 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 := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ G.CliqueFree r

Tactic:
[

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.CliqueFree r