mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case a
n : ℕ
α : Type := ⋯
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ Iio ⟨n, ⋯⟩ ⊆ univ

Tactic:
exact subset_univ _

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ (fun n ↦ ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n ↦ ↑(ruzsaSzemerediNumberNat n)

Tactic:
trans fun n ↦ (n / 3 - 2) * ↑((n - 3) / 6) * exp (-4 * √(log ↑((n - 3) / 6)))

Goal state after:
⊢ (fun n ↦ ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n ↦
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

⊢ (fun n ↦ (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) =O[atTop] fun n ↦
    ↑(ruzsaSzemerediNumberNat n)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ Sum.inl a = m.idxFun i

Tactic:
cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a

Tactic:
let S : Set (Ultrafilter M) := ⋂ n, { U | ∀ᶠ m in U, m ∈ FP (a.drop n) }
  have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
  · rcases h with ⟨U, hU, U_idem⟩
    refine ⟨U, U_idem, ?_⟩
    convert! Set.mem_iInter.mp hU 0
  · exact Ultrafilter.continuous_mul_left
  · apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
    · intro n U hU
      filter_upwards [hU]
      rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]
      exact FP.tail _
    · intro n
      exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
    · exact (ultrafilter_isClosed_basic _).isCompact
    · intro n
      apply ultrafilter_isClosed_basic
  · exact IsClosed.isCompact (isClosed_iInter fun i => ultrafilter_isClosed_basic _)
  · intro U hU V hV
    rw [Set.mem_iInter] at *
    intro n
    rw [Set.mem_ofPred_eq, Ultrafilter.eventually_mul]
    filter_upwards [hU n] with m hm
    obtain ⟨n', hn⟩ := FP.mul hm
    filter_upwards [hV (n' + n)] with m' hm'
    apply hn
    simpa only [Stream'.drop_drop, add_comm] using hm'

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ＼ D).Dep X ↔ M.Dep X ∧ Disjoint X D

Tactic:
rw [dep_iff, dep_iff, delete_indep_iff, delete_ground, subset_sdiff]

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M ＼ D).IsBasis' I X ↔ M.IsBasis' I (X \ D)

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, delete_isBasis_iff, delete_ground, sdiff_eq,
    inter_comm M.E, ← inter_assoc, ← sdiff_eq, ← isBasis'_iff_isBasis_inter_ground,
    and_iff_left_iff_imp, inter_comm, ← inter_sdiff_assoc]
  exact fun _ ↦ disjoint_sdiff_left

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
apply FP.cons
    rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm]
    refine Set.mem_of_subset_of_mem ?_ (ih _ (s.min'_mem hs) h)
    have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h :=
      Nat.succ_le_of_lt (Finset.min'_lt_of_mem_erase_min' _ _ <| Finset.min'_mem _ _)
    obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_le this
    rw [hd, ← Stream'.drop_drop, add_comm]
    apply FP_drop_subset_FP

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤m M
⊢ M.IsNonloop e

Tactic:
by
  obtain ⟨C, D, rfl⟩ := hNM
  exact h.of_delete.of_contract

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J

Tactic:
by
  rw [hI.contract_eq_contract_delete, delete_indep_iff, hI.indep.contract_indep_iff,
    and_comm, ← and_assoc, ← disjoint_union_right, sdiff_union_self,
    union_eq_self_of_subset_right hI.subset, and_comm, disjoint_comm]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

Tactic:
by
  wlog hCE : C ⊆ M.E with aux
  · rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      sdiff_inter, sdiff_eq_empty.2 (M.closure_subset_ground _), union_empty]
  obtain ⟨I, hI⟩ := M.exists_isBasis C
  rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete,
    delete_delete, union_comm, sdiff_union_sdiff_cancel (M.subset_closure C) hI.subset]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
I : Set α
⊢ (Matroid.disjointSigma M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E

Tactic:
simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
B : Set α
⊢ (Matroid.disjointSigma M h).IsBase B ↔ (∀ (i : ι), (M i).IsBase (B ∩ (M i).E)) ∧ B ⊆ ⋃ i, (M i).E

Tactic:
simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • (f ![a, b] + f ![a, b])
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ False

Tactic:
← two_nsmul

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ False
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b c : WideSubquiver.toType V (geodesicSubtree r)⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f

Tactic:
rintro a b c ⟨e, p, h⟩ ⟨f, q, j⟩
      cases h.symm.trans j
      constructor <;> rfl

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

Goal state before:
pp: case succ
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
p : Path a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = n + 1
h_pos : 0 < p.length
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
obtain ⟨c, p', e, rfl⟩ := (length_ne_zero_iff_eq_cons p).mp h_pos.ne'

Goal state after:
case succ
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

Tactic:
ext ⟨v, f | g⟩ <;>
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [Quiver.symmetrifyStar]`
    simp only [Quiver.symmetrifyStar, Function.comp_apply]

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inl f⟩)

case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inr g⟩)
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case insert.refine_2
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u

Tactic:
· simp only [mem_memberSubfamily, and_imp]
      exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs

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:
← hcardst,

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) = #t + k
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x x✝ : α
⊢ (mkClasses c H) x x✝ ↔ (mkClasses c H) x✝ x

Tactic:
Setoid.comm'

Goal state after:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x x✝ : α
⊢ (mkClasses c H) x✝ x ↔ (mkClasses c H) x✝ x
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Relation.ReflGen (fromEdgeSet s).Adj x✝¹ x✝ ↔ Relation.ReflGen (Sym2.ToRel s) x✝¹ x✝

Tactic:
simpa [Relation.reflGen_iff] using by tauto

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ i + r - i ≤ k

Tactic:
Nat.add_sub_cancel_left

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ r ≤ k
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C.supp
hv : v ∈ C.supp
⊢ G.Reachable u v

Tactic:
by
  rw [mem_supp_iff] at hu hv
  exact ConnectedComponent.exact (hv ▸ hu)

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

Goal state before:
pp: case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = i + r - i
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
Nat.add_sub_cancel_left

Goal state after:
case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ #A = 0

Tactic:
← b

Goal state after:
case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ #A = r
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.chromaticNumber ≤ 1

Tactic:
by
  rw [← Nat.cast_one, chromaticNumber_le_iff_colorable]
  refine ⟨Coloring.mk (fun _ => 0) ?_⟩
  intro v w
  cases Subsingleton.elim v w
  simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
⊢ G.chromaticNumber ≤ ↑(card V)

Tactic:
← chromaticNumber_top

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
⊢ G.chromaticNumber ≤ ⊤.chromaticNumber
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : G.Adj v w
⊢ v ∈ s

Tactic:
by
  apply h.mem_of_adj at hadj
  have nhw : w ∉ s := Set.disjoint_right.mp h.disjoint hw
  simpa [hw, nhw] using hadj

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
⊢ {v ∈ s | G.Adj v w} ⊆ s

Tactic:
exact filter_subset (G.Adj · w) s

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ Walk.map (cons h✝ w).toSubgraph.hom (cons h✝ w).mapToSubgraph = cons h✝ w

Tactic:
rw [mapToSubgraph, Walk.map, map_map]
    exact congrArg₂ _ rfl w.map_mapToSubgraph_hom

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = G.dist v u

Tactic:
rw [dist, dist, edist_comm]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 1 ↔ G.Adj u v

pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ 1 ≠ 0

Tactic:
edist_eq_one_iff_adj

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.Adj u v ↔ G.Adj u v

V : Type u_1
G : SimpleGraph V
u v : V
⊢ 1 ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = 1 ↔ G.Adj u v

Tactic:
by
  rw [dist, ENat.toNat_eq_iff, ENat.natCast_one, edist_eq_one_iff_adj]
  decide

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
hadj : G.Adj v (p.getVert 2)
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2

Tactic:
have : G.dist v w ≤ p.tail.tail.length + 1 :=
      dist_le <| p.tail.tail.cons <| p.getVert_tail ▸ hadj
    lia

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

Goal state before:
pp: case refine_1.inr.inl.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ ↑left.toRight
j : V
hj : j ∈ ↑right.toLeft
⊢ G.Adj i j

Tactic:
rw [mem_coe, mem_toRight] at hi
        rw [mem_coe, mem_toLeft] at hj
        simpa using h hi hj

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

Goal state before:
pp: case refine_1.inr.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1

Tactic:
· simpa using h hl hr

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

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

Tactic:
cases n

Goal state after:
case zero
⊢ cycleGraph (0 + 1) = circulantGraph {1}

case succ
n✝ : ℕ
⊢ cycleGraph (n✝ + 1 + 1) = circulantGraph {1}
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
x✝ : V
⊢ A.diag x✝ = 0 x✝

Tactic:
simp [h.apply_diag]

Goal state after:
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✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
f : W → V
i : W
⊢ A.submatrix f f i i = 0

Tactic:
simp [h.apply_diag]

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 → α
⊢ (vec ⬝ᵥ fun i ↦ adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v

Tactic:
refine congr rfl ?_

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i ↦ adjMatrix α G i v) = adjMatrix α G v
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: 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
⊢ ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1

Tactic:
refine ⟨u, v, hp.nil_iff_eq.not.mp hnil, ?_, ?_⟩ <;>
    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

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.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
h1 : ¬G.Adj (e 1) (e 2)
⊢ False

Tactic:
have h2 : G.Adj (e 0) (e 2) := by simp [pathGraph_adj]

Goal state after:
α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
h1 : ¬G.Adj (e 1) (e 2)
h2 : G.Adj (e 0) (e 2)
⊢ False
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
z : Finset V
⊢ #z = r → ¬∀ ⦃x : V⦄, x ∈ ↑z → ∀ ⦃y : V⦄, y ∈ ↑z → x ≠ y → G.Adj x y

Tactic:
zc

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
z : Finset V
zc : #z = r
⊢ ¬∀ ⦃x : V⦄, x ∈ ↑z → ∀ ⦃y : V⦄, y ∈ ↑z → x ≠ y → G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⟨↑v₁, ⋯⟩
⊢ ↑v₁ = ↑v₂

Tactic:
have hv' : F c₁ v₁ = F c₂ v₁' := by
      apply congr_heq
      · rw [hc]
      · rw [Subtype.heq_iff_coe_eq]
        simp [hc]

Goal state after:
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⟨↑v₁, ⋯⟩
hv' : (F c₁) v₁ = (F c₂) v₁'
⊢ ↑v₁ = ↑v₂
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
⊢ Even (K.supp \ s).ncard

Tactic:
· have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
    rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by lia)]
    simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h

Goal state after: