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

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).1 < n.succ

pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n.succ

Tactic:
decreasing_by
    · simp_wf; have := fst_le ijh.2; lia
    · simp_wf; have := snd_le ijh.2; lia

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ (c + 1) * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)

Tactic:
pow_succ

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ c * x ! * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A * A) = A⁻¹ * A

Tactic:
by
        rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]
        simp_rw [← coe_inj, coe_mul]
        rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe]

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

Goal state before:
pp: m : Multiset ℕ
⊢ 0 < (map (fun j ↦ j !) m).prod

Tactic:
simp [Nat.factorial_pos]

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

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < (↑p.nest).length
⊢ count D (List.take i ↑p.nest) < count U (List.take i ↑p.nest)

Tactic:
simp_rw [nest, length_append, length_singleton] at ub ⊢

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
⊢ 0 < (map (fun x ↦ x !) m).prod * (count a m)!

Tactic:
simp [Nat.factorial_pos]

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

Goal state before:
pp: case e'_6
p : DyckWord
x✝ : DyckStep
⊢ (x✝ == U) = decide ¬(x✝ == D) = true

Tactic:
rename_i s

Goal state after:
case e'_6
p : DyckWord
s : DyckStep
⊢ (s == U) = decide ¬(s == D) = true
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count U (List.take ((↑p).length - 1 + 1) ↑p) = count D (List.take ((↑p).length - 1 + 1) ↑p)

Tactic:
Nat.sub_add_cancel lp,

Goal state after:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count U (List.take (↑p).length ↑p) = count D (List.take (↑p).length ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ m ! = ∏ x ∈ ∅.erase 0, (count x (replicate m n))!

pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}.erase 0, (count x (replicate m n))!

Tactic:
· rw [hm, factorial_zero, eq_comm]
      rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}.erase 0, (count x (replicate m n))!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) ↑p ++ List.take (p.firstReturn + 1 - (↑p).length) ↑q) =
    count D (List.take (p.firstReturn + 1) ↑p ++ List.take (p.firstReturn + 1 - (↑p).length) ↑q)

Tactic:
show p.firstReturn + 1 - p.toList.length = 0 by lia,

Goal state after:
case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) ↑p ++ List.take 0 ↑q) =
    count D (List.take (p.firstReturn + 1) ↑p ++ List.take 0 ↑q)
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 : α
⊢ muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x

Tactic:
muFun'_apply,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i : ℕ
⊢ Filter.Tendsto (fun j ↦ (f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))).order) Filter.atTop (nhds ⊤)

Tactic:
refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)
  intro m hm
  grw [PowerSeries.smul_eq_C_mul, ← le_order_mul]
  refine lt_add_of_nonneg_of_lt (by simp) ?_
  nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧)
  rw [order_X_pow]
  norm_cast
  grind

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

Goal state before:
pp: case tail.inr.inl
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.insidePart
⊢ p.semilength ≤ r.semilength

pp: case tail.inr.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength

Tactic:
· exact ih.trans (hm ▸ semilength_insidePart_lt hr).le

Goal state after:
case tail.inr.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: k : ℤ
⊢ 2 * ↑(pentagonal k) = k * (3 * k - 1)

Tactic:
natCast_pentagonal

Goal state after:
k : ℤ
⊢ 2 * (k * (3 * k - 1) / 2) = k * (3 * k - 1)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
hrz : (K - 1) * ↑(#A) < ↑(r z)
w : G
hw : w ∈ S
hrw : (2 - K) * ↑(#A) ≤ ↑(r w)
⊢ z •> w ∈ S

Tactic:
← r_inv

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
hrz : (K - 1) * ↑(#A) < ↑(r z⁻¹)
w : G
hw : w ∈ S
hrw : (2 - K) * ↑(#A) ≤ ↑(r w)
⊢ z •> w ∈ S
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ ∑' (n : ℕ), powMulProdOneSubPow k n x + x ^ (3 * k + 5) * ∑' (n : ℕ), powMulProdOneSubPow (k + 1) n x =
    1 - x ^ (2 * k + 3)

Tactic:
show 1 - x ^ (2 * k + 3) = 0 - aux k 0 x by simp [aux]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ ∑' (n : ℕ), powMulProdOneSubPow k n x + x ^ (3 * k + 5) * ∑' (n : ℕ), powMulProdOneSubPow (k + 1) n x = 0 - aux k 0 x
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 * m = i + 1

Tactic:
hj,

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 = m * j
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:

Tactic:
ex (Set.toFinset H)
      _ = κ                               := hH.isFragment
      _ ≤ #(A * S) - K * #A :=
        connectivity_le_expansion hK.le hS <| card_pos.mp <| hS.card_pos.trans_le hA₁
      _ ≤ (2 - ε) * #S - (1 - ε / 2) * #S := by gcongr; linarith
      _ = (1 - ε / 2) * #S                := by linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ y✝ : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
x✝ : ∃ x y, G.IsLink e x y ∧ H.IsLink e x y
x y : α
hfG : G.IsLink e x y
hfH : H.IsLink e x y
z w : α
⊢ s(x, y) = s(z, w) ↔ H.IsLink e z w

Tactic:
hfH.isLink_iff_sym2_eq

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ y✝ : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
x✝ : ∃ x y, G.IsLink e x y ∧ H.IsLink e x y
x y : α
hfG : G.IsLink e x y
hfH : H.IsLink e x y
z w : α
⊢ s(x, y) = s(z, w) ↔ s(x, y) = s(z, w)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type ?u.3
inst✝ : Semigroup M
U V W : Ultrafilter M
p : M → Prop
⊢ (∀ᶠ (x : M) in ↑(U * V * W), p x) ↔ ∀ᶠ (x : M) in ↑(U * (V * W)), p x

Tactic:
by simp [Ultrafilter.eventually_mul, mul_assoc]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x ↦ C (⇑eα.symm ∘ x ∘ ⇑eι)) (l.reindex eη eα eι)

Tactic:
by
  simp [reindex_isMono, Function.comp_assoc]; simpa [← Function.comp_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2.htd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)} ⊆ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}

Tactic:
U

Goal state after:
case refine_2.htd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
⊢ U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)} → U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J

Tactic:
rw [((coloops_indep _).subset hss).contract_indep_iff, delete_indep_iff,
    union_indep_iff_indep_of_subset_coloops hss, and_comm]

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

Goal state before:
pp: σ : 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
this :
  ∃ g' r',
    m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
        ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
obtain ⟨g', r', H'⟩ := this
      use g', r' + monomial (m.degree f) (m.leadingCoeff f)
      constructor
      · simp [← add_assoc, ← H'.1, subLTerm]
      constructor
      · exact fun b ↦ le_trans (H'.2.1 b) (degree_sub_LTerm_le f)
      · intro c hc i
        by_cases hc' : c ∈ r'.support
        · exact H'.2.2 c hc' i
        · convert! hf i
          classical
          have := MvPolynomial.support_add hc
          rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this
          simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')

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

Goal state before:
pp: case inr
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 0 ≠ r 1

Tactic:
rw [ha1, hb0] at hab

Goal state after:
case inr
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 1 ≠ r 0
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha1 : a = r 1
hb0 : b = r 0
⊢ r 0 ≠ r 1
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ f ![a, b] < f r

Tactic:
by
  rw [FractionalOperation.tt, Multiset.mem_map] at rin
  rw [show r = ![r 0, r 1] by simp [← List.ofFn_inj]]
  apply lt_of_le_of_ne (mcf.right (r 0) (r 1)).left
  intro equ
  have asymm : r 0 ≠ r 1 := by
    rcases (mcf.right (r 0) (r 1)).right equ with ⟨ha0, hb1⟩ | ⟨ha1, hb0⟩
    · rw [ha0, hb1] at hab
      exact hab
    · rw [ha1, hb0] at hab
      exact hab.symm
  apply asymm
  obtain ⟨o, in_omega, rfl⟩ := rin
  change o (fun j => ![![a, b], ![b, a]] j 0) = o (fun j => ![![a, b], ![b, a]] j 1)
  convert! symmega ![a, b] ![b, a] (by simp [List.Perm.swap]) o in_omega using 2 <;>
    simp [Matrix.const_fin1_eq]

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length < (p.cons e).length

Tactic:
Path.length_cons,

Goal state after:
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = p.cons e
⊢ (shortestPath r a).length < p.length + 1
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : j = i
⊢ (mapDomain (fun x ↦ i) e) j = (single i (e ())) j

Tactic:
hj,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : j = i
⊢ (mapDomain (fun x ↦ i) e) i = (single i (e ())) i
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case nil.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₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : φ.mapPath Path.nil = Path.cast ⋯ ⋯ ((φ.mapPath p₂).cons (φ.map e₂))
⊢ False

Tactic:
Path.cast_cons

Goal state after:
case nil.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₁ y₂ b✝ : U
p₂ : Path u b✝
e₂ : b✝ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : φ.mapPath Path.nil = (Path.cast ⋯ ⋯ (φ.mapPath p₂)).cons (Hom.cast ⋯ ⋯ (φ.map e₂))
⊢ False
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons.nil
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₂
h : φ.obj y₁ = φ.obj u
h' : Path.cast ⋯ h ((φ.mapPath p₁).cons (φ.map e₁)) = φ.mapPath Path.nil
⊢ False

Tactic:
Path.cast_cons

Goal state after:
case cons.nil
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₂
h : φ.obj y₁ = φ.obj u
h' : (Path.cast ⋯ ⋯ (φ.mapPath p₁)).cons (Hom.cast ⋯ h (φ.map e₁)) = φ.mapPath Path.nil
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) = #𝒜

Tactic:
rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]
  · conv_rhs => rw [← card_filter_add_card_filter_not (fun s => (a ∈ s))]
  · apply (erase_injOn' _).mono
    simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ e (s.truncatedSup a) = (map e.toEmbedding s).truncatedSup (e a)

Tactic:
truncatedSup,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ e (if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤) =
    if h : e a ∈ lowerClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s
h : compress u v a ∉ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
· exact Or.inr ⟨h, a, ha, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Tactic:
exact (subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : ¬(w ∈ s ∪ v ∧ w ∉ u)
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ False

Tactic:
← Classical.not_imp,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : ¬¬(w ∈ s ∪ v → w ∈ u)
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
this : #s ≤ Fintype.card α / 2
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
revert hs

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : #s ≤ Fintype.card α / 2
⊢ (↑s).Intersecting → ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v → Relation.ReflTransGen G.Adj u v

Tactic:
rintro ⟨h⟩
    induction h with
    | nil => rfl
    | cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Set.univ.Nonempty

Tactic:
by
  rw [← Set.nonempty_iff_univ_nonempty]
  exact hconn u v

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y
hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y
⊢ s(x, y) ∉ w.edges

Tactic:
by
  classical
  exact fun hxy ↦ hw.disjoint_edges_takeUntil_dropUntil (w.snd_mem_support_of_mem_edges hxy)
    ((w.takeUntil y _).mem_edges_of_not_reachable_deleteEdges huy)
    (by simpa using (w.dropUntil y _).reverse.mem_edges_of_not_reachable_deleteEdges hvy)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Tactic:
rw [← ENat.natCast_toNat_eq_self] at hne

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : ↑G.chromaticNumber.toNat = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n