mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
hi : i < p.firstReturn
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Tactic:
have ne := not_of_lt_findIdx hi
  rw [decide_eq_false_iff_not, ← ne_eq, getElem_range] at ne
  exact lt_of_le_of_ne (p.count_D_le_count_U (i + 1)) ne.symm

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (mu' 𝕜) a b = -∑ x ∈ Ioc a b, (mu' 𝕜) x b

Tactic:
mu'_apply,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜) x b) = -∑ x ∈ Ioc a b, (mu' 𝕜) x b
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
⊢ ∃ j, j ≠ 0 ∧ j * m - 1 = i

Tactic:
refine ⟨j, by grind, Nat.sub_eq_of_eq_add ?_⟩

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
⊢ j * m = i + 1
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
this : ↑(#(A ∩ B)) + ↑(#(A ∪ B)) = ↑(#A) + ↑(#B)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B

Tactic:
have : K * #(A ∩ B) + K * #(A ∪ B) = K * #A + K * #B := by simp only [← mul_add, this]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
this✝ : ↑(#(A ∩ B)) + ↑(#(A ∪ B)) = ↑(#A) + ↑(#B)
this : K * ↑(#(A ∩ B)) + K * ↑(#(A ∪ B)) = K * ↑(#A) + K * ↑(#B)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.IsLoopAt e x ↔ G.IsLoopAt e x

Tactic:
by
  unfold Graph.IsLoopAt
  rw [hHG.isLink_iff he]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ G₁ = G₂

Tactic:
← G₁.mk_eq_self G₁.edge_mem_iff_exists_isLink,

Goal state after:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ { vertexSet := V(G₁), IsLink := G₁.IsLink, edgeSet := E(G₁), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ } =
    G₂
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
h : G.IsLink e x y
⊢ (x ∈ V(G) ∧ x ∉ X) ∧ y ∈ V(G) ∧ y ∉ X ↔ x ∉ X ∧ y ∉ X

Tactic:
simp [h.left_mem, h.right_mem]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
⊢ ↑(vertical v l) x i = Sum.elim v (↑l x) i

Tactic:
cases i

Goal state after:
case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val✝ : ι
⊢ ↑(vertical v l) x (Sum.inl val✝) = Sum.elim v (↑l x) (Sum.inl val✝)

case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val✝ : ι'
⊢ ↑(vertical v l) x (Sum.inr val✝) = Sum.elim v (↑l x) (Sum.inr val✝)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
i : ι ⊕ ι'
⊢ ↑(l.horizontal v) x i = Sum.elim (↑l x) v i

Tactic:
cases i

Goal state after:
case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val✝ : ι
⊢ ↑(l.horizontal v) x (Sum.inl val✝) = Sum.elim (↑l x) v (Sum.inl val✝)

case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val✝ : ι'
⊢ ↑(l.horizontal v) x (Sum.inr val✝) = Sum.elim (↑l x) v (Sum.inr val✝)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
⊢ ↑(l.prod l') x i = Sum.elim (↑l x) (↑l' x) i

Tactic:
cases i

Goal state after:
case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι
⊢ ↑(l.prod l') x (Sum.inl val✝) = Sum.elim (↑l x) (↑l' x) (Sum.inl val✝)

case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι'
⊢ ↑(l.prod l') x (Sum.inr val✝) = Sum.elim (↑l x) (↑l' x) (Sum.inr val✝)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ M.IsBasis B (M.E \ D)

Tactic:
exact h.1.isBasis_ground.isBasis_subset (by simp [subset_sdiff, h.1.subset_ground, h.2])
    sdiff_subset

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
⊢ (fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s))
      ((fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩)) n) =
    n

Tactic:
by
        obtain hns | hsn := lt_or_ge n.1 #s
        · simp [hns]
        · simp [hsn.not_gt, hsn, mem_compl.1 <| Subtype.prop _]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ (M ／ C).IsColoop e ↔ M.IsColoop e ∧ e ∉ C

Tactic:
simp [isColoop_iff_mem_coloops]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
exact H'.2.2

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ (M i).Indep J

Tactic:
convert! hI (Sigma.mk i '' J) (by simpa) (hJ.image _) i

Goal state after:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ J = Sigma.mk i ⁻¹' Sigma.mk i '' J
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
x✝ : ι × α
⊢ x✝ ∈ (Matroid.sum' M).E ↔ x✝ ∈ ⋃ i, Prod.mk i '' (M i).E

Tactic:
simp [Matroid.sum']

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case nil.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝ : V
q : Path r b✝
f : b✝ ⟶ r
⊢ Path.nil = q.cons f

Tactic:
· exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
mcf : HasMaxCutProperty f
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
⊢ ¬AdmitsFractional f ω

Tactic:
intro contr

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
mcf : HasMaxCutProperty f
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
contr : AdmitsFractional f ω
⊢ False
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: case mpr
V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))) →
    ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v

Tactic:
· intro h_no_bidir w h_same_scc
    by_contra hw_ne
    obtain ⟨hab, hba⟩ :=
      exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc
    exact (h_no_bidir w hw_ne) ⟨hba, hab⟩

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩

Tactic:
have h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩ := by
        simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]; exact ⟨hφx, hφp⟩

Goal state after:
case cons.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩
⊢ ⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ insert k (Ioo 0 k) | a ∈ A} ⊆ Ioo 0 k

Tactic:
filter_insert,

Goal state after:
case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ (if k ∈ A then insert k ({a ∈ Ioo 0 k | a ∈ A}) else {a ∈ Ioo 0 k | a ∈ A}) ⊆ Ioo 0 k
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
⊢ x ∈ A

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case mp.inl
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
⊢ 0 ∈ A

case mp.inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
hx : x ≠ 0
⊢ x ∈ A
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Finset ℕ
⊢ schnirelmannDensity ↑A ≤ 0

Tactic:
simp only [schnirelmannDensity_le_iff_forall, zero_add]

Goal state after:
A : Finset ℕ
⊢ ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: m n : ℕ
h : n < m
⊢ ∑ i ∈ range (n + 1), ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i)) = 1

Tactic:
by
  set f : ℕ → ℚ := fun i ↦ n.choose i * (m.choose i : ℚ)⁻¹ with hf
  suffices ∀ i ∈ range (n + 1), f i - f (i + 1) = n.choose i * (m - n) / ((m - i) * m.choose i) by
    rw [← sum_congr rfl this, sum_range_sub', hf]
    simp [choose_zero_right]
  intro i h₁
  rw [mem_range] at h₁
  have h₁ := le_of_lt_succ h₁
  have h₂ := h₁.trans_lt h
  have h₃ := h₂.le
  have hi₄ : (i + 1 : ℚ) ≠ 0 := i.cast_add_one_ne_zero
  have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq m i)
  push_cast at this
  dsimp [f, hf]
  rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]
  have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq n i)
  push_cast at this
  rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]
  have : (m - i : ℚ) ≠ 0 := sub_ne_zero_of_ne (cast_lt.mpr h₂).ne'
  have : (m.choose i : ℚ) ≠ 0 := cast_ne_zero.2 (choose_pos h₂.le).ne'
  simp [field, *]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ (↑m)⁻¹

Tactic:
rw [← one_div, ← @Nat.cast_one ℝ]

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ ↑1 / ↑m
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∈ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a

Tactic:
simp only [mem_upperClosure, mem_coe, not_exists, not_and] at ht
  simp only [truncatedInf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
    upper_aux.2 (Or.inl hs)]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
⊢ ∂^[0] ∅ = ∅

Tactic:
simp [*, shadow_empty]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
n✝ : ℕ
a✝ : ∂^[n✝] ∅ = ∅
⊢ ∂^[n✝ + 1] ∅ = ∅

Tactic:
simp [*, shadow_empty]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a : α
⊢ ↑(birkhoffFinset a) = birkhoffSet a

Tactic:
classical
  -- TODO: This should be a single `simp` call but `simp` refuses to use
  -- `OrderIso.coe_toOrderEmbedding` and `Fintype.coe_finsetOrderIsoSet_symm`
  simp [birkhoffFinset, (OrderIso.coe_toOrderEmbedding)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ 2 * #s ≤ Fintype.card α

Tactic:
refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_

Goal state after:
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ #(s.disjUnion (map { toFun := compl, inj' := ⋯ } s) ⋯) = 2 * #s
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

Tactic:
obtain hjk | r₁ := hjk.lt_or_eq

Goal state after:
case mpr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk✝ : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
hjk : j < k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

case mpr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun t ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ⊆ s
⊢ ∃ u ∈ 𝒜, s ∩ u = t

Tactic:
rwa [← mem_powerset, ← h, mem_image] at ht

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this✝ : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed ∅ ∅ 𝒜

Tactic:
exact isCompressed_self _ _

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
⊢ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜

Tactic:
by
  ext s
  simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
  constructor
  · rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)
    · exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
    refine ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, ?_⟩
    rw [card_erase_of_mem ha, hs]
    rfl
  · rintro ⟨⟨t, ht, hst⟩, hs⟩
    by_cases h : s ∈ 𝒜
    · exact Or.inl ⟨h, hs⟩
    obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_notMem h).symm)
    refine Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, ?_⟩, a, mem_insert_self _ _, erase_insert ha⟩
    rw [card_insert_of_notMem ha, hs]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ insert a t) * f₄ (s ∪ insert a t) + f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›)
        (inter_insert_of_notMem ‹_›) (insert_inter_distrib _ _ _).symm, union_insert,
        insert_union_distrib, ← add_mul]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ (f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Reachable = Relation.ReflTransGen G.Adj

Tactic:
by
  ext
  exact reachable_iff_reflTransGen ..

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
x : V
hadj : G.Adj u x
w' : G.Walk x v
⊢ (G.neighborSet u).Nonempty

Tactic:
exact ⟨x, hadj⟩

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
x✝ : x ∈ ⋃ i, s i ∩ f i ⁻¹' t
a : Set α
i : ι
hi : (fun i ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ a
⊢ x ∈ hs.piecewise f ⁻¹' t

Tactic:
← hi,

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
x✝ : x ∈ ⋃ i, s i ∩ f i ⁻¹' t
a : Set α
i : ι
hi : (fun i ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ (fun i ↦ s i ∩ f i ⁻¹' t) i
⊢ x ∈ hs.piecewise f ⁻¹' t
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case right
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some ⋯.some ∈ s ⋯.some

Tactic:
exact hs.some_mem ((singleton_nonempty k).preimage hg).some

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

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

Tactic:
refine ⟨fun ⟨C⟩ ↦ eq_bot_iff_forall_not_adj.mpr fun u v h ↦ ?_, fun h ↦ h ▸ ⟨0, by simp⟩⟩
  exact C.map_rel h <| Subsingleton.elim ..

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ G.neighborSet v ⊆ t

Tactic:
rw [isBipartiteWith_neighborSet h hv]

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ {w | w ∈ t ∧ G.Adj v w} ⊆ t
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ {w ∈ t | G.Adj v w} = bipartiteAbove G.Adj t v

Tactic:
bipartiteAbove

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ {w ∈ t | G.Adj v w} = {b ∈ t | G.Adj v b}
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → (completeGraph (Fin 2)).Adj (c a) (c b)
v w : V
hvw : (completeGraph (Fin 2)).Adj (c v) (c w)
⊢ v ∈ {v | c v = 0} ∧ w ∈ {v | c v = 1} ∨ v ∈ {v | c v = 1} ∧ w ∈ {v | c v = 0}

Tactic:
simp [Set.mem_ofPred_eq] at hvw ⊢

Goal state after:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → (completeGraph (Fin 2)).Adj (c a) (c b)
v w : V
hvw : ¬c v = c w
⊢ c v = 0 ∧ c w = 1 ∨ c v = 1 ∧ c w = 0
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
⊢ G.IsBipartite

Tactic:
refine ⟨s.indicator 1, fun {v w} hw ↦ ?_⟩
  obtain (⟨hs, ht⟩ | ⟨ht, hs⟩) := h.2 hw <;>
    { replace ht : _ ∉ s := h.1.subset_compl_left ht; simp [hs, ht] }

Goal state after: