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

Goal state before:
pp: case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ (Fintype.card α + 1) * (#(f' i) + #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
    2 ^ (Fintype.card α + 1) * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]

Goal state after:
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 * #(f' i)) + 2 * (2 ^ Fintype.card α * #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)

Tactic:
← (Set.Sized.shadow h𝒜) hs,

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - #s
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer

Tactic:
intro a

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ ∀ ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case zero
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
hk : 0 ≤ Fintype.card α
⊢ ∑ r ∈ range (0 + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
    ↑(#(falling (Fintype.card α - 0) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - 0))

Tactic:
| zero =>

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

Goal state before:
pp: case pos
α : 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 ∈ ℬ
⊢ f₃ (s ∩ insert a t) * f₄ (s ∪ insert a t) + f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›)
        (inter_insert_of_notMem ‹_›) (insert_inter_distrib _ _ _).symm,

Goal state after:
case pos
α : 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 ∈ ℬ
⊢ f₃ (s ∩ insert a t) * f₄ (s ∪ insert a t) + f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) ≤ 1

Tactic:
div_le_iff₀

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) ≤ 1 * ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))

𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ s
⊢ x ∈ {x | (mkClasses c H) x y}

Tactic:
_s'

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ s
_s' : Set α
⊢ _s' ∈ c → x ∈ _s' → y ∈ _s'
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case zero
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[0] 𝒞) ≤ #(∂^[0] 𝒜)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mpr
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes

Tactic:
· exact exists_of_mem_partition hc

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

Goal state before:
pp: case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
⊢ ∀ {a b : β},
    (SimpleGraph.map (⇑f) G).Adj a b →
      (completeGraph (Fin n)).Adj (extend (⇑f) (⇑C) (const β default) a) (extend (⇑f) (⇑C) (const β default) b)

Tactic:
intro a

Goal state after:
case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a : β
⊢ ∀ {b : β},
    (SimpleGraph.map (⇑f) G).Adj a b →
      (completeGraph (Fin n)).Adj (extend (⇑f) (⇑C) (const β default) a) (extend (⇑f) (⇑C) (const β default) b)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
⊢ G.Colorable n

Tactic:
have : G.chromaticNumber ≠ ⊤ := (trans h (ENat.natCast_lt_top n)).ne

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : G.chromaticNumber ≠ ⊤
⊢ G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber = ↑n + 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

Tactic:
eq_iff_le_not_lt,

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n + 1 ∧ ¬G.chromaticNumber < ↑n + 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≤ ⨅ n ∈ Set.ofPred G'.Colorable, ↑n

Tactic:
simp only [Set.mem_ofPred_eq, le_iInf_iff]

Goal state after:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ∀ (i : ℕ), G'.Colorable i → ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑i
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
⊢ (∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges

Tactic:
rintro ⟨u, c, hc, he⟩

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
⊢ G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
e : Sym2 V
⊢ (G.deleteEdges {e}).IsBridge e ↔ G.IsBridge e

Tactic:
induction e with

Goal state after:
case h
V : Type u
G : SimpleGraph V
u v : V
⊢ (G.deleteEdges {s(u, v)}).IsBridge s(u, v) ↔ G.IsBridge s(u, v)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
this : G.Coloring ↥(Finset.univ.erase b)
⊢ G.Colorable (card V - 1)

Tactic:
by simpa using Coloring.colorable this

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
⊢ 2 ≤ G.chromaticNumber

Tactic:
by
  refine le_of_not_gt fun h ↦ ?_
  obtain ⟨c⟩ := chromaticNumber_le_iff_colorable.mp (Order.le_of_lt_add_one h)
  exact c.valid hadj (Subsingleton.elim (c u) (c v))

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

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

Tactic:
eq_iff_le_not_lt,

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber < 1 ↔ G = ⊥ ∧ Nonempty V
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
⊢ ∀ {v w : V ⊕ W}, (completeBipartiteGraph V W).Adj v w → v.isRight ≠ w.isRight

Tactic:
by
      intro v w
      cases v <;> cases w <;> simp

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

Goal state before:
pp: case zero
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree 0
⊢ (completeMultipartiteGraph V).Colorable (0 - 1)

Tactic:
| zero =>

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
⊢ ∑ v ∈ s, G.degree v = ∑ x ∈ t.attach, G.degree ↑x

Tactic:
← sum_attach s,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ x ∈ s.attach, G.degree ↑x = ∑ x ∈ t.attach, G.degree ↑x
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
w u v x : V
p : G.Walk u v
hadj : p.toSubgraph.Adj w x
⊢ ¬p.Nil

Tactic:
by
  cases p <;> simp_all

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

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: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
⊢ G.dist u w ≤ G.dist u v + G.dist v w

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

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

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

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

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

Goal state before:
pp: case h.inl
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
use x, hxs, hx, h.le

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

Goal state before:
pp: case refine_2.refine_2.inr
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
this :
  ∀ {V : Type u_1} {G : SimpleGraph V} {n : ℕ},
    2 < n →
      ∀ (a : V) (p : G.Walk a a),
        p.IsCycle →
          ∀ (hp₂ : p.length = n) (x : ℕ) (hx : x < n) (y : ℕ) (hy : y < n),
            (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩ → x ≠ y → x > y → G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
hle : ¬x > y
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
exact this hn a p hp₁ hp₂ y hy x hx hab.symm hne.symm (by lia) |>.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: case zero
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
⊢ ↑(G.finsetWalkLength 0 u v) = {p | p.length = 0}

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: case succ
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
⊢ ↑(G.finsetWalkLength (n + 1) u v) = {p | p.length = n + 1}

Tactic:
simp only [finsetWalkLength, Walk.setOfPred_length_eq_add_one, Finset.coe_biUnion,
      Finset.mem_coe, Finset.mem_univ, Set.iUnion_true, Finset.coe_map, Set.iUnion_coe_set]
    congr!
    grind

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
hc : G.Connected
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
hu : ⟨p, hp⟩ = q
⊢ p = ↑q

Tactic:
exact Subtype.ext_iff.mp hu

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

Tactic:
intro a

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
⊢ ∀ (ha₁ : a ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a = a₂
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

Tactic:
| zero =>

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

Goal state before:
pp: case map_rel'
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
⊢ ∀ {a b : ↥c},
    c.toSimpleGraph.Adj a b →
      (completeGraph (Fin 2)).Adj (Fin.ofNat 2 (Nonempty.some ⋯).length) (Fin.ofNat 2 (Nonempty.some ⋯).length)

Tactic:
intro a

Goal state after:
case map_rel'
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a : ↥c
⊢ ∀ {b : ↥c},
    c.toSimpleGraph.Adj a b →
      (completeGraph (Fin 2)).Adj (Fin.ofNat 2 (Nonempty.some ⋯).length) (Fin.ofNat 2 (Nonempty.some ⋯).length)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ a₂✝ : Fin 3
a✝ :
  (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₁✝ =
    (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₂✝
this✝ : v ≠ w₁
this : v ≠ w₂
⊢ a₁✝ = a₂✝

Tactic:
have := h.adj.ne

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ a₂✝ : Fin 3
a✝ :
  (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₁✝ =
    (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₂✝
this✝¹ : v ≠ w₁
this✝ : v ≠ w₂
this : w₁ ≠ w₂
⊢ a₁✝ = a₂✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_1
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
e : Sym2 (Fin r × Fin t)
he : e ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
induction e with

Goal state after:
case refine_1.h
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : s(v₁, v₂) ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)
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
  · rw [completeEquipartiteGraph_eq_bot_iff.mpr (Or.inr ht_eq0)]
    exact bot_isCompleteMultipartite
  · rw [isCompleteMultipartite_iff]
    use (Fin r), const (Fin r) (Fin t)
    simp_rw [const_apply, exists_prop]
    exact ⟨const (Fin r) (Fin.pos_iff_nonempty.mp ht_pos),
      ⟨completeEquipartiteGraph.completeMultipartiteGraph⟩⟩

Goal state after:
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},
    (turanGraph (Fintype.card V) r).Adj (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) a)
        (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) b) ↔
      G.Adj a b

Tactic:
intro a

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 : V
⊢ ∀ {b : V},
    (turanGraph (Fintype.card V) r).Adj (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) a)
        (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) b) ↔
      G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ ∀ ⦃a : V⦄, a ∈ s → a ∉ c.supp

Tactic:
intro a

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
⊢ a ∈ s → a ∉ c.supp
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
⊢ ⊥.ediam.toNat = 0

Tactic:
ENat.toNat_eq_zero

Goal state after:
α : Type u_1
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
α : Type u_1
h✝ : Subsingleton α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
⊢ ⊥.center = Set.univ

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
α : Type u_1
h✝ : Subsingleton α
⊢ ⊥.center = Set.univ

case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊥.center = Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
⊢ ⊤.center = Set.univ

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
α : Type u_1
h✝ : Subsingleton α
⊢ ⊤.center = Set.univ

case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊤.center = Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

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

Tactic:
· 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: