mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ G.edgeFinset.card = {default}ᶜ.card

Tactic:
refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj

Goal state after:
case notNil
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
w : V
hw : w ∈ {default}ᶜ
⊢ ¬(f w).Nil

case memEdges
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}ᶜ
⊢ ((f a).firstDart ⋯).edge ∈ G.edgeFinset

case inj
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₂

case surj
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
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = b
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
w : V
hw : w ∈ {default}ᶜ
⊢ w ≠ default

Tactic:
by simpa using hw

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

Goal state before:
pp: n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
⊢ ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
    H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H

Tactic:
intro _

Goal state after:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G✝ : SimpleGraph (Fin n)
⊢ ∀ [inst : DecidableRel G✝.Adj], H'.Free G✝ → #G✝.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case refine_2.inr
n r : ℕ
h : n ≤ r
a b : Fin n
⊢ ↑a % r = ↑b % r ↔ a = b

Tactic:
rw [Nat.mod_eq_of_lt (a.2.trans_le h), Nat.mod_eq_of_lt (b.2.trans_le h), Fin.val_inj]

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

Goal state before:
pp: case right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
⊢ #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset

Tactic:
rw [card_edgeFinset_replaceVertex_of_not_adj _ this,
    card_edgeFinset_replaceVertex_of_not_adj _ hst, dst, Nat.add_sub_cancel]

Goal state after:
case right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
⊢ #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
⊢ False

Tactic:
rw [← h2] at hOdd

Goal state after:
n : ℕ
h : 2 ≤ n
hOdd : Odd 2
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
⊢ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length

Tactic:
intro _

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u✝ : α
⊢ ∀ (w : G.Walk u✝ u✝), ¬Odd w.length
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Pairwise fun k l ↦ Disjoint (C.labelGraph k) (C.labelGraph l)

Tactic:
intro _

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i✝ : K
⊢ ∀ ⦃j : K⦄, i✝ ≠ j → (fun k l ↦ Disjoint (C.labelGraph k) (C.labelGraph l)) i✝ j
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Set.univ.PairwiseDisjoint C.labelGraph

Tactic:
intro _

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x✝ : K
⊢ x✝ ∈ Set.univ → ∀ ⦃y : K⦄, y ∈ Set.univ → x✝ ≠ y → Function.onFun Disjoint C.labelGraph x✝ y
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ Injective fun x ↦
    match x with
    | 0 => w₁
    | 1 => v
    | 2 => w₂

Tactic:
intro _

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ : Fin 3
⊢ ∀ ⦃a₂ : Fin 3⦄,
    (fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂)
          a₁✝ =
        (fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂)
          a₂ →
      a₁✝ = a₂
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 b : Fin 3},
    G.Adj
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          b) ↔
      (pathGraph 3)ᶜ.Adj a b

Tactic:
intro _

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ : Fin 3
⊢ ∀ {b : Fin 3},
    G.Adj
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          a✝)
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          b) ↔
      (pathGraph 3)ᶜ.Adj a✝ b
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_1
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
hr : 0 < r
right✝ : 0 < t
⊢ ↑v % r < r

Tactic:
exact Nat.mod_lt v hr

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
n : ℕ
hn : 3 ≤ n
⊢ G.CliqueFree n

Tactic:
refine not_cliqueFree_iff_top_isContained n |>.not_right.mpr fun hle ↦ ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
n : ℕ
hn : 3 ≤ n
hle : completeGraph (Fin n) ⊑ G
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
⊢ G.eccent u ≠ 0

Tactic:
obtain ⟨v, huv⟩ := exists_ne ‹_›

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : v ≠ u
⊢ G.eccent u ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ ⨆ u, (fun u ↦ ⨆ v, G.edist u v) u = ⨆ p, G.edist p.1 p.2

Tactic:
iSup_prod

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ ⨆ u, (fun u ↦ ⨆ v, G.edist u v) u = ⨆ i, ⨆ j, G.edist (i, j).1 (i, j).2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

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

Tactic:
intro _

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
⊢ v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts → ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl.inr
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hcy : C y = C v
hx : x = w₁
hy : y ∈ ↑t
⊢ False

Tactic:
apply (C.valid _ hcy.symm).elim
      exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G.subgraphOfAdj h).IsMatching

Tactic:
intro _

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
⊢ v✝ ∈ (G.subgraphOfAdj h).verts → ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
⊢ (Subgraph.coeSubgraph M).IsMatching

Tactic:
intro _

Goal state after:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
⊢ v✝ ∈ (Subgraph.coeSubgraph M).verts → ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
⊢ (M.induce (M.verts ∩ c.supp)).IsMatching

Tactic:
intro _

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v✝ : V
⊢ v✝ ∈ (M.induce (M.verts ∩ c.supp)).verts → ∃! w, (M.induce (M.verts ∩ c.supp)).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : ¬v = a
⊢ False

Tactic:
· exact haj <| hw.isNClique_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
⊢ ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x

Tactic:
intro _

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
w✝ : α
⊢ w✝ ∈ W → w✝ ≠ a → w✝ ≠ b → G.Adj w✝ x
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2

Tactic:
apply hpc.ncard_neighborSet_toSubgraph_eq_two

Goal state after:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ v ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := ⋯
w x : V
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).Adj w x ↔ c.toSubgraph.spanningCoe.Adj w x

Tactic:
simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
      Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
w x : V
⊢ p.toSubgraph.Adj w x ∨ (w = v ∧ x = u ∨ w = u ∧ x = v) ∧ w ≠ x ↔ s(v, u) = s(w, x) ∨ p.toSubgraph.Adj w x
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ Cardinal.mk ↑(G.neighborSet v) = Cardinal.mk ↑(p.toSubgraph.neighborSet v)

Tactic:
← Set.cast_ncard (Set.toFinite _),

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ ↑(G.neighborSet v).ncard = Cardinal.mk ↑(p.toSubgraph.neighborSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ Cardinal.mk ↑(G.neighborSet (p.getVert n)) = Cardinal.mk ↑(p.toSubgraph.neighborSet (p.getVert n))

Tactic:
← Set.cast_ncard (Set.toFinite _),

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ ↑(G.neighborSet (p.getVert n)).ncard = Cardinal.mk ↑(p.toSubgraph.neighborSet (p.getVert n))
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ ↑(G.neighborSet (p.getVert n)).ncard = Cardinal.mk ↑(p.toSubgraph.neighborSet (p.getVert n))

Tactic:
← Set.cast_ncard (Set.toFinite _),

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ ↑(G.neighborSet (p.getVert n)).ncard = ↑(p.toSubgraph.neighborSet (p.getVert n)).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: V : Type u_1
r : V
⊢ (starGraph r).IsUniversal r

Tactic:
intro _

Goal state after:
V : Type u_1
r w✝ : V
⊢ r ≠ w✝ → (starGraph r).Adj r w✝
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ Cardinal.mk ↑(G.neighborSet v) = Cardinal.mk ↑(p.toSubgraph.neighborSet v)

Tactic:
← Set.cast_ncard (Set.toFinite _),

Goal state after:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ ↑(G.neighborSet v).ncard = Cardinal.mk ↑(p.toSubgraph.neighborSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ ↑(G.neighborSet v).ncard = Cardinal.mk ↑(p.toSubgraph.neighborSet v)

Tactic:
← Set.cast_ncard (Set.toFinite _),

Goal state after:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ ↑(G.neighborSet v).ncard = ↑(p.toSubgraph.neighborSet v).ncard
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
⊢ ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})

Tactic:
intro _

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x✝ : α
⊢ x✝ ∈ X → 3 ≤ #({z ∈ W | ¬G.Adj x✝ z})
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
have bdW := sum_degree_le_of_le_not_adj dXle (fun y _ ↦ one_le y)

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
x✝¹ x✝ : ℕ × ℕ
h : x✝ ≤ x✝¹
⊢ x✝¹ ∈ ↑((Equiv.prodComm ℕ ℕ).finsetCongr μ.cells) → x✝ ∈ ↑((Equiv.prodComm ℕ ℕ).finsetCongr μ.cells)

Tactic:
simp only [Finset.mem_coe, Equiv.finsetCongr_apply, Finset.mem_map_equiv]
    intro hcell
    apply μ.isLowerSet _ hcell
    simp [h]

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
c : ℕ × ℕ
⊢ c ∈ μ.transpose ↔ c.swap ∈ μ

Tactic:
simp [transpose]

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i : ℕ
hi : i < μ.colLen 0
⊢ 0 < μ.rowLen i

Tactic:
← mem_iff_lt_colLen,

Goal state after:
μ : YoungDiagram
i : ℕ
hi : (i, 0) ∈ μ
⊢ 0 < μ.rowLen i
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt : PlacedTile ps
a b : G
r :
  (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries)) a b
⊢ a • ↑(↑ps pt.index) = b • ↑(↑ps pt.index)

Tactic:
QuotientGroup.leftRel_eq

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt : PlacedTile ps
a b : G
r : a⁻¹ * b ∈ Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries
⊢ a • ↑(↑ps pt.index) = b • ↑(↑ps pt.index)
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
pt : PlacedTile ps
a b : G
r :
  (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries)) a b
⊢ { index := pt.index, groupElts := ↑(g * a) } = { index := pt.index, groupElts := ↑(g * b) }

Tactic:
QuotientGroup.leftRel_eq

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
pt : PlacedTile ps
a b : G
r : a⁻¹ * b ∈ Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries
⊢ { index := pt.index, groupElts := ↑(g * a) } = { index := pt.index, groupElts := ↑(g * b) }
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g • ↑pt ↔ g⁻¹ • x ∈ ↑pt

Tactic:
Set.mem_smul_set_iff_inv_smul_mem

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec f

Tactic:
let := Primcodable.subtype hp
  refine ⟨fun h => ?_, fun hf => subtype_val.comp hf⟩
  refine Nat.Primrec.of_eq h fun n => ?_
  rcases @decode α _ n with - | a; · rfl
  simp; rfl

Goal state after: