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

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

Tactic:
unfold vcDim

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ 𝒜.shatterer.sup card ≤ ℬ.shatterer.sup card
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ (ker f).classes ⊆ Set.range fun y ↦ {x | f x = y}

Tactic:
rintro s ⟨x, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ {x_1 | (ker f) x_1 x} ∈ Set.range fun y ↦ {x | f x = y}
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } r ≤
      { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } s ↔
    r ≤ s

Tactic:
conv_rhs => rw [← mkClasses_classes r, ← mkClasses_classes s]

Goal state after:
α : Type u_1
r s : Setoid α
⊢ { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } r ≤
      { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } s ↔
    mkClasses r.classes ⋯ ≤ mkClasses s.classes ⋯
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr.convert_5
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝³ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r ↑(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
rw [coe_union, Set.sized_union]

Goal state after:
case inr.convert_5
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝³ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r ↑𝒜 ∧ Set.Sized r ↑(∂^[n - 2 * r] 𝒜ᶜˢ)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
⊢ x ∉ w.support

Tactic:
rintro hxw

Goal state after:
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber = 1 ↔ G = ⊥ ∧ Nonempty V

Tactic:
rw [eq_iff_le_not_lt, Order.lt_one_iff_nonpos, ← not_isEmpty_iff, ← Nat.cast_one, ← Nat.cast_zero,
    chromaticNumber_le_iff_colorable, chromaticNumber_le_iff_colorable, colorable_one_iff,
    colorable_zero_iff]

Goal state after:
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.neighborFinset w ⊆ s

Tactic:
by
  classical
  rw [isBipartiteWith_neighborFinset' h hw]
  exact filter_subset (G.Adj · w) s

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ completeBipartiteGraph α β ⊑ G →
    ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right

Tactic:
refine fun ⟨f⟩ ↦ ⟨univ.map ⟨f ∘ Sum.inl, f.injective.comp Sum.inl_injective⟩,
      univ.map ⟨f ∘ Sum.inr, f.injective.comp Sum.inr_injective⟩, by simp, by simp,
      fun _ hl _ hr ↦ ?_⟩
    rw [mem_coe, mem_map] at hl hr
    replace ⟨_, _, hl⟩ := hl
    replace ⟨_, _, hr⟩ := hr
    rw [← hl, ← hr]
    exact f.toHom.map_adj (by simp)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
by
  by_cases! h' : ¬G.Reachable u w
  · grind [dist_eq_zero_iff_eq_or_not_reachable]
  rw [← ENat.natCast_le_natCast, ENat.natCast_add]
  grind [SimpleGraph.edist_triangle, Reachable.trans, Reachable.symm]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
by
  by_cases! h' : ¬G.Reachable u w
  · grind [dist_eq_zero_iff_eq_or_not_reachable]
  rw [← ENat.natCast_le_natCast, ENat.natCast_add]
  grind [SimpleGraph.edist_triangle, Reachable.trans, Reachable.symm]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.IsPath

Tactic:
classical
  have : p.bypass = p := by
    apply bypass_eq_self_of_length_le_length_bypass
    calc p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass
  rw [← this]
  apply Walk.bypass_isPath

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
⊢ (∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) ↔
    v = p.snd ∨ v = p.penultimate

Tactic:
grind [getVert_endpoint_iff, add_tsub_cancel_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : Group M
x✝¹ x✝ : M
⊢ (mulCayley Set.univ).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
simp [mulCayley_adj]

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

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

Tactic:
exact ⟨hHs.some, hHs.some_mem, by simp⟩

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

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

Tactic:
← extremalNumber_le_iff

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ H.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)
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:
ext i j
  cases eq_or_ne i j <;> simp [‹_›]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
h : H ⊑ induce {v}ᶜ G
⊢ H ⊑ G

Tactic:
exact h.trans ⟨Copy.induce G {v}ᶜ⟩

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ ∀ (i j : V), adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1

Tactic:
grind [adjMatrix_apply]

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

Goal state before:
pp: case zero
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u v : V
⊢ (adjMatrix α G ^ 0) u v = ↑(#(G.finsetWalkLength 0 u v))

Tactic:
obtain rfl | h := eq_or_ne u v

Goal state after:
case zero.inl
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u : V
⊢ (adjMatrix α G ^ 0) u u = ↑(#(G.finsetWalkLength 0 u u))

case zero.inr
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u v : V
h : u ≠ v
⊢ (adjMatrix α G ^ 0) u v = ↑(#(G.finsetWalkLength 0 u v))
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ G.degree u = 1

Tactic:
rw [degree_eq_one_iff_existsUnique_adj]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃! w, G.Adj u w
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ G.degree v = 1

Tactic:
rw [degree_eq_one_iff_existsUnique_adj]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃! w, G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case map_rel'
α : 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
⊢ Odd ((Nonempty.some ⋯).length + 1 + (Nonempty.some ⋯).reverse.length)

Tactic:
length_reverse,

Goal state after:
case map_rel'
α : 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
⊢ Odd ((Nonempty.some ⋯).length + 1 + (Nonempty.some ⋯).length)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ (True ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (True ∧ c.supp ⊆ c'.supp) ∧ Odd {x | True ∧ G.connectedComponentMk x = c}.ncard

Tactic:
true_and,

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ Odd c.supp.ncard ∧ c.supp ⊆ c'.supp ↔ c.supp ⊆ c'.supp ∧ Odd {x | G.connectedComponentMk x = c}.ncard
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t

Tactic:
rw [← card_neighborFinset_eq_degree, neighborFinset_completeEquipartiteGraph v,
    card_product, card_compl, card_singleton, Fintype.card_fin, card_univ, Fintype.card_fin]

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

Goal state before:
pp: case pos
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : t = 0
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
rw [completeEquipartiteGraph_eq_bot_iff.mpr <| .inr ht]
    have : IsEmpty (Fin r × Fin t) := by simp [ht, Fin.isEmpty]
    exact Copy.bot .ofIsEmpty

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

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : n + w ≡ n + x [MOD r]
⊢ w = x

Tactic:
rw [Nat.ModEq.add_iff_left rfl] at this

Goal state after:
case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w ≡ x [MOD r]
⊢ w = x
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K, ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑∅

Tactic:
IsCompleteBetween,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K, ∀ p ∈ K.parts, ∀ ⦃v₁ : V⦄, v₁ ∈ ↑p → ∀ ⦃v₂ : V⦄, v₂ ∈ ↑∅ → G.Adj v₁ v₂
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
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}
h_le_sup :
  Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEmbedding) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}.sup fun x ↦ Fintype.card { x_1 // x_1 ∈ x.edgeSet }
⊢ Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEquiv) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦
      Fintype.card { x_1 // x_1 ∈ x.edgeSet }

Tactic:
exact h_le_sup

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
hv : v ∈ K.vertsᶜ \ filter K t
ht'_pos : 0 < t'
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).degree v < #K.verts - t' + t

Tactic:
simp_rw [Finset.mem_sdiff, ErdosStone.filter, mem_filter, not_and_or, and_or_left,
    and_not_self_iff, false_or, not_forall, not_exists, not_and_or, not_forall, exists_prop] at hv
  obtain ⟨hv, p, hp, hs⟩ := hv
  rw [← card_neighborFinset_eq_degree,
    isBipartiteWith_neighborFinset' (between_verts_isBipartiteWith K) hv]
  conv =>
    enter [1, 1, 2]
    unfold CompleteEquipartiteSubgraph.verts
  rw [filter_disjiUnion, card_disjiUnion, sum_eq_sum_sdiff_singleton_add hp]
  apply add_lt_add_of_le_of_lt
  · conv_rhs =>
      rw [K.card_verts, ← Nat.sub_one_mul, ← K.card_parts.resolve_right ht'_pos.ne',
        ← card_singleton p, ← Finset.card_sdiff_of_subset (singleton_subset_iff.mpr hp),
        ← smul_eq_mul, ← sum_const,
        ← Finset.sum_congr rfl fun _ h ↦ K.card_mem_parts (mem_sdiff.mp h).1]
    exact sum_le_sum (fun _ _ ↦ card_filter_le _ _)
  · contrapose! hs
    obtain ⟨s, hs⟩ := powersetCard_nonempty.mpr hs
    have hs' : s ∈ p.powersetCard t := powersetCard_mono (filter_subset _ _) hs
    refine ⟨s, hs', fun w hw ↦ ?_⟩
    obtain ⟨_, hadj, _⟩ := by
      rw [mem_powersetCard] at hs
      apply hs.1 at hw
      rwa [mem_filter, between_adj] at hw
    exact hadj.symm

Goal state after:
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)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}
h_le_sup :
  Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEmbedding) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}.sup fun x ↦ Fintype.card { x_1 // x_1 ∈ x.edgeSet }
⊢ Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEquiv) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      Fintype.card { x_1 // x_1 ∈ x.edgeSet }

Tactic:
exact h_le_sup

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ Surjective h.toEdge

Tactic:
rintro ⟨⟨x, y⟩, he⟩

Goal state after:
case mk
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
val✝ : Sym2 V
x y : V
he : Quot.mk (Sym2.Rel V) (x, y) ∈ M.edgeSet
⊢ ∃ a, h.toEdge a = ⟨Quot.mk (Sym2.Rel V) (x, y), he⟩
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
⊢ p₁ ∪ p₂ = Set.univ

Tactic:
classical
  obtain ⟨f, _, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_
  have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)
  grind

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w

Tactic:
exact (hadj ⟨w, _⟩).symm

Goal state after:
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:
by
  convert! one_ne_zero.ite_eq_left_iff
  infer_instance

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ↑(#{x | True ∧ (x = a ∨ x = b)}) = ↑(#{a, b})

Tactic:
congr 2

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ {x | True ∧ (x = a ∨ x = b)} = {a, b}
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ((incMatrix R G)ᵀ * incMatrix R G) e e = if e ∈ G.edgeSet then 2 else 0

Tactic:
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ite_zero_mul_ite_zero, one_mul,
    sum_boole, and_self_iff]

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = if e ∈ G.edgeSet then 2 else 0
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#{x | x = v ∨ x = w}) = ↑(#{v, w})

Tactic:
congr 2

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ {x | x = v ∨ x = w} = {v, w}
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✝ : CommSemiring R
x : V → R
⊢ x ⬝ᵥ degMatrix R G *ᵥ x = ∑ i, ↑(G.degree i) * x i * x i

Tactic:
by
  simp only [dotProduct, degMatrix, mulVec_diagonal, ← mul_assoc, mul_comm]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this : (G \ p.toSubgraph.spanningCoe).Adj w' v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
use (((hcyc.reachable_sdiff_toSubgraph_spanningCoe_aux
    (p.cons hw'2.symm) hp'p).some).mapLe hle).append this.toWalk

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
⊢ SimpleGraph.map (⇑(subtype fun x ↦ x ∈ G.edgeSet)) G.lineGraph ≤
    SimpleGraph.map (⇑(subtype fun x ↦ x ∈ G'.edgeSet)) G'.lineGraph

Tactic:
rintro _ _ ⟨hne', ⟨⟨⟩, h₁⟩, ⟨⟨⟩, h₂⟩, ⟨hne, hinter⟩, rfl, rfl⟩

Goal state after:
case mk.mk
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
val✝¹ : Sym2 V
a✝¹ : V × V
h₁ : Quot.mk (Sym2.Rel V) a✝¹ ∈ G.edgeSet
val✝ : Sym2 V
a✝ : V × V
h₂ : Quot.mk (Sym2.Rel V) a✝ ∈ G.edgeSet
hne : ⟨Quot.mk (Sym2.Rel V) a✝¹, h₁⟩ ≠ ⟨Quot.mk (Sym2.Rel V) a✝, h₂⟩
hinter : (↑↑⟨Quot.mk (Sym2.Rel V) a✝¹, h₁⟩ ∩ ↑↑⟨Quot.mk (Sym2.Rel V) a✝, h₂⟩).Nonempty
hne' :
  (subtype fun x ↦ x ∈ G.edgeSet) ⟨Quot.mk (Sym2.Rel V) a✝¹, h₁⟩ ≠
    (subtype fun x ↦ x ∈ G.edgeSet) ⟨Quot.mk (Sym2.Rel V) a✝, h₂⟩
⊢ (SimpleGraph.map (⇑(subtype fun x ↦ x ∈ G'.edgeSet)) G'.lineGraph).Adj
    ((subtype fun x ↦ x ∈ G.edgeSet) ⟨Quot.mk (Sym2.Rel V) a✝¹, h₁⟩)
    ((subtype fun x ↦ x ∈ G.edgeSet) ⟨Quot.mk (Sym2.Rel V) a✝, h₂⟩)