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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (#s + 1) * #(𝒜 ∩ ℬ)

Tactic:
pow_succ',

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * 2 ^ #s * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

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

Tactic:
exact fun h ↦ h𝒜₂ (mem_insert_of_mem h)

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

Goal state before:
pp: case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(#𝒜) / ↑((Fintype.card α).choose r) ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))

Tactic:
div_le_div_iff₀

Goal state after:
case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(#𝒜) * ↑((Fintype.card α).choose (r - 1)) ≤ ↑(#(∂ 𝒜)) * ↑((Fintype.card α).choose r)

case inr.hb
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose r)

case inr.hd
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose (r - 1))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr.inr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this✝ : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
this : a ∉ t
⊢ False

Tactic:
apply (min'_le tᶜ _ _).not_gt gt

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := ⋯
hjk : j ≤ k
this✝ : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
this : a ∉ t
⊢ a ∈ tᶜ
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := ⋯
hjk : j ≤ k
this✝ : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
this : a ∉ t
⊢ a ∈ tᶜ

Tactic:
rwa [mem_compl]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s = ∅

Tactic:
← Finset.card_eq_zero

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ #s = 0
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ⊆ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

Tactic:
simp only [subset_empty, shadow_singleton_empty] at this

Goal state after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 = ∅
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}

Tactic:
simp_rw [mem_sdiff (s := s), filter_inj, and_assoc]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ (memberSubfamily a 𝒜).shatterer ⊆ 𝒜.shatterer

Tactic:
simp only [subset_iff, mem_shatterer]

Goal state after:
case refine_3.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ ∀ ⦃x : Finset α⦄, (memberSubfamily a 𝒜).Shatters x → 𝒜.Shatters x
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ (𝓓 a 𝒜).shatterer ⊆ 𝒜.shatterer

Tactic:
simp only [subset_iff, mem_shatterer]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
⊢ ∀ (y₁ y₂ : Set α), y₁ ∈ s ∧ a ∈ y₁ → y₂ ∈ s ∧ a ∈ y₂ → y₁ = y₂

Tactic:
intro b₁

Goal state after:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ : Set α
⊢ ∀ (y₂ : Set α), b₁ ∈ s ∧ a ∈ b₁ → y₂ ∈ s ∧ a ∈ y₂ → b₁ = y₂
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
huv' : Gᶜ.Adj u v
hvw' : Gᶜ.Adj v w
⊢ Gᶜ.Reachable u w

Tactic:
exact huv'.reachable.trans hvw'.reachable

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

Goal state before:
pp: 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
⊢ #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) = #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
card_union_of_disjoint ‹_›

Goal state after:
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
⊢ #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) = #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ)
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
⊢ Disjoint (G.neighborFinset w) t

Tactic:
rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]
  exact isBipartiteWith_neighborSet_disjoint' h hw

Goal state after:
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
w : ↥t
| #(G.neighborFinset ↑w)

Tactic:
isBipartiteWith_bipartiteBelow h w.prop

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
w : ↥t
| #(bipartiteBelow G.Adj s ↑w)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < ↑2
h' : s ≠ {s(u, w.snd)}
⊢ (G.deleteEdges s).Reachable u w.snd

Tactic:
· refine Walk.reachable <| Walk.cons (deleteEdges_adj.mpr ⟨this, ?_⟩) Walk.nil
    contrapose h'
    refine (Set.subsingleton_iff_singleton h').mp ?_
    exact Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs)

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

Goal state before:
pp: case inl.inr
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
apply Adj.reachable; simp

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

Goal state before:
pp: case inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
apply Adj.reachable; simp

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
⊢ G.neighborSet v ⊆ (between s sᶜ G).neighborSet v ∪ s

Tactic:
intro w hadj
  rw [neighborSet, Set.mem_union, Set.mem_ofPred, between_adj]
  by_cases hw : w ∈ s
  · exact Or.inr hw
  · exact Or.inl ⟨hadj, Or.inl ⟨hv, hw⟩⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless

Tactic:
by
  simp_rw [Subgraph.IsInduced, IsChordless, IsChord, Sym2.forall, Sym2.lift_mk, G.mem_edgeSet,
    mem_verts_toSubgraph, adj_toSubgraph_iff_mem_edges]
  grind only

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 (V ⊕ V)
he : e ∈ G.bipartiteDoubleCover.edgeFinset
⊢ ∃ a,
    ∃ (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
      (match a, ha with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        e

Tactic:
induction e with | _ v w

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V ⊕ V
he : s(v, w) ∈ G.bipartiteDoubleCover.edgeFinset
⊢ ∃ a,
    ∃ (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
      (match a, ha with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
      obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
      rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
      exact edist_le _

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

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

Tactic:
obtain ⟨p, hp⟩ := hconn.exists_walk_length_eq_dist u v
  obtain ⟨q, hq⟩ := hconn.exists_walk_length_eq_dist v w
  rw [← hp, ← hq, ← Walk.length_append]
  apply dist_le

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : Group M
⊢ mulCayley s⁻¹ = mulCayley s

Tactic:
by
  ext u v
  simp [mulCayley_adj, or_comm]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A.compl.compl = A

Tactic:
by
  ext
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `simp`. This is probably a problem at Mathlib's end rather than `grind`'s,
  as we are relying on seeing through the definition of `Matrix`, and `of`. The original proof was:
  `grind [of, compl, IsAdjMatrix]` -/
  simp [compl]; grind [compl, IsAdjMatrix]

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✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
rw [mulVec, adjMatrix_dotProduct]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t

Tactic:
by
  rw [IsTuranMaximal, IsExtremal] at h; contrapose! h; intro cf
  wlog hd : G.degree t < G.degree s generalizing G t s
  · replace hd : G.degree s < G.degree t := lt_of_le_of_ne (le_of_not_gt hd) h
    exact this (by rwa [adj_comm] at hn) hd.ne' cf hd
  classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  lia

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

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
F : SimpleGraph V
hF : H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
⊢ ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsTree

Tactic:
grind [IsTree, Connected, preconnected_iff_reachable_eq_top]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.Connected
F : SimpleGraph V
hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
⊢ ∃ T ≤ G, T.IsTree

Tactic:
grind [IsTree, Connected, preconnected_iff_reachable_eq_top]

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

Goal state before:
pp: case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).2 ≤ ↑v.2

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred v.1.pos, mul_comm r ↑v.2]
        exact Nat.add_le_add_left (Nat.le_pred_of_lt v.1.prop) (↑v.2 * r)

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

Goal state before:
pp: r t : ℕ
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
rcases t.eq_zero_or_pos with ht_eq0 | ht_pos

Goal state after:
case inl
r t : ℕ
ht_eq0 : t = 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

case inr
r t : ℕ
ht_pos : t > 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
| (completeEquipartiteGraph r t).degree v

Tactic:
rw [degree_completeEquipartiteGraph v]

Goal state after:
r t : ℕ
v : Fin r × Fin t
| (r - 1) * t
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
| 2 * (r.choose 2 * t ^ 2)

Tactic:
rw [← Nat.mul_assoc, Nat.choose_two_right, Nat.mul_div_cancel' r.even_mul_pred_self.two_dvd]

Goal state after:
r t : ℕ
| r * (r - 1) * t ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
⊢ G'.oddComponents.ncard ≤ G.oddComponents.ncard

Tactic:
have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
      {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty := by
    refine Set.nonempty_of_ncard_ne_zero fun h' ↦ Nat.not_odd_zero ?_
    rw [← h']
    exact (c.odd_oddComponents_ncard_subset_supp _ h).2 hc

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty
⊢ G'.oddComponents.ncard ≤ G.oddComponents.ncard
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∃! x_1, x_1 ∈ s ∩ (G.connectedComponentMk x).supp

Tactic:
use x

Goal state after:
case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ (fun x_1 ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) x ∧
    ∀ (y : V), (fun x_1 ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) y → y = x
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
⊢ Fin r × Fin t ↪ V

Tactic:
by
      use fun (i, j) ↦ fₜ (fᵣ i) j
      intro (i₁, j₁) (i₂, j₂) heq
      rw [Prod.mk.injEq]
      contrapose! heq with hne
      rcases eq_or_ne i₁ i₂ with heq | hne
      · rw [heq, ← Subtype.ext_iff.ne]
        exact (fₜ _).injective.ne (hne heq)
      · refine (K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne
        exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

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

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≤ 1 → ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
intro h v huv
    have hd : G.edist u v ≤ 1 := edist_le_eccent.trans h
    have hd' : 1 ≤ G.edist u v := Order.one_le_iff_pos.mpr (G.edist_pos_of_ne huv)
    exact edist_eq_one_iff_adj.mp (le_antisymm (hd') hd).symm

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
h : 1 ≤ G.eccent u
⊢ G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
← h.ge_iff_eq'

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
h : 1 ≤ G.eccent u
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ G.Adj v w

Tactic:
· exact h ▸ h₂ ⟨w, by assumption⟩ |>.symm

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
⊢ (Subgraph.map (Hom.ofLE hGG') M).IsMatching

Tactic:
by
  intro _ hv
  obtain ⟨_, hv, hv'⟩ := Set.mem_image _ _ _ |>.mp hv
  obtain ⟨w, hw⟩ := h hv
  use w
  simpa using hv' ▸ hw

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

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f ⟨x, hx₁⟩ = v
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False

Tactic:
use x

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f ⟨x, hx₁⟩ = v
⊢ (fun w ↦ if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False) x ∧
    ∀ (y : V), (fun w ↦ if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False) y → y = x
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
⊢ (M ⊔ M').IsMatching

Tactic:
intro v hv
  have aux {N N' : Subgraph G} (hN : N.IsMatching) (hd : Disjoint N.support N'.support)
    (hmN : v ∈ N.verts) : ∃! w, (N ⊔ N').Adj v w := by
    obtain ⟨w, hw⟩ := hN hmN
    use w
    refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩
    intro y hy
    cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v
  cases Set.mem_or_mem_of_mem_union hv with
  | inl hmM => exact aux hM hd hmM
  | inr hmM' =>
    rw [sup_comm]
    exact aux hM' (Disjoint.symm hd) hmM'

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
by
  have : Fintype V := Fintype.ofFinite V
  exact reachable_sdiff_toSubgraph_spanningCoe_aux hcyc p hp

Goal state after: