mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
z : G
⊢ ∀ x ∈ A, ∀ x_1 ∈ A, x⁻¹ * x_1 = z → ∃ y ∈ A, ∃ a ∈ A, y * a⁻¹ = z

Tactic:
rintro x hx y hy rfl

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ (x •> A ∩ y •> A).Nonempty

Tactic:
by
    simpa using lt_card_smul_inter_smul (K := 2) (mod_cast h) hx hy

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n : ℕ
⊢ catalan (n + 1) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Tactic:
by
  rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n,
    sum_range]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))

Goal state after:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    ∑ i, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i)

d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) = ↑d.succ.centralBinom / (↑d.succ + 1)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take i [U]) + count D (List.take (i - [U].length) ↑p) +
      count D (List.take (i - ([U] ++ ↑p).length) [D]) ≤
    count U (List.take i [U]) + count U (List.take (i - [U].length) ↑p) +
      count U (List.take (i - ([U] ++ ↑p).length) [D])

Tactic:
← add_rotate (count D _),

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) +
      count D (List.take (i - [U].length) ↑p) ≤
    count U (List.take i [U]) + count U (List.take (i - [U].length) ↑p) +
      count U (List.take (i - ([U] ++ ↑p).length) [D])
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e'_2.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

Tactic:
simp only [toFinset_replicate]

Goal state after:
case e'_2.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ x ∈ (if m = 0 then ∅ else {n}).erase 0, (count x (replicate m n))!
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ n.succ * p.parts.bell = (∑ a ∈ p.parts.toFinset, count a p.parts * a) * p.parts.bell

Tactic:
rw [succ_eq_add_one, mul_eq_mul_right_iff]
    left
    simpa [smul_eq_mul, p.parts_sum] using Finset.sum_multiset_count p.parts

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : ¬muFun' 𝕜 b a = 0
⊢ a ≤ b

Tactic:
rw [muFun'_apply] at h
      split_ifs at h with hab
      · exact hab.le
      · rw [neg_eq_zero] at h
        obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h
        exact (nonempty_Ioc.1 ⟨x, hx⟩).le

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mu 𝕜 = mud

Tactic:
suffices mud * zeta 𝕜 = 1 by
    rw [← mu_mul_zeta] at this
    apply_fun (· * mu 𝕜) at this
    symm
    simpa [mul_assoc, zeta_mul_mu] using this

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mud * zeta 𝕜 = 1
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, mud a x = ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x (ofDual a)

Tactic:
simp [Icc_orderDual_def, mud]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ Summable (HPow.hPow (X ^ i * X ^ 1))

Tactic:
exact summable_pow_of_constantCoeff_eq_zero (by simp)

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

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder + ∑ i ∈ Icc ⊥ (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0

Tactic:
← sum_Ioc_add_eq_sum_Icc,

Goal state after:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioc ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder + ⊥.largeSchroder * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingSecond n = (n + 1).choose 2

Tactic:
by
  induction n with
  | zero => simp only [zero_add, stirlingSecond_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
G H : Graph α β
h : x ∈ V(G)
h' : x ∈ V(H)
⊢ ¬Disjoint G H

Tactic:
simp only [Disjoint, le_bot_iff, not_forall, ne_eq, ne_bot_iff]
  use noEdge {x} β
  simp [h, h']

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_1
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
p : AlmostMono C'
x : α
⊢ C (↑(p.line.prod (map some l')) (some x)) = p.color

Tactic:
Line.prod_apply,

Goal state after:
case neg.refine_1
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
p : AlmostMono C'
x : α
⊢ C (Sum.elim (↑p.line (some x)) (↑(map some l') (some x))) = p.color
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
⊢ M ／ C ＼ D = M ＼ D ／ C

Tactic:
wlog hCE : C ⊆ M.E generalizing C with aux

Goal state after:
case inr
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α}, Disjoint C D → C ⊆ M.E → M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
⊢ M ／ C ＼ D = M ＼ D ／ C

α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ＼ D = M ＼ D ／ C
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
I : Set α
⊢ (Matroid.disjointSigma M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E

Tactic:
by
  simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i ↦ (M i).E)
B : Set α
⊢ (Matroid.disjointSigma M h).IsBase B ↔ (∀ (i : ι), (M i).IsBase (B ∩ (M i).E)) ∧ B ⊆ ⋃ i, (M i).E

Tactic:
by
  simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

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

Goal state before:
pp: case e'_2.e'_1
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' I =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk false ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I

Tactic:
simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

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

Goal state before:
pp: case e'_2.e'_2
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' I =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk true ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I

Tactic:
simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

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

Goal state before:
pp: case e'_2.e'_1
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' B =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk false ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B

Tactic:
simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

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

Goal state before:
pp: case e'_2.e'_2
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' B =
    (fun a ↦ Equiv.ulift a) ''
      Sigma.mk true ⁻¹'
        (fun a ↦ (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
          (fun a ↦ Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B

Tactic:
simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

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

Goal state before:
pp: case neg
σ : 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
⊢ ∃ 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

Tactic:
by_cases hf'0 : m.subLTerm f = 0

Goal state after:
case pos
σ : 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
hf'0 : m.subLTerm f = 0
⊢ ∃ 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

case neg
σ : 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
hf'0 : ¬m.subLTerm f = 0
⊢ ∃ 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
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
hf'0 : m.subLTerm f = 0
⊢ m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) 0 + 0

Tactic:
by simp [hf'0]

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E

Tactic:
← inter_union_distrib_left,

Goal state after:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ (M.E ∪ N.E)
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ B = B ∩ M.E ∪ B ∩ N.E

Tactic:
← inter_union_distrib_left,

Goal state after:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ B = B ∩ (M.E ∪ N.E)
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
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ 2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
have half_sharp :
      ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
      ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
      apply Multiset.sum_lt_sum
      · intro r rin
        exact le_of_lt (mcfab.rows_lt_aux hab symmega rin)
      · obtain ⟨g, _⟩ := valid.contains
        have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
        exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩

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
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
half_sharp :
  (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ 2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
cases hv' with

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

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

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
| #𝒜

Tactic:
← filter_union_filter_not_eq (fun s => (erase s a ∈ 𝒜)) 𝒜

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
| #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
⊢ x ≤ m → x % m = 1 → x = 1

Tactic:
hxm

Goal state after:
case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
⊢ x % m = 1 → x = 1
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : SemilatticeSup α
s : Finset α
⊢ s ⊻ s = s ↔ SupClosed ↑s

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : SemilatticeInf α
s : Finset α
⊢ s ⊼ s = s ↔ InfClosed ↑s

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u

Tactic:
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩

Goal state after:
case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
⊢ s ∩ u ∪ t ∩ u = u

case refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u

Tactic:
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩

Goal state after:
case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∩ t
⊢ s ∩ u ∩ (t ∩ u) = u

case refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u) → u ⊆ s ∩ t
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ 𝓒 u u s = s

Tactic:
grind [mem_compression]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) → ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
rintro ⟨u, rfl, htu, hsuA⟩
    exact ⟨_, hsuA, subset_union_left, by rw [union_sdiff_cancel_left htu]⟩

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Tactic:
rintro ⟨u, rfl, hut, htu⟩

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = #u
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

Tactic:
obtain hs | hs := le_total (Fintype.card α) #s

Goal state after:
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

case inr
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : #s ≤ Fintype.card α
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧
      (toColex t = toColex (s.erase (s.min' hs)) ∨
        ∃ w, (w ∈ s.erase (s.min' hs) ∧ w ∉ t) ∧ {a ∈ t | w < a} = {a ∈ s.erase (s.min' hs) | w < a}) →
    ∃ a ∉ t,
      #s = #(insert a t) ∧
        (toColex (insert a t) = toColex s ∨ ∃ w, (w ∈ s ∧ w ∉ insert a t) ∧ {a ∈ insert a t | w < a} = {a ∈ s | w < a})

Tactic:
filter_inj,

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧
      (toColex t = toColex (s.erase (s.min' hs)) ∨
        ∃ w, (w ∈ s.erase (s.min' hs) ∧ w ∉ t) ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
    ∃ a ∉ t,
      #s = #(insert a t) ∧
        (toColex (insert a t) = toColex s ∨
          ∃ w, (w ∈ s ∧ w ∉ insert a t) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(#𝒜) / ↑((Fintype.card α).choose r) ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))

Tactic:
rw [div_le_div_iff₀] <;> norm_cast

Goal state after:
case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r

case inr.hb
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose r

case inr.hd
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose (r - 1)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w, (w ∈ s ∧ w ∉ (s ⊔ U) \ V) ∧ {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}

Tactic:
filter_inj,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w, (w ∈ s ∧ w ∉ (s ⊔ U) \ V) ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ ∃ a ∈ 𝒜, s ⊆ a

Tactic:
exact h.exists_superset

Goal state after: