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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
⊢ s.erase a ≠ t

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
ht : s.erase a ∈ 𝒜
hst : s ⊆ s.erase a
⊢ False
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
h : mkClasses x.toSet ⋯ = mkClasses y.toSet ⋯ := le_antisymm hx hy
⊢ x = y

Tactic:
rw [Partitions.ext_iff, ← classes_mkClasses x.toSet x.isPartition,
      ← classes_mkClasses y.toSet y.isPartition, h]

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
⊢ (G.connectedComponentMk v).supp ⊆ c'.supp

Tactic:
intro v' hv'

Goal state after:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : v' ∈ (G.connectedComponentMk v).supp
⊢ v' ∈ c'.supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
he : G.IsBridge s(u, v)
⊢ u ≠ v

Tactic:
rintro rfl

Goal state after:
V : Type u
G : SimpleGraph V
u : V
he : G.IsBridge s(u, u)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
⊢ G.Reachable w v

Tactic:
by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom

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

Goal state before:
pp: case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty

Tactic:
obtain ⟨w, hw⟩ := exists_walk_of_edist_eq_coe h

Goal state after:
case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ (G.commonNeighbors u v).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.map (G.boxProdRight G a).toHom w).ofBoxProdRight = cons' x y z h w

pp: case hc
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (a, x).2 ((G.boxProdRight G a).toHom y).2 ∧ (a, x).1 = ((G.boxProdRight G a).toHom y).1

Tactic:
←
      Walk.boxProdRight

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w

case hc
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (a, x).2 ((G.boxProdRight G a).toHom y).2 ∧ (a, x).1 = ((G.boxProdRight G a).toHom y).1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
⊢ (sSup Hs).IsAcyclic

Tactic:
rcases Hs.eq_empty_or_nonempty with rfl | hnemp
  · simp
  · intro u p hp
    obtain ⟨H, hH, hpH⟩ := p.exists_mem_contains_edges_of_directed Hs hnemp h_dir
    exact h_acyc H hH (p.transfer H hpH) <| Walk.IsCycle.transfer hp hpH

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v : V
p q : G.Path u v
⊢ p = q

Tactic:
have := p.isPath.exists_isCycle_of_ne q.isPath
    grind [IsAcyclic, Subtype.coe_inj]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w = p.reverse.snd

Tactic:
apply h.eq_snd_of_adj_start hp.reverse hadj

Goal state after:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj v w
hsupp : w ∈ p.support
⊢ w ∈ p.reverse.support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ p.support

Tactic:
Subtype.mk.inj <| hG.subsingleton_path u v |>.elim ⟨p, hp⟩ ⟨_, hq.concat hv hadj.symm⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ (q.concat ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
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
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ¬y = default

Tactic:
rintro rfl

Goal state after:
case refine_1
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
x : V
h : G.Adj x default
h' : (f x).length ≤ (f default).length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
⊢ G'.Adj u v

Tactic:
have := congrArg Walk.edges <| congrArg Subtype.val <|
    htree.isAcyclic.subsingleton_path u v |>.elim ⟨p.mapLe hle, hp.mapLe hle⟩ <| Path.singleton hadj

Goal state after:
V : Type u_1
G : SimpleGraph V
htree : G.IsTree
G' : SimpleGraph V
h' : G'.Connected
hle : G' ≤ G
u v : V
hadj : G.Adj u v
p : G'.Walk u v
hp : p.IsPath
this : (↑⟨mapLe hle p, ⋯⟩).edges = (↑(Path.singleton hadj)).edges
⊢ G'.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ #(completeEquipartiteGraph r t).edgeFinset = r.choose 2 * t ^ 2

Tactic:
rw [← mul_right_inj' two_ne_zero, ← sum_degrees_eq_twice_card_edges]
  conv_lhs =>
    rhs; intro v
    rw [degree_completeEquipartiteGraph v]
  rw [sum_const, smul_eq_mul, card_univ, card_prod, Fintype.card_fin, Fintype.card_fin]
  conv_rhs =>
    rw [← Nat.mul_assoc, Nat.choose_two_right, Nat.mul_div_cancel' r.even_mul_pred_self.two_dvd]
  rw [← mul_assoc, mul_comm r _, mul_assoc t _ _, mul_comm t, mul_assoc _ t, ← pow_two]

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
this :
  h.finpartition.part ↑⟨a, ⋯⟩ = h.finpartition.part ↑⟨b, ⋯⟩ ↔
    ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
⊢ ↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b

Tactic:
rw [← h.not_adj_iff_part_eq] at this

Goal state after:
case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
⊢ ↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b
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
⊢ G ⊑ completeEquipartiteGraph n t

Tactic:
by
  have (c : Fin n) : Nonempty (C.colorClass c ↪ Fin t) := by
    rw [Embedding.nonempty_iff_card_le, Fintype.card_fin]
    exact h c
  have F (c : Fin n) := Classical.arbitrary (C.colorClass c ↪ Fin t)
  have hF {c₁ c₂ v₁ v₂} (hc : c₁ = c₂) (hv : F c₁ v₁ = F c₂ v₂) : v₁.val = v₂.val := by
    let v₁' : C.colorClass c₂ := ⟨v₁, by simp [← hc]⟩
    have hv' : F c₁ v₁ = F c₂ v₁' := by
      apply congr_heq
      · rw [hc]
      · rw [Subtype.heq_iff_coe_eq]
        simp [hc]
    rw [hv'] at hv
    simpa [Subtype.ext_iff] using (F c₂).injective hv
  use ⟨fun v ↦ (C v, F (C v) ⟨v, C.mem_colorClass v⟩), C.valid⟩
  intro v w h
  rw [Prod.mk.injEq] at h
  exact hF h.1 h.2

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

Goal state before:
pp: case neg.refine_2.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ #(cons s K.parts ⋯) = r + 1 ∨ t = 0

pp: case neg.refine_2.refine_3
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ ∀ {p : Finset V}, p ∈ cons s K.parts ⋯ → #p = t

pp: case neg.refine_2.refine_4
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ (↑(cons s K.parts ⋯)).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2

Tactic:
· rw [Finset.card_cons, K.card_parts.resolve_right ht]
        exact .inl rfl

Goal state after:
case neg.refine_2.refine_3
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ ∀ {p : Finset V}, p ∈ cons s K.parts ⋯ → #p = t

case neg.refine_2.refine_4
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ (↑(cons s K.parts ⋯)).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D → ∃ x ∈ ↑C, x ∈ ↑D

Tactic:
rintro rfl

Goal state after:
case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
⊢ ∃ x ∈ ↑C, x ∈ ↑(hom h C)
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (ComponentCompl.supp C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K

Tactic:
by
  simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter,
    Set.mem_range, componentComplFunctor_map]
  exact
    ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL =>
      h (Opposite.op L) (opHomOfLE KL)⟩

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
x✝ : ∃ b, (b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b) ∧ x < #b.edgeFinset
w✝ : SimpleGraph (V ⊕ W)
h_le : w✝ ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free w✝
h_lt : x < #w✝.edgeFinset
⊢ x < #w✝.edgeFinset

Tactic:
by convert h_lt

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fintype.card α = Fintype.card α - 1 + 1

Tactic:
Nat.sub_one_add_one Fintype.card_ne_zero

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s
⊢ G.Adj v ↑(f ⟨v, hv⟩)

pp: case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w

Tactic:
· exact hadj ⟨v, _⟩

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : 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₁
hax : x = a
⊢ v ≠ x

Tactic:
rintro rfl

Goal state after:
case pos
α : 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
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : 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₁
hax : ¬x = a
⊢ v ≠ x

Tactic:
rintro rfl

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : 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₁
hax : x = a
⊢ w₁ ≠ x

Tactic:
rintro rfl

Goal state after:
case pos
α : 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 w₁ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₁ z}) ≤ 2
haj : ¬G.Adj w₁ a
hbj : ¬G.Adj w₁ b
hcj : ¬G.Adj w₁ a
hdj : ¬G.Adj w₁ b
hax : w₁ = a
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : 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₁
hax : ¬x = a
⊢ w₁ ≠ x

Tactic:
rintro rfl

Goal state after:
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 w₁ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₁ z}) ≤ 2
haj : ¬G.Adj w₁ a
hbj : ¬G.Adj w₁ b
hcj : ¬G.Adj w₁ a
hdj : ¬G.Adj w₁ b
hax : ¬w₁ = a
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : 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₁
hbx : x = b
⊢ w₂ ≠ x

Tactic:
rintro rfl

Goal state after:
case pos
α : 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 w₂ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₂ z}) ≤ 2
haj : ¬G.Adj w₂ a
hbj : ¬G.Adj w₂ b
hcj : ¬G.Adj w₂ a
hdj : ¬G.Adj w₂ b
hbx : w₂ = b
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : 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₁
hbx : ¬x = b
⊢ w₂ ≠ x

Tactic:
rintro rfl

Goal state after:
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 w₂ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₂ z}) ≤ 2
haj : ¬G.Adj w₂ a
hbj : ¬G.Adj w₂ b
hcj : ¬G.Adj w₂ a
hdj : ¬G.Adj w₂ b
hbx : ¬w₂ = b
⊢ False
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
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₁ (insert x (s.erase a)))

Tactic:
exact hw.isNClique_fst_left.insert_insert_erase has hw.fst_notMem fun _ hz hZ ↦
               wa (h1s hz) hZ fun h ↦ hbw <| (mem_insert.1 (h ▸ hz)).resolve_right hbs

Goal state after: