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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a

Tactic:
classical
  obtain rfl | hf := hf.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
    simp [hfg]
  obtain rfl | hg := hg.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
    simp [hfg]
  have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ
  · simpa [hfg, sum_pos hg] using this
  · simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
    rw [sup_comm, inf_comm]
    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _

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

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

Tactic:
by_cases hadj : G.Adj v (p.getVert 2)

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

case neg
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
hadj : ¬G.Adj v (p.getVert 2)
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ G.Adj x.1 a' ∧ x.2 = b' ∨ H.Adj x.2 b' ∧ x.1 = a' ↔ G.Adj x.1 a' ∧ b' = x.2 ∨ a' = x.1 ∧ H.Adj x.2 b'

Tactic:
simp only [eq_comm, and_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ G.Adj x.1 y.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ H.Adj x.2 y.2 ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1

Tactic:
simp only [eq_comm, and_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊔ H ⊔ K).Connected

Tactic:
refine Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_
  · exact (top_induce_pair_connected_of_adj huv).preconnected
  · exact ⟨u, by simp [uH]⟩
  · exact ⟨v, by simp [vK]⟩

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

Goal state before:
pp: case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
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
hle : x > y
hab : n + ↑⟨y, hy⟩ - ↑⟨x, hx⟩ = 1
⊢ G.Adj p.support[⟨n, ⋯⟩] p.support[⟨0 + 1, ⋯⟩]

Tactic:
simp [← hp₂, p.adj_snd hp₁.not_nil]

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

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

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

Tactic:
· exact card_bij (fun j hj ↦ .inl j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getLeft <| (hmem_right hj).left Sum.isLeft_inl, by simp [hj]⟩)

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
⊢ ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right

Tactic:
· simp_rw [← card_left, ← card_right]
    refine ⟨left.map .inl, right.map .inr, card_map _, card_map _, fun i hi j hj ↦ ?_⟩
    simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj
    obtain ⟨i', hi', hi⟩ := hi
    obtain ⟨j', hj', hj⟩ := hj
    simpa [← hi, ← hj] using h hi' hj'

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (G.subgraphOfAdj h).coe.IsTree

Tactic:
by
  refine ⟨Subgraph.subgraphOfAdj_connected h, fun w p hp ↦ ?_⟩
  have : _ = _ := p.adj_snd hp.not_nil
  have : _ = _ := p.adj_penultimate hp.not_nil
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was:
  `grind [Sym2.eq_iff, IsCycle.snd_ne_penultimate]` -/
  simp_all
  grind [IsCycle.snd_ne_penultimate]

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

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
rw [Finset.sup_le_iff]

Goal state after:
case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
rw [Finset.sup_le_iff]

Goal state after:
case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ∀ b ∈ {G | H.Free G}, #b.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.IsExtremal H.Free ↔ H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H

Tactic:
by
  rw [IsExtremal, and_congr_right_iff, ← extremalNumber_le_iff]
  exact fun h ↦ ⟨eq_of_le_of_ge (card_edgeFinset_le_extremalNumber h), ge_of_eq⟩

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

Goal state before:
pp: case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ Even (Walk.cons h p).length ↔ (c u = true ↔ c w = true)

Tactic:
simp only [Walk.length_cons, Nat.even_add_one]

Goal state after:
case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬Even p.length ↔ (c u = true ↔ c w = true)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ Even p.length ↔ (c u = true ↔ c v = true)

Tactic:
by
  induction p with
  | nil => simp
  | @cons u v w h p ih =>
    simp only [Walk.length_cons, Nat.even_add_one]
    have : ¬ c u = true ↔ c v = true := by
      rw [← not_iff, ← Bool.eq_iff_iff]
      exact c.valid h
    tauto

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

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ #((completeEquipartiteGraph r t).neighborFinset v) = (r - 1) * t

Tactic:
neighborFinset_completeEquipartiteGraph v,

Goal state after:
r t : ℕ
v : Fin r × Fin t
⊢ #({v.1}ᶜ ×ˢ univ) = (r - 1) * t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
⊢ G.IsTuranMaximal r

Tactic:
obtain ⟨J, _, j⟩ := exists_isTuranMaximal (V := V) hr

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
⊢ G.IsTuranMaximal r
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x✝¹ : G.ConnectedComponent
x✝ : x✝¹ ∈ C
⊢ x✝¹ ∈ G.connectedComponentMk '' Quot.out '' C

Tactic:
by simpa [connectedComponentMk]

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

Goal state before:
pp: case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬G.Connected

Tactic:
connected_iff

Goal state after:
case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬(G.Preconnected ∧ Nonempty α)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.ediam.toNat = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

Tactic:
ENat.toNat_eq_zero,

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = 0 ∨ G.ediam = ⊤ ↔ G.ediam = ⊤ ∨ Subsingleton α
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ (n' ^ 2 - (n' % r) ^ 2) * (r - 1) / (2 * r) + (n' % r).choose 2 + n' * (r - 1) + r.choose 2 =
    ((n' + r) ^ 2 - ((n' + r) % r) ^ 2) * (r - 1) / (2 * r) + ((n' + r) % r).choose 2

Tactic:
ring₁,

Goal state after:
case inr.inr
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ n' % r * (n' / r) * (r - 1) + r * (r - 1) * (n' / r) ^ 2 / 2 + (n' % r).choose 2 + n' * (r - 1) + r.choose 2 =
    ((n' + r) ^ 2 - ((n' + r) % r) ^ 2) * (r - 1) / (2 * r) + ((n' + r) % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ n' % r * (n' / r) * (r - 1) + r * (r - 1) * (n' / r) ^ 2 / 2 + (n' % r).choose 2 + n' * (r - 1) + r.choose 2 =
    ((n' + r) ^ 2 - ((n' + r) % r) ^ 2) * (r - 1) / (2 * r) + ((n' + r) % r).choose 2

Tactic:
ring₁,

Goal state after:
case inr.inr
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
⊢ n' % r * (n' / r) * (r - 1) + r * (r - 1) * (n' / r) ^ 2 / 2 + (n' % r).choose 2 + n' * (r - 1) + r.choose 2 =
    (n' + r) % r * ((n' + r) / r) * (r - 1) + r * (r - 1) * ((n' + r) / r) ^ 2 / 2 + ((n' + r) % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : G.CliqueFree (0 + 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

Tactic:
cliqueFree_one,

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : IsEmpty V
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
rw [hs.ncard]

Goal state after:
case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : 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
p2 : G.IsPathGraph3Compl v w₁ w₂
d1 : v ∉ s
d2 : v ∉ t
d3 : w₁ ∉ s
d4 : w₂ ∉ t
c1 : G.IsNClique (r + 1) (insert v s)
c2 : G.IsNClique (r + 1) (insert w₁ s)
c3 : G.IsNClique (r + 1) (insert v t)
c4 : G.IsNClique (r + 1) (insert w₂ t)
hk : #(s ∩ t) = k
⊢ #(t ∩ s) = k

Tactic:
rwa [inter_comm]

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

Goal state before:
pp: case h.refine_1
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv✝ : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
v : { x // x ∈ G'.verts }
hv : v ∈ M.verts ∧ ↑v = v✝
⊢ ∃ (h : v✝ ∈ G'.verts), M.Adj ⟨v✝, ⋯⟩ w

Tactic:
exact ⟨hv.2 ▸ v.2, hw.1⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ M.support = M.verts

Tactic:
refine M.support_subset_verts.antisymm fun v hv => ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ v ∈ M.support
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 = ↑2

Tactic:
hcyc (Set.nonempty_of_mem hadj.symm)

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)
⊢ ↑2 = ↑2
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ G.ediam ≤ 2

Tactic:
rw [ediam_le_iff]

Goal state after:
case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ ∀ (u v : V), G.edist u v ≤ 2
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
⊢ ↑(Fintype.card ↑{p | p.length = 2}) =
    (k • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0

Tactic:
rw [@Fintype.card_congr _ _ (G.fintypeSetWalkLength v w 2) _
    (G.walkLengthTwoEquivCommonNeighbors v w)]

Goal state after:
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ List.count e p.edges ≤ 1

Tactic:
by_cases he : e ∈ p.edges

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ p.edges
⊢ List.count e p.edges ≤ 1

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∉ p.edges
⊢ List.count e p.edges ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.edgeSet = G.edgeSet

Tactic:
by
  rwa [← h.isTrail.isEulerian_iff]

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

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < w[(i2, j2).1]
⊢ w[i2] ≤ w[i1]

Tactic:
obtain rfl | h := eq_or_lt_of_le hi
        · rfl
        · exact hw.getElem_ge_getElem_of_le h.le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f

Tactic:
show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p ↦ f p.1 p.2) ↔ Primrec₂ f
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
l : List β
x : σ
⊢ (G a)^[n + 1] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)

Tactic:
simp only [iterate_succ, comp_apply]
    rcases l with - | ⟨b, l⟩ <;> simp [G, IH]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
        (ofNat (List ℕ) n).reverse) =
    encode (decode n)

Tactic:
rw [List.foldl_reverse]
        apply Nat.case_strong_induction_on n; · simp
        intro n IH; simp
        rcases @decode α _ n.unpair.1 with - | a; · rfl
        simp only [Option.bind_some, Option.map_some]
        suffices ∀ (o : Option (List ℕ)) (p), encode o = encode p →
            encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p) from
          this _ _ (IH _ (Nat.unpair_right_le n))
        intro o p IH
        cases o <;> cases p
        · rfl
        · injection IH
        · injection IH
        · exact congr_arg (fun k => (Nat.pair (encode a) k).succ.succ) (Nat.succ.inj IH)

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun b ↦ f n = b) (g n) = f n

Tactic:
exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a ↦ List.ofFn fun i ↦ f i a

Tactic:
simp only [List.ofFn_succ]

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a ↦ f 0 a :: List.ofFn fun i ↦ f i.succ a