mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ ↑wG.length + ↑wH.length = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
simp only [hwG, hwH]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (induce s G).Preconnected ↔ (⊤.induce s).Preconnected

Tactic:
induce_eq_coe_induce_top,

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).coe.Preconnected ↔ (⊤.induce s).Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (induce s G).Connected ↔ (⊤.induce s).Connected

Tactic:
induce_eq_coe_induce_top,

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).coe.Connected ↔ (⊤.induce s).Connected
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: ⊢ ∀ (x x_1 : Fin 2), (cycleGraph 2).Adj x x_1 = ⊤.Adj x x_1

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (x x_1 : Fin 3), (cycleGraph 3).Adj x x_1 = ⊤.Adj x x_1

Tactic:
decide

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

Goal state before:
pp: n : ℕ
⊢ (have hadj := ⋯;
      cons hadj (cycleCons n (Fin.last (n + 2)))).length =
    n + 3

Tactic:
simp [cycleGraph.length_cycle_cons]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
⊢ cycleGraph n ⊑ G ↔ ∃ v p, p.IsCycle ∧ p.length = n

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h' ↦ ?_⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph n).Copy G
⊢ ∃ v p, p.IsCycle ∧ p.length = n

case refine_2
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
h' : ∃ v p, p.IsCycle ∧ p.length = n
⊢ cycleGraph n ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley s

Tactic:
by
  nth_rw 2 [← Set.sdiff_union_inter s {1}]
  rw [mulCayley_union]
  ext u v
  simp +contextual [mulCayley_adj']

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m

Tactic:
simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.sup_le_iff, mem_filter_univ]

Goal state after:
V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ (∀ (b : SimpleGraph V), H.Free b → #b.edgeFinset ≤ m) ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₁ H₁ = extremalNumber n₂ H₂

Tactic:
by
  rw [h, le_antisymm_iff]
  and_intros
  on_goal 2 =>
    replace e := e.symm
  all_goals
    rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
    intro G _ h
    apply card_edgeFinset_le_extremalNumber
    contrapose h
    exact h.trans' ⟨e.toCopy⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
⊢ G.IsTree ↔ G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V

Tactic:
refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
⊢ G.IsAcyclic
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
⊢ G.minDegree = 1

pp: case neg
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : ¬2 ≤ G.minDegree
⊢ G.minDegree = 1

Tactic:
· have := h.card_edgeFinset
    have := G.sum_degrees_eq_twice_card_edges
    have hle : ∑ v : V, 2 ≤ ∑ v, G.degree v := by
      gcongr
      exact le_trans q (G.minDegree_le_degree _)
    rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] at hle
    lia

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : ¬2 ≤ G.minDegree
⊢ G.minDegree = 1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ ∃ x, True

Tactic:
classical
  use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)
  /- Each path between vertex u and another vertex in G.induce {v}ᶜ
  is contained in G.induce {v}ᶜ. -/
  intro z hz
  rw [Set.mem_compl_iff, Set.mem_singleton_iff]
  obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz
  /- Prove vertex v is not in the path formed from the concatenated walks
  by showing that vertex u must then be passed twice. -/
  by_contra
  subst_vars
  refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_
  rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]
  have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))
  simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this
  have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))
  rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this
  lia

Goal state after:
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 < min (#univ) r
⊢ False

Tactic:
lt_min_iff

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
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case inl
r t : ℕ
ht_eq0 : t = 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
rw [completeEquipartiteGraph_eq_bot_iff.mpr (Or.inr ht_eq0)]

Goal state after:
case inl
r t : ℕ
ht_eq0 : t = 0
⊢ ⊥.IsCompleteMultipartite
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

Tactic:
by
  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.Diam

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

Tactic:
eq_top_iff,

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

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

Tactic:
cases eq_or_ne u v <;> simp_all [edist_top_of_ne]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ G.ediam = ⊤

Tactic:
eq_top_iff,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ ⊤ ≤ G.ediam
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.Connected
⊢ G.ediam = ⊤

Tactic:
rw [connected_iff_exists_forall_reachable] at h
  push Not at h
  obtain ⟨_, hw⟩ := h Classical.ofNonempty
  rw [eq_top_iff, ← edist_eq_top_of_not_reachable hw]
  exact edist_le_ediam

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

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

Tactic:
exact Or.inl ediam_eq_zero_of_subsingleton

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
⊢ Set.univ = ↑C

Tactic:
symm

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := ⋯
dis : K ∩ ↑C ⊆ ∅ := ⋯
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
⊢ ↑C = Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ↑(sSup (range fun i ↦ f i)) = ⨆ i, ↑(f i)

Tactic:
coe_sSup,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ⨆ G_1 ∈ range fun i ↦ f i, ↑G_1 = ⨆ i, ↑(f i)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
rw [ncard_eq_toFinset_card s hs] at he

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2

Tactic:
rw [le_div_iff₀' (by positivity), ← Nat.cast_two, ← Nat.cast_mul, Nat.cast_le]

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ 2 * #G.edgeFinset ≤ zarankiewicz n n s t
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case 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 : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
hx : x ∈ ↑s
⊢ False

Tactic:
apply (C.valid _ hcx.symm).elim

Goal state after:
α : 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 : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
hx : x ∈ ↑s
⊢ G.Adj v x
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
⊢ ∃ h, Bijective h ∧ ∀ (a : ↑p₁), G.Adj ↑a ↑(h a)

Tactic:
classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : V) (h : x ∈ p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) (h : x ∈ p₂) : f x ∉ p₂ := h₁.disjoint |>.notMem_of_mem_left <|
    isBipartiteWith_neighborSet_subset h₁.symm h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ incMatrix R G a e * incMatrix R G b e = 0

Tactic:
by
  rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_notMem]
  rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]
  exact Set.notMem_empty e

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

Goal state before:
pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
⊢ ↑(#{x | e ∈ G.incidenceSet x}) = 0

Tactic:
revert h
    refine e.ind ?_
    intro v w h
    simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this✝ : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
this : Even (M.induce c.supp).verts.toFinset.card
⊢ Even (Fintype.card ↑c.supp)

Tactic:
simp only [Subgraph.induce_verts, Set.toFinset_card] at this

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this✝ : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
this : Even (Fintype.card ↑c.supp)
⊢ Even (Fintype.card ↑c.supp)
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})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
have xcle : ∀ x ∈ Xᶜ, 1 ≤ #{z ∈ s ∩ t | ¬ G.Adj x z} := by
    intro x hx
    apply card_pos.2
    obtain ⟨_, hy⟩ : ∃ y ∈ s ∩ t, ¬ G.Adj x y := by
      contrapose! hx
      simpa [X] using hx
    exact ⟨_, mem_filter.2 hy⟩

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)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case inl
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v u : V
ha : v ≠ u ∧ ¬G.Adj v u
hne : v ≠ u
⊢ ¬G.Adj v u ∧ ¬G.Adj u u

Tactic:
simpa [adj_comm] using ha.2

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

Goal state before:
pp: case inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
w u : V
ha : u ≠ w ∧ ¬G.Adj u w
hne : u ≠ w
⊢ ¬G.Adj u u ∧ ¬G.Adj w u

Tactic:
simpa [adj_comm] using ha.2

Goal state after:
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 ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.liftOn' groupElts (fun g ↦ g • ↑(↑ps index)) ⋯).Nonempty ↔ (↑(↑ps index)).Nonempty

Tactic:
← groupElts.out_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 ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ ((Quotient.mk'' (Quotient.out groupElts)).liftOn' (fun g ↦ g • ↑(↑ps index)) ⋯).Nonempty ↔ (↑(↑ps index)).Nonempty
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 ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.liftOn' groupElts (fun g ↦ g • ↑(↑ps index)) ⋯).Finite ↔ (↑(↑ps index)).Finite

Tactic:
← groupElts.out_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 ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ ((Quotient.mk'' (Quotient.out groupElts)).liftOn' (fun g ↦ g • ↑(↑ps index)) ⋯).Finite ↔ (↑(↑ps index)).Finite
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (Option.map some (decode n))

Tactic:
cases @decode α _ n <;> simp

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

Goal state before:
pp: case some.zero
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) 0 =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) 0) + 1

Tactic:
simp [*, encodek]

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

Goal state before:
pp: case some.succ
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
n✝ : ℕ
a✝ :
  Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) n✝ =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) n✝) + 1
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) (n✝ + 1) =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (n✝ + 1)) + 1

Tactic:
simp [*, encodek]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
l : List α
n : ℕ
⊢ Sum.rec (fun val ↦ none) (fun val ↦ some val) (F l n) = l[n]?

Tactic:
symm

Goal state after:
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α := ⋯
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
l : List α
n : ℕ
⊢ l[n]? = Sum.rec (fun val ↦ none) (fun val ↦ some val) (F l n)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode (decode n) = encode (Option.map Subtype.val (decode n))

Tactic:
rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩) <;> rfl

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

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
⊢ b ∈ bs ∧ bs' ⊆ bs

Tactic:
simpa using has

Goal state after: