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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))

Tactic:
have : ε ≤ G.edgeDensity {y ∈ t | G.Adj x y} {y ∈ u | G.Adj x y} := by
    rw [abs_sub_lt_iff] at this; linarith

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this : ε ≤ ↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * ↑(#G.edgeFinset) - 2 * ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    ↑(#{x | G.Adj x.1 x.2}) - ↑(#{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})

pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ {x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2} ⊆ {x | G.Adj x.1 x.2}

Tactic:
· norm_cast
        rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ {x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2} ⊆ {x | G.Adj x.1 x.2}
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(s ×ˢ t) ≤ Eₘ[s, t]

Tactic:
exact card_le_card_of_injOn (fun x => ((x.1, x.1), x.2, x.2)) (by simp [Set.MapsTo]) (by simp)

Goal state after:
Module: Mathlib.Combinatorics.Additive.Randomisation

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) =
    ∑ t, (𝔼 a, ∏ ψ ∈ t, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, ↑(c ψ)

Tactic:
by
        simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]

Goal state after:
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_2.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ p ∣ #{a_1 | ↑x a_1 ≠ 0}

Tactic:
← CharP.cast_eq_zero_iff (ZMod p),

Goal state after:
case refine_2.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ ↑(#{a_1 | ↑x a_1 ≠ 0}) = 0
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case composite
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i

Tactic:
suffices ∀ k ≤ 2 * m - 1, ∃ 𝒜 : Finset (Finset ι), #𝒜 = k ∧
      (𝒜 : Set (Finset ι)).Pairwise _root_.Disjoint ∧
        ∀ ⦃t⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i by
     -- Assume `𝒜` is a family of `2 * m - 1` sets, each of size `n` and sum divisible by `n`.
      obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := this _ le_rfl
      -- By induction hypothesis on `m`, find a subfamily `ℬ` of size `m` such that the sum over
      -- `t ∈ ℬ` of `(∑ i ∈ t, a i) / n` is divisible by `m`.
      obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge
      -- We are done.
      refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).1, ?_, ?_⟩
      · rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1, hℬcard]
      rwa [sum_biUnion, Int.natCast_mul, mul_comm, ← Int.dvd_div_iff_mul_dvd, Int.sum_div]
      · exact fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.2
      · exact dvd_sum fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.2
      · exact h𝒜disj.mono hℬ𝒜

Goal state after:
case composite
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
⊢ ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a

Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
    singleton_le_singleton]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : Fintype.card L ≤ #(s.biUnion t) + (Fintype.card L - #s)
⊢ #s ≤ #(s.biUnion t)

Tactic:
rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
simp [pointCount]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), f l ∉ l
hf3 : Function.Bijective f
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
exact ⟨f, hf3, fun l ↦ (sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
        ((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ <| mem_univ _⟩

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
⊢ lineCount L p = lineCount L q

Tactic:
cases nonempty_fintype P
  cases nonempty_fintype L
  obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
  have h := card_points_eq_card_lines P L
  let n := lineCount L p₂
  have hp₂ : lineCount L p₂ = n := rfl
  have hl₁ : pointCount P l₁ = n := (HasLines.lineCount_eq_pointCount h h₂₁).symm.trans hp₂
  have hp₃ : lineCount L p₃ = n := (HasLines.lineCount_eq_pointCount h h₃₁).trans hl₁
  have hl₃ : pointCount P l₃ = n := (HasLines.lineCount_eq_pointCount h h₃₃).symm.trans hp₃
  have hp₁ : lineCount L p₁ = n := (HasLines.lineCount_eq_pointCount h h₁₃).trans hl₃
  have hl₂ : pointCount P l₂ = n := (HasLines.lineCount_eq_pointCount h h₁₂).symm.trans hp₁
  suffices ∀ p : P, lineCount L p = n by exact (this p).trans (this q).symm
  refine fun p =>
    or_not.elim (fun h₂ => ?_) fun h₂ => (HasLines.lineCount_eq_pointCount h h₂).trans hl₂
  refine or_not.elim (fun h₃ => ?_) fun h₃ => (HasLines.lineCount_eq_pointCount h h₃).trans hl₃
  rw [(eq_or_eq h₂ h₂₂ h₃ h₂₃).resolve_right fun h =>
      h₃₃ ((congr_arg (p₃ ∈ ·) h).mp h₃₂)]

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

Goal state before:
pp: x : BinaryTree Unit
n : ℕ
⊢ x ∈ treesOfNumNodesEq n ↔ x.numNodes = n

Tactic:
induction x using BinaryTree.unitRecOn generalizing n <;> cases n <;>
    simp [treesOfNumNodesEq_succ, *]

Goal state after:
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)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this✝² : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this✝¹ : #l = #A
this✝ : #r = #A
this : #(l ∪ r) < 2 * #A
t : G
ht : t ∈ A ∧ t⁻¹ * z ∈ A
⊢ ∃ y ∈ A, ∃ z_1 ∈ A, y * z_1 = z

Tactic:
exact ⟨t, ht.1, t⁻¹ * z, ht.2, by simp⟩

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑p)

Tactic:
have := p.count_U_eq_count_D

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
this : count U ↑p = count D ↑p
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
hn : p.IsNested
⊢ count U (↑p).dropLast.tail = count D (↑p).dropLast.tail

Tactic:
have := p.count_U_eq_count_D

Goal state after:
p q : DyckWord
h : p ≠ 0
hn : p.IsNested
this : count U ↑p = count D ↑p
⊢ count U (↑p).dropLast.tail = count D (↑p).dropLast.tail
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m n : ℕ
hm : m = 0
⊢ (multinomial ∅ fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ ∅.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

pp: case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
· simp [hm]

Goal state after:
case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: 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
this : (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
⊢ ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
calc
          (#Z : ℝ)
      _ = (Fintype.card H / #S : ℝ)⁻¹ := by simp [← card_H_mul_card_Z]
      _ ≤ (((φ - K) * (K - ψ) / ((2 - K) * K) * #S) / #S)⁻¹ := by gcongr
      _ = (2 - K) * K / ((φ - K) * (K - ψ)) := by
        have : (#S : ℝ) ≠ 0 := by positivity
        simp [this]

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ List.take (p.firstReturn + 1) ↑(p + q) = List.take (p.firstReturn + 1) ↑p

Tactic:
exact take_append_of_le_length (firstReturn_lt_length h)

Goal state after:
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)
this✝ : K * ↑(#(A ∩ B)) + K * ↑(#(A ∪ B)) = K * ↑(#A) + K * ↑(#B)
this : ↑(#(A * S ∩ (B * S))) + ↑(#(A * S ∪ B * S)) = ↑(#(A * S)) + ↑(#(B * S))
⊢ ↑(#(A ∩ B * S)) ≤ ↑(#(A * S ∩ (B * S)))

Tactic:
inter_mul_subset

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)
this : ↑(#(A * S ∩ (B * S))) + ↑(#(A * S ∪ B * S)) = ↑(#(A * S)) + ↑(#(B * S))
⊢ ↑(#(A * S ∩ (B * S))) ≤ ↑(#(A * S ∩ (B * S)))
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)
this✝¹ : K * ↑(#(A ∩ B)) + K * ↑(#(A ∪ B)) = K * ↑(#A) + K * ↑(#B)
this✝ : ↑(#(A * S ∩ (B * S))) + ↑(#(A * S ∪ B * S)) = ↑(#(A * S)) + ↑(#(B * S))
this : ↑(#(A ∩ B * S)) ≤ ↑(#(A * S ∩ (B * S)))
⊢ ↑(#(A ∩ B * S)) - K * ↑(#(A ∩ B)) + (↑(#((A ∪ B) * S)) - K * ↑(#(A ∪ B))) ≤
    ↑(#(A * S)) - K * ↑(#A) + (↑(#(B * S)) - K * ↑(#B))

Tactic:
union_mul

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)
this✝ : ↑(#(A * S ∩ (B * S))) + ↑(#(A * S ∪ B * S)) = ↑(#(A * S)) + ↑(#(B * S))
this : ↑(#(A ∩ B * S)) ≤ ↑(#(A * S ∩ (B * S)))
⊢ ↑(#(A ∩ B * S)) - K * ↑(#(A ∩ B)) + (↑(#(A * S ∪ B * S)) - K * ↑(#(A ∪ B))) ≤
    ↑(#(A * S)) - K * ↑(#A) + (↑(#(B * S)) - K * ↑(#B))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case calc_1
n : ℕ
⊢ n ≤ 2 * 3 * (n / 6 + 1)

Tactic:
exact (Nat.lt_mul_div_succ _ <| by simp).le

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

Goal state before:
pp: case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → (ofSimpleGraph G).Adj ↑a✝ ↑b✝

Tactic:
rw [ofSimpleGraph_adj_iff]

Goal state after:
case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → G.Adj ↑a✝ ↑b✝
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ (ofSimpleGraph G).Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)

Tactic:
rw [ofSimpleGraph_adj_iff]

Goal state after:
case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ G.Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: ⊢ ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

Tactic:
intro κ _
    by_cases h : Nonempty κ
    · refine ⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩
    · exact ⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩

Goal state after:
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
C : (Unit → Option α) → κ
⊢ ∀ (x : Option α), C (↑(diagonal (Option α) Unit) x) = C fun x ↦ none
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
hNM : N ≤r M
⊢ N = M ＼ (M.E \ N.E)

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
⊢ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
apply_fun (M.E \ Matroid.E ·) at h

Goal state after:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M.E \ (M ＼ (D₁ ∩ M.E)).E = M.E \ (M ＼ (D₂ ∩ M.E)).E
⊢ D₁ ∩ M.E = D₂ ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ = M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁)

Tactic:
rw [contract_delete_contract_delete']

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (∃ B, (M.IsBase (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.IsBase B ∧ J ⊆ B ∧ I ⊆ B

Tactic:
exact ⟨fun ⟨B, ⟨hBI, hdj⟩, hJB⟩ ↦ ⟨disjoint_of_subset_left hJB hdj, _, hBI,
    hJB.trans subset_union_left, subset_union_right⟩,
    fun ⟨hdj, B, hB, hJB, hIB⟩ ↦ ⟨B \ I,⟨by simpa [union_eq_self_of_subset_right hIB],
      disjoint_sdiff_left⟩, subset_sdiff.2 ⟨hJB, hdj⟩ ⟩⟩

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

Goal state before:
pp: case h.left
σ : 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
i : ι
hb0 : m.degree (b i) = 0
⊢ m.leadingCoeff (b i) • f = f * C (m.leadingCoeff (b i))

Tactic:
rw [mul_comm, smul_eq_C_mul]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := ⋯
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (Polynomial.map (eval x) Q).natDegree ≤ degreeOf none P

Tactic:
Polynomial.natDegree_le_iff_coeff_eq_zero

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ ∀ (N : ℕ), degreeOf none P < N → (Polynomial.map (eval x) Q).coeff N = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' D' : Set α
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')

Tactic:
by
  rw [contract_delete_contract', delete_delete]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')

Tactic:
by
  rw [contract_delete_contract_delete', sdiff_eq_left.mpr h]

Goal state after:
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
o : (Fin 2 → D) → D
in_omega : o ∈ ω
equ : f ![a, b] = f ![(fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0, (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1]
asymm : (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i ↦ o (swap ![![a, b], ![b, a]] i)) 1
⊢ (List.ofFn ![a, b]).Perm (List.ofFn ![b, a])

Tactic:
by simp [List.Perm.swap]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
h : p.comp q = nil
⊢ q.length = 0

Tactic:
have hlen : (p.comp q).length = 0 := by
    simpa using congrArg Path.length h
  have : p.length + q.length = 0 := by
    simpa [length_comp] using hlen
  exact Nat.eq_zero_of_add_eq_zero_left this

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜

Tactic:
by
  ext s
  refine mem_compression.trans ⟨?_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩
  rintro (h | h)
  · exact h.1
  · cases h.1 (mem_compression_of_insert_mem_compression h.2)

Goal state after: