mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
i : ℕ
⊢ 1 - (X ^ (i + 1)) ^ m = (∑ x ∈ range m, (X ^ (i + 1)) ^ x) * (1 - X ^ (i + 1))

Tactic:
geom_sum_mul_neg

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < (X ^ ((k + 1) * m) * ∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order

Tactic:
← le_order_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < (X ^ ((k + 1) * m)).order + (∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Multipliable fun n ↦ 1 - X ^ (n + k + 1)

Tactic:
exact Pentagonal.multipliable_one_sub_X_pow R

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n <
    ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order

Tactic:
← le_order_mul,

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n <
    ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2)).order +
      (∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
⊢ G.IsLink e x y ↔ ⊥.IsLink e x y

Tactic:
simp only [edgeSet_bot, mem_empty_iff_false, not_false_eq_true, not_isLink_of_notMem_edgeSet,
    iff_false]

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
⊢ ¬G.IsLink e x y
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.restrict F ≤ G.restrict F

Tactic:
refine (Compatible.of_le_le (G := G) (restrict_le.trans h) (by simp)).le_iff.mpr ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ V(H.restrict F) ⊆ V(G.restrict F)

case refine_2
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H.restrict F) ⊆ E(G.restrict F)
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
h : G = noEdge V(G) β
⊢ E(G) = ∅

Tactic:
rw [h, edgeSet_noEdge]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
⊢ (∃ D ⊆ M.E, N = M ＼ D) → N ≤r M

Tactic:
rintro ⟨D, -, rfl⟩; apply delete_isRestriction

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J

Tactic:
((coloops_indep _).subset hss).contract_indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.left
σ : 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
⊢ m.toSyn
      (m.degree
        (b j *
          (g' j + (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) j))) ≤
    m.toSyn (m.degree f)

Tactic:
rw [mul_add]

Goal state after:
case h.right.left
σ : 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
⊢ m.toSyn
      (m.degree
        (b j * g' j +
          b j * (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) j)) ≤
    m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
⊢ Disjoint X (C \ M.E ∪ C ∩ M.E)

Tactic:
disjoint_union_right,

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
⊢ Disjoint X (C \ M.E) ∧ Disjoint X (C ∩ M.E)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case neg
σ : 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
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
hc : ¬i = j
⊢ m.toSyn (m.degree (b j * 0)) ≤ m.toSyn (m.degree f)

Tactic:
· simp only [mul_zero, degree_zero, map_zero]
          exact bot_le

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
⊢ J.Finite → (M i).Indep J

Tactic:
hJ

Goal state after:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ (M i).Indep J
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
⊢ (∀ (i : ι), (M i).IsBasis (Sigma.mk i ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' I) (Sigma.mk i ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' X)) ↔
    ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)

Tactic:
convert! Iff.rfl <;>
  exact ext <| by simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')

Tactic:
contract_delete_contract_delete',

Goal state after:
α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ (C ∪ C' \ D) ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
this : p.length + q.length = 0
⊢ p.length = 0

Tactic:
exact Nat.eq_zero_of_add_eq_zero_right this

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) / ↑k ≤ 1 - (↑k)⁻¹

Tactic:
rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne']

Goal state after:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) / ↑k ≤ (↑k - 1) / ↑k
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v

Tactic:
rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ #({a ∈ s | compress u v a ∈ s} ∪ {a ∈ image (compress u v) s | a ∉ s}) = #s

Tactic:
card_union_of_disjoint compress_disjoint,

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ #({a ∈ s | compress u v a ∈ s}) + #({a ∈ image (compress u v) s | a ∉ s}) = #s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ #s = r + 1

Tactic:
← h𝒜 (erase_mem_shadow hs ha),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ #s = #(s.erase a) + 1
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
hs : InfIrred s
⊢ ∃ a, Ici a = s

Tactic:
obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_minimal (coe_nonempty.2 hs.ne_top)
    exact ⟨a, (hs.2 <| erase_inf_Ici ha fun b hb ↦ le_imp_eq_iff_le_imp_ge.2 <| has hb).resolve_left
      (lt_erase.2 ha).ne'⟩

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ s.sup id ≤ (fun s ↦ (↑s).toFinset.sup Subtype.val) ((fun a ↦ { carrier := {b | ↑b ≤ a}, lower' := ⋯ }) (s.sup id))

Tactic:
exact Finset.sup_le fun i hi ↦
          le_sup_of_le (b := ⟨i, hs hi⟩) (Set.mem_toFinset.2 <| le_sup (f := id) hi) le_rfl

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

Goal state before:
pp: case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ #u + (k + 1) = #s

Tactic:
rw [← hcardst, hcardtu, add_right_comm]

Goal state after:
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ #u + (k + 1) = #u + k + 1
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
⊢ s.Intersecting ↔ (s.Pairwise fun a b ↦ ¬Disjoint a b) ∧ s ≠ {⊥}

Tactic:
refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : s.Intersecting
⊢ s ≠ {⊥}

case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h : 𝒜 ⊆ ℬ
x✝ : Finset α
⊢ x✝ ∈ 𝒜.shatterer → x✝ ∈ ℬ.shatterer

Tactic:
by simpa using Shatters.mono_left h

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

Goal state before:
pp: V : Type u
inst✝² : Nontrivial V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
⊢ 0 < G.minDegree

Tactic:
rw [hv]

Goal state after:
V : Type u
inst✝² : Nontrivial V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
⊢ 0 < G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.Adj w v

pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.Adj v w

Tactic:
· exact hadj.symm

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∉ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ 0 ≤ f₃ (s ∩ t) + f₃ (insert a (s ∩ t))

Tactic:
exact add_nonneg (h₃ _) (h₃ _)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hG : G.Colorable n
⊢ ↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C

Tactic:
le_chromaticNumber_iff_forall_surjective

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hG : G.Colorable n
⊢ (∀ (C : G.Coloring (Fin n)), Surjective ⇑C) ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
simpa [show w.length - 1 + 1 = w.length by lia]
    using w.toSubgraph_adj_getVert (by lia : w.length - 1 < w.length)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝¹ v v✝ : V
hadj : G.Adj u v✝
w : G.Walk v✝ v
hs : ∀ x ∈ (cons hadj w).support, x ∈ s
⊢ Walk.map { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (cons hadj w).mapToSubgraph = Walk.induce s (cons hadj w) hs

Tactic:
by
    rw [mapToSubgraph, map_cons, map_map]
    exact congrArg _ <| w.map_mapToSubgraph_eq_induce s (hs · <| List.mem_of_mem_tail ·)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < G.dist u v
⊢ Set.univ.Nonempty

Tactic:
by
  rw [dist_eq_sInf] at h
  simpa [Set.range_nonempty_iff_nonempty, Set.nonempty_iff_univ_nonempty] using
    Nat.nonempty_of_pos_sInf h

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

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
hs : ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr
d : (V ⊕ W) × (V ⊕ W)
hadj : (G ⊕g H).Adj d.1 d.2
left✝ : { toProd := d, adj := hadj } ∈ p.darts
hd1 : d.1 ∈ Set.range Sum.inl
hd2 : d.2 ∈ Set.range Sum.inr
⊢ False

Tactic:
obtain ⟨v', hv'⟩ := hd1

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
hs : ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr
d : (V ⊕ W) × (V ⊕ W)
hadj : (G ⊕g H).Adj d.1 d.2
left✝ : { toProd := d, adj := hadj } ∈ p.darts
hd2 : d.2 ∈ Set.range Sum.inr
v' : V
hv' : Sum.inl v' = d.1
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n m : ℕ
h : m + 1 < n + 3
⊢ (cycleCons n ⟨m, ⋯⟩).length + 1 = m + 1

Tactic:
rw [cycleGraph.length_cycle_cons n]

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

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber ≤ 2

Tactic:
exact hc.chromaticNumber_le

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

Goal state before:
pp: V : Type u_1
K : Type u_3
C : TopEdgeLabeling V K
k : K
x y : V
⊢ (EdgeLabeling.labelGraph C k).Adj x y ↔ ∃ (H : x ≠ y), EdgeLabeling.get C x y H = k

Tactic:
simp [EdgeLabeling.labelGraph_adj, EdgeLabeling.get_eq]

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

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

Tactic:
mul_comm r (t - 1)

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (t - 1) * r + r
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
h✝ : ∀ (v : α), ∃ w, ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ G.eccent u = ⊤

Tactic:
rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
h✝ : ∀ (v : α), ∃ w, ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ G.edist u v ≤ G.eccent u
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
u : α
⊢ ⊤.eccent u ≤ 1

Tactic:
rw [eccent, iSup_le_iff]

Goal state after:
α : Type u_1
inst✝ : Nontrivial α
u : α
⊢ ∀ (i : α), ⊤.edist u i ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ C.supp.Infinite → ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

Tactic:
rintro Cinf L h
      obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.sdiff Cinf L.finite_toSet)
      exact ⟨componentComplMk _ vL, rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
⊢ Finite (G.ComponentCompl ↑K)

Tactic:
classical
  rcases K.eq_empty_or_nonempty with rfl | h
  -- If K is empty, then removing K doesn't change the graph, which is connected, hence has a
  -- single connected component
  · dsimp [ComponentCompl]
    rw [Finset.coe_empty, Set.compl_empty]
    have := Gpc.out.subsingleton_connectedComponent
    exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
  -- Otherwise, we consider the function `touch` mapping a connected component to one of its
  -- vertices adjacent to `K`.
  · let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
      let p := C.exists_adj_boundary_pair Gpc.out h
      ⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩
    -- `touch` is injective
    have touch_inj : touch.Injective := fun C D h' => ComponentCompl.pairwise_disjoint.eq
      (Set.not_disjoint_iff.mpr ⟨touch C, (C.exists_adj_boundary_pair Gpc.out h).choose_spec.1,
                                 h'.symm ▸ (D.exists_adj_boundary_pair Gpc.out h).choose_spec.1⟩)
    -- `touch` has finite range
    have : Finite (Set.range touch) := by
      refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
      apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
      simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_ofPred_eq, implies_true]
    -- hence `touch` has a finite domain
    apply Finite.of_injective_finite_range touch_inj

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

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : IsEmpty V
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

Tactic:
← Fintype.card_eq_zero_iff

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (fun x ↦ ↑(extremalNumber x H) / (H.turanDensity * ↑(x.choose 2))) atTop (𝓝 1)
n : ℕ
hn : 2 ≤ n
⊢ H.turanDensity * ↑(n.choose 2) ≠ 0

Tactic:
simpa [h, Nat.choose_eq_zero_iff]

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'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) - (↑(#(filter K t)) * ↑(#K.verts) - ↑(#(filter K t)) * (↑t' - ↑t)) +
      ↑(#(filter K t)) * ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
← sub_add,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) - ↑(#(filter K t)) * ↑(#K.verts) + ↑(#(filter K t)) * (↑t' - ↑t) +
      ↑(#(filter K t)) * ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
he : Even s.ncard
t u : Set α
hutu : t ∪ u = s
hdtu : Disjoint t u
hctu : #↑t = #↑u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
huv : (G.deleteEdges {s(u, v)}).Reachable p.snd v
⊢ (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd

Tactic:
apply hp.isTrail.isEdgeReachable_two <;> simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ G.edgeSet
⊢ e ∈ p.edges

Tactic:
by simpa [Nat.succ_le_iff] using (h e he).ge

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

Goal state before:
pp: case refine_1
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ (completeGraph V).vertexCoverNum
⊢ (completeGraph V).vertexCoverNum ≤ ENat.card V - 1

Tactic:
vertexCoverNum_le_card_sub_one

Goal state after:
case refine_1
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ (completeGraph V).vertexCoverNum
⊢ ENat.card V - 1 ≤ ENat.card V - 1