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

Goal state before:
pp: case pos
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∈ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

pp: case neg
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
· exact Or.inr hw

Goal state after:
case neg
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
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 □ H).degree x = G.degree x.1 + H.degree x.2

Tactic:
degree,

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 □ H).neighborFinset x).card = G.degree x.1 + H.degree x.2
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 □ H).neighborFinset x).card = G.degree x.1 + H.degree x.2

Tactic:
degree,

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 □ H).neighborFinset x).card = (G.neighborFinset x.1).card + H.degree x.2
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 □ H).neighborFinset x).card = (G.neighborFinset x.1).card + H.degree x.2

Tactic:
degree,

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 □ H).neighborFinset x).card = (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case neg.refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : ↑w.length = (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ ↑(w.ofBoxProdLeft.length + w.ofBoxProdRight.length)

Tactic:
exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)

Goal state after:
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 j : V ⊕ V
hi : ∃ a ∈ left, Function.Embedding.inl a = i
hj : ∃ a ∈ right, Function.Embedding.inr a = j
⊢ G.bipartiteDoubleCover.Adj i j

Tactic:
Function.Embedding.inl_apply,

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 j : V ⊕ V
hj : ∃ a ∈ right, Function.Embedding.inr a = j
hi : ∃ a ∈ left, Sum.inl a = i
⊢ G.bipartiteDoubleCover.Adj i j
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
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
← this,

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

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
intro G

Goal state after:
case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
⊢ G ∈ {G | H.Free G} → #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
intro G

Goal state after:
case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
⊢ G ∈ {G | H.Free G} → #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
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:
simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.lt_sup_iff, mem_filter_univ]
  exact ⟨fun ⟨_, h, h'⟩ ↦ ⟨_, _, h, h'⟩, fun ⟨_, _, h, h'⟩ ↦ ⟨_, h, by convert!
    h'⟩⟩

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

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂

Tactic:
intro G

Goal state after:
case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
⊢ ∀ [inst : DecidableRel G.Adj], H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁

Tactic:
intro G

Goal state after:
case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
⊢ ∀ [inst : DecidableRel G.Adj], H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
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
⊢ (G.replaceVertex s t).degree u = G.degree u - 1

Tactic:
degree,

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
⊢ #((G.replaceVertex s t).neighborFinset u) = G.degree u - 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 : ℕ
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
⊢ #((G.replaceVertex s t).neighborFinset u) = G.degree u - 1

Tactic:
degree,

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
⊢ #((G.replaceVertex s t).neighborFinset u) = #(G.neighborFinset u) - 1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this : G.edgeFinset.card + 1 = Fintype.card V
⊢ G.minDegree = 1

Tactic:
have := G.sum_degrees_eq_twice_card_edges

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
⊢ G.minDegree = 1
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
⊢ 3 ≤ (cycleGraph n).chromaticNumber

Tactic:
let w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)

Goal state after:
case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
⊢ 3 ≤ (cycleGraph n).chromaticNumber
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
    intro c
    obtain ⟨_, hv⟩ := c.nonempty_supp
    use fun a ↦ Fin.ofNat 2 (c.connected_toSimpleGraph ⟨_, hv⟩ a).some.length
    intro a b hab he
    apply h _ <| (((c.connected_toSimpleGraph ⟨_, hv⟩ a).some.concat hab).append
                 (c.connected_toSimpleGraph ⟨_, hv⟩ b).some.reverse).map c.toSimpleGraph_hom
    rw [length_map, length_append, length_concat, length_reverse, add_right_comm]
    have : ((Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ a)).length) % 2 =
        (Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ b)).length % 2 := by
      simp_rw [← Fin.val_natCast, ← Fin.ofNat_eq_cast, he]
    exact (Nat.even_iff.mpr (by lia)).add_one

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : V), ⊤.Adj x y → (if G.Adj y x then 1 else 0) = if G.Adj x y then 1 else 0

Tactic:
simp [G.adj_comm]

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

Goal state before:
pp: r t : ℕ
⊢ #univ • ((r - 1) * t) = 2 * (r.choose 2 * t ^ 2)

Tactic:
smul_eq_mul,

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.parts • t = r * t

Tactic:
smul_eq_mul,

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.parts * t = r * t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ ∑ v, (turanGraph (n + r) r).degree v = ∑ v, (turanGraph n r).degree v + 2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
degree,

Goal state after:
n r : ℕ
⊢ ∑ x, #((turanGraph (n + r) r).neighborFinset x) =
    ∑ x, #((turanGraph n r).neighborFinset x) + 2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
· obtain ⟨u, v, huv⟩ := exists_edist_eq_ediam_of_ne_top <| ediam_ne_top_of_diam_ne_zero h
    use u, v
    rw [diam, dist, congrArg ENat.toNat huv]

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.ediam ≤ 2 * G.radius

Tactic:
apply le_trans (h ▸ G.edist_triangle (v := w))

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.edist w✝¹ w + G.edist w w✝ ≤ 2 * G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (induce (↑∅)ᶜ G).ConnectedComponent

Tactic:
rw [Finset.coe_empty, Set.compl_empty]

Goal state after:
case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (induce Set.univ G).ConnectedComponent
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
⊢ ∀ ⦃G : SimpleGraph (Fin (n + 1))⦄ [inst : DecidableRel G.Adj],
    H.Free G → ↑(#G.edgeFinset) ≤ ↑(extremalNumber n H) / ↑(n.choose 2) * ↑((n + 1).choose 2)

Tactic:
intro G

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
⊢ ∀ [inst : DecidableRel G.Adj],
    H.Free G → ↑(#G.edgeFinset) ≤ ↑(extremalNumber n H) / ↑(n.choose 2) * ↑((n + 1).choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
intro G

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
⊢ G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G →
    #G.edgeFinset ≤ {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ ∀ (b : SimpleGraph (V ⊕ W)),
    b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
          #x.edgeFinset

Tactic:
intro G

Goal state after:
case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
⊢ G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G →
    #G.edgeFinset ≤
      {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
        #x.edgeFinset
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✝¹ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs✝ : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs : s ⊆ {v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v} ∧ #s = t
hs' : s ∈ powersetCard t p
w : Fin n
hw✝ : w ∈ s
hw : w ∈ {v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}
⊢ ?m.327 hs' w hw✝

Tactic:
rwa [mem_filter, between_adj] at hw

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.IsAcyclic
⊢ G.girth = 0

Tactic:
by simp [girth, h]

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

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
| m + n

Tactic:
← Fintype.card_fin (m + n)

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
| Fintype.card (Fin (m + n))
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: 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],
    (completeBipartiteGraph α β).Free G → ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2

Tactic:
intro G

Goal state after:
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], (completeBipartiteGraph α β).Free G → ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
left✝ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
⊢ p₁ ∪ p₂ = Set.univ

Tactic:
refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
left✝ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
x : V
⊢ x ∈ p₁ ∪ p₂
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})
⊢ ∑ w ∈ W, G.degree w = ∑ v, #(G.neighborFinset v ∩ W)

Tactic:
degree,

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})
⊢ ∑ w ∈ W, #(G.neighborFinset w) = ∑ v, #(G.neighborFinset v ∩ W)
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
⊢ ↑t / (↑r * ε) < ↑⌊↑t / (↑r * ε)⌋₊ + 1

Tactic:
exact Nat.lt_floor_add_one (t / (r * ε))

Goal state after: