mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
⊢ ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
i

Goal state after:
case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
⊢ ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝ c✝ : V
p : Path r b✝
e : b✝ ⟶ c✝
ih : ∀ (q : Path r b✝), p = q
q : Path r c✝
⊢ p.cons e = q

Tactic:
| cons p e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Weight

Goal state before:
pp: case cons
V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e
i j b✝ c✝ : V
p : Path i b✝
e : b✝ ⟶ c✝
ih : 0 < weight (fun {i j} ↦ w) p
⊢ 0 < weight (fun {i j} ↦ w) (p.cons e)

Tactic:
| cons p e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Weight

Goal state before:
pp: case cons
V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : {i j : V} → (i ⟶ j) → R
hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e
i j b✝ c✝ : V
p : Path i b✝
e : b✝ ⟶ c✝
ih : 0 ≤ weight (fun {i j} ↦ w) p
⊢ 0 ≤ weight (fun {i j} ↦ w) (p.cons e)

Tactic:
| cons p e ih =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
have : ∀ {x : ℕ}, ∀ s ∈ powersetCard x (univ : Finset α),
    (card α / ((card α - #s) * (card α).choose #s) : ℚ) =
      card α / ((card α - x) * (card α).choose x) := by
    intro n s hs
    rw [mem_powersetCard_univ.1 hs]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ ∀ (x : ℕ), x ∈ A + B

Tactic:
rintro (_ | m)

Goal state after:
case zero
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ∈ A + B

case succ
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
⊢ m + 1 ∈ A + B
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
h : ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
b c : α
ha : b ⊔ c = a
⊢ b = a ∨ c = a

Tactic:
simpa [← ha] using h ha.ge

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
card_truncatedInf_union_add_card_truncatedInf_sups

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∈ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
obtain ⟨b, hbv, Hcomp⟩ := huv a hau
      refine mem_shadow_iff_insert_mem.2 ⟨b, notMem_sdiff_of_mem_right hbv, ?_⟩
      rw [← Hcomp.eq] at ht
      have hsb :=
        sup_sdiff_mem_of_mem_compression ht ((erase_subset _ _).trans hvt)
          (disjoint_erase_comm.2 huvs.1)
      rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
        erase_union_of_mem hau] at hsb

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

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∪ compl ⁻¹' ↑s

Tactic:
simp_rw [mem_union, mem_preimage]

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∨ aᶜ ∈ ↑s
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
a : α
ha : V.max' hV < a
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s

Tactic:
have : a ∉ V := fun H ↦ ha.not_ge (le_max' _ _ H)

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
a : α
ha : V.max' hV < a
this : a ∉ V
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x _y : α
h : ∀ s ∈ c, x ∈ s → _y ∈ s
s : Set α
hs : s ∈ c
hy : _y ∈ s
t : Set α
right✝ : ∀ (y : Set α), (fun b ↦ b ∈ c ∧ x ∈ b) y → y = t
ht : t ∈ c
hx : x ∈ t
⊢ x ∈ s

Tactic:
rwa [eq_of_mem_eqv_class H hs hy ht (h t ht hx)]

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

Goal state before:
pp: V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
⊢ G.support = Set.univ

Tactic:
simp only [Set.eq_univ_iff_forall]
  intro v
  obtain ⟨w, hw⟩ := exists_ne v
  obtain ⟨p⟩ := h v w
  cases p with
  | nil => contradiction
  | @cons _ w => exact ⟨w, ‹_›⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Injective supp

Tactic:
refine ConnectedComponent.ind₂ ?_

Goal state after:
V : Type u
G : SimpleGraph V
⊢ ∀ (v w : V),
    (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
      G.connectedComponentMk v = G.connectedComponentMk w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ Maximal (fun x ↦ (induce x G).Connected) s ↔ ∃ C, C.supp = s

Tactic:
refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
s : Set V
x✝ : Maximal (fun x ↦ (induce x G).Connected) s
hconn : (fun x ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun x ↦ (induce x G).Connected) y → s ⊆ y → y ⊆ s
⊢ ∃ C, C.supp = s

case refine_2
V : Type u
G : SimpleGraph V
s : Set V
x✝ : ∃ C, C.supp = s
C : G.ConnectedComponent
h : C.supp = s
⊢ Maximal (fun x ↦ (induce x G).Connected) s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Set.univ.Nonempty

Tactic:
rw [← Set.nonempty_iff_univ_nonempty]
  exact hconn u v

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

Goal state before:
pp: case mk
V : Type u
G G' : SimpleGraph V
e : Sym2 V
hG : G ≤ G'
a b : V
h : ¬(G'.deleteEdges {s(a, b)}).Reachable a b
⊢ ¬(G.deleteEdges {s(a, b)}).Reachable a b

Tactic:
grw [hG]

Goal state after:
case mk
V : Type u
G G' : SimpleGraph V
e : Sym2 V
hG : G ≤ G'
a b : V
h : ¬(G'.deleteEdges {s(a, b)}).Reachable a b
⊢ ¬(G'.deleteEdges {s(a, b)}).Reachable a b
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
⊢ G.CliqueFree n

Tactic:
by
  have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top
  obtain ⟨m, hc'⟩ := chromaticNumber_ne_top_iff_exists.mp hne
  have := colorable_chromaticNumber hc'
  refine this.cliqueFree ?_
  rw [← ENat.natCast_toNat_eq_self] at hne
  rw [← hne] at hc
  simpa using hc

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
⊢ Nonempty (β ↪ ↥right)

Tactic:
rw [← card_coe] at card_right

Goal state after:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : Fintype.card ↥right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
⊢ Nonempty (β ↪ ↥right)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ c, H.verts = c.supp

Tactic:
rw [SimpleGraph.ConnectedComponent.exists]

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Maximal Subgraph.Connected G' ↔ ∃ C, C.toSubgraph = G'

Tactic:
refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
⊢ ∃ C, C.toSubgraph = G'

case refine_2
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : ∃ C, C.toSubgraph = G'
C : G.ConnectedComponent
h : C.toSubgraph = G'
⊢ Maximal Subgraph.Connected G'
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ⊓ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ⊔ g b)

Tactic:
← map_sup,

Goal state after:
case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ⊓ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g (a ⊔ b))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
⊢ ∃ p, p.toSubgraph ≤ H

Tactic:
refine (hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_

Goal state after:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk ⟨u, hu⟩ ⟨v, hv⟩
⊢ ∃ p, p.toSubgraph ≤ H
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case succ
n n✝ : ℕ
hm : n✝ + 1 ≤ n + 3
⊢ (cycle n).getVert (n✝ + 1) = ⟨(n + 3 - (n✝ + 1)) % (n + 3), ⋯⟩

Tactic:
· grind +locals [getVert_cons_succ, cycleGraph.getVert_cycleCons]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
⊢ mulCayley {1} = ⊥

Tactic:
← mulCayley_erase_one,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
⊢ mulCayley ({1} \ {1}) = ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: n : ℕ
⊢ cycleGraph (n + 1) = circulantGraph {1}

Tactic:
by
  cases n
  · exact edgeFinset_inj.mp rfl
  · aesop

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
h : ∀ (u v : V), Subsingleton (G.Path u v)
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ False

Tactic:
have := h _ v |>.elim ⟨_, hc.isPath_tail⟩ ⟨_, .of_adj <| c.adj_snd hc.not_nil |>.symm⟩

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
h : ∀ (u v : V), Subsingleton (G.Path u v)
v : V
c : G.Walk v v
hc : c.IsCycle
this : ⟨c.tail, ⋯⟩ = ⟨⋯.toWalk, ⋯⟩
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
hij : A i j = 1
⊢ A j i = 1

Tactic:
rwa [h.symm.apply i j]

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
h : H.Free G
v : V
⊢ #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (Fintype.card V - 1) H

Tactic:
rw [← card_edgeFinset_induce_compl_singleton, ← @card_unique ({v} : Set V), ← card_compl_set]
  apply card_edgeFinset_le_extremalNumber
  contrapose h
  exact h.trans ⟨Copy.induce G {v}ᶜ⟩

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

Goal state before:
pp: n r : ℕ
hr : 0 < r
f : (completeGraph (Fin (r + 1))).Copy (turanGraph n r)
x y : Fin (r + 1)
d : x ≠ y
c : ⟨↑(f x) % r, ⋯⟩ = ⟨↑(f y) % r, ⋯⟩
⊢ False

Tactic:
Fin.mk.injEq

Goal state after:
n r : ℕ
hr : 0 < r
f : (completeGraph (Fin (r + 1))).Copy (turanGraph n r)
x y : Fin (r + 1)
d : x ≠ y
c : ↑(f x) % r = ↑(f y) % r
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
v w : Fin 2
⊢ (fun v ↦ ⟨↑v, ⋯⟩) v = (fun v ↦ ⟨↑v, ⋯⟩) w → v = w

Tactic:
Fin.mk.injEq

Goal state after:
n : ℕ
h : 2 ≤ n
v w : Fin 2
⊢ ↑v = ↑w → v = w
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:
← cliqueFinset_eq_empty_iff,

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.cliqueFinset r = ∅
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
⊢ Odd #({a ∈ G.oddComponents.toFinset | (fun c ↦ c.supp ⊆ c'.supp) a}) ↔
    Odd #({x ∈ {c | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)})

Tactic:
congr! 2

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
⊢ {a ∈ G.oddComponents.toFinset | (fun c ↦ c.supp ⊆ c'.supp) a} =
    {x ∈ {c | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts

Tactic:
card_parts

Goal state after:
case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a
n r : ℕ
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) = ∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0

Tactic:
simp [← Fin.sum_univ_eq_sum_range]

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

Goal state before:
pp: case neg
α : 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:
have : Nonempty (Fin r ↪ K.parts) := by
      rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]
    let fᵣ : Fin r ↪ K.parts := Classical.arbitrary (Fin r ↪ K.parts)
    have (p : K.parts) : Nonempty (Fin t ↪ p) := by
      rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
    let fₜ (p : K.parts) : Fin t ↪ p :=
      Classical.arbitrary (Fin t ↪ p)
    let f : (Fin r) × (Fin t) ↪ V := 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
    refine ⟨⟨f, fun hne ↦ ?_⟩, f.injective⟩
    refine K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop
    exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ G.ediam ≤ 2 * G.eccent u

Tactic:
by
  refine ediam_le_of_edist_le fun v w ↦ ?_
  calc
    G.edist v w
      ≤ G.edist v u + G.edist u w := G.edist_triangle
    _ = G.edist u v + G.edist u w := by rw [edist_comm]
    _ ≤ G.eccent u + G.eccent u := add_le_add edist_le_eccent edist_le_eccent
    _ = 2 * G.eccent u := (two_mul _).symm

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⊤ ∨ G.ediam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

Tactic:
ediam_eq_zero_iff_subsingleton

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⊤ ∨ Subsingleton α ↔ G.ediam = ⊤ ∨ Subsingleton α
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_4
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
p✝ : Finset V
h : ∃ a, True ∧ map { toFun := fun j ↦ f (a, j), inj' := ⋯ } univ = p✝
⊢ #p✝ = t

Tactic:
true_and

Goal state after:
case neg.refine_4
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
p✝ : Finset V
h : ∃ a, map { toFun := fun j ↦ f (a, j), inj' := ⋯ } univ = p✝
⊢ #p✝ = t
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, ∀ ⦃v₁ : V⦄, v₁ ∈ p → ∀ ⦃v₂ : V⦄, False → G.Adj v₁ v₂

Tactic:
IsEmpty.forall_iff,

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⦄, True
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
⊢ Function.Injective supp

Tactic:
refine ConnectedComponent.ind₂ ?_

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
⊢ ∀ (v w : ↑Kᶜ),
    supp ((induce Kᶜ G).connectedComponentMk v) = supp ((induce Kᶜ G).connectedComponentMk w) →
      (induce Kᶜ G).connectedComponentMk v = (induce Kᶜ G).connectedComponentMk w