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

Goal state before:
pp: case mp.inl.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, b, e} = {a, b, c}

pp: case mp.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, d, b} = {a, b, c}

pp: case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

pp: case mp.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, a, b} = {a, b, c_1}

pp: case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

pp: case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
any_goals
        first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
h : (Walk.cons h✝ p✝).IsPath
⊢ ⟨Walk.cons h✝ p✝, h⟩ = Path.nil

Tactic:
simp at h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
w : V
hw₁ : w ∈ p.support
hw₂ : w ∈ q.support
c : G.Walk w w
hc₁ : c.IsCycle
hc₂ : c.support.Sublist (p.support ++ q.support.reverse.tail)
⊢ ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.length ≤ p.length + q.length

Tactic:
use w, hw₁, hw₂, c, hc₁, by grind [hc₂.length_le]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ A.Nonempty

pp: case refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ x.Nonempty

pp: case refine_3
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ B.Nonempty

pp: case refine_4
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ y.Nonempty

Tactic:
exacts [⟨_, hx⟩, nonempty_of_mem_parts _ (hA hx), ⟨_, hy⟩, nonempty_of_mem_parts _ (hB hy)]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 = 2⁻¹

Tactic:
rw [mul_inv, inv_mul_cancel_right₀]; positivity

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ False

Tactic:
refine hG.not_ge (le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < card G ^ 2))

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 ≤ 1 * ↑(Fintype.card G) ^ 2
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₂ - x₂ + (y₁ - x₁) = y₁ - x₁ + (y₁ - x₁)

Tactic:
add_right_cancel_iff,

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₂ - x₂ = y₁ - x₁
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
t : Finset α
h : 0 < Eₘ[∅, t]
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
h : 0 < Eₘ[s, ∅]
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#(A / A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
← divConst_mul_card

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * ↑(#A) * (δₘ[A] * ↑(#A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
        ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))) ^
      2

Tactic:
card_product

Goal state after:
case refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
        ↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts)) ^
      2
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
⊢ ↑(#{a_1 | ↑x a_1 ≠ 0}) = 0

Tactic:
← Finset.sum_boole

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
⊢ (∑ x_1, if ↑x x_1 ≠ 0 then 1 else 0) = 0
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ map (fun x ↦ x + (k + 1)) n.bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices

Tactic:
simp [add_comm (a := 1)]

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

Goal state before:
pp: 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
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i

Tactic:
obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge

Goal state after:
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
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∃ L₀, L₀.SortedLT ∧ L = map (fun x ↦ x + a + 1) L₀

Tactic:
refine ⟨L.map (· - (a+1)), ?_, ?_⟩

Goal state after:
case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun x ↦ x - (a + 1)) L).SortedLT

case refine_2
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ L = map (fun x ↦ x + a + 1) (map (fun x ↦ x - (a + 1)) L)
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
⊢ ((fun x ↦ 2 ^ x) ∘ fun x ↦ x + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i)

Tactic:
ext x

Goal state after:
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
x : ℕ
⊢ ((fun x ↦ 2 ^ x) ∘ fun x ↦ x + a + 1) x = 2 ^ a * (2 * 2 ^ x)
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: 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 : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t

Tactic:
by
          rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (h𝒜 ht).2.1, h𝒜card]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
a : α
h : ∀ b ∈ {a}, b < a
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ 2 * ?m.31 - 1 ≤ #s.toEnumFinset

Tactic:
simpa using hs

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

Goal state before:
pp: n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ 2 * n - 1 ≤ #s.toEnumFinset

Tactic:
simpa using hs

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 - v 2 * w 1 = 0 ∧ v 2 * w 0 - v 0 * w 2 = 0 ∧ v 0 * w 1 - v 1 * w 0 = 0 ∧ True
⊢ False

Tactic:
and_true,

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 - v 2 * w 1 = 0 ∧ v 2 * w 0 - v 0 * w 2 = 0 ∧ v 0 * w 1 - v 1 * w 0 = 0
⊢ False
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n

Tactic:
simp [List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

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
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
⊢ a⁻¹ •> ↑A = ↑H

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
⊢ x ∈ a⁻¹ •> ↑A ↔ x ∈ ↑H
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements α) = numDerangements (card α)

Tactic:
rw [← card_derangements_invariant (card_fin _)]
  exact card_derangements_fin_eq_numDerangements

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
h : ↑(#(∅ * ∅)) < 3 / 2 * ↑(#∅)
⊢ False

Tactic:
simp at h

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
⊢ z ∈ A * A

Tactic:
have hr : r = z • A⁻¹ := by
    rw [inter_eq_right, ← this, mul_assoc _ A,
      ← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), subset_smul_finset_iff]
    simp only [← mul_assoc, smul_smul]
    refine smul_finset_subset_mul ?_
    simp [← hz, mul_mem_mul, ha, hb, hc]

Goal state after:
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⁻¹
⊢ z ∈ A * A
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) = (m.sum + a).choose a * m.bell

Tactic:
by
  let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)!
  have hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! := by
    unfold rest
    congr! 1 with j hj
    · grind [Multiset.toFinset_cons]
    · simp [Finset.mem_erase.mp hj]
  let c := (m.map (· !)).prod * (m.count a)! * rest
  have hm0 : m.bell * c = m.sum ! := by
    have hsplit : (m.count a)! * rest = ∏ j ∈ m.toFinset.erase 0, (m.count j)! := by
      by_cases hmem : a ∈ m.toFinset.erase 0
      · rw [← Finset.mul_prod_erase _ _ hmem]
      · have hcount : m.count a = 0 := by grind [Multiset.count_eq_zero_of_notMem]
        simp [rest, Finset.erase_eq_of_notMem hmem, hcount]
    simpa [c, hsplit, mul_assoc] using Multiset.bell_mul_eq m
  have hm : m.sum ! * a ! = m.bell * a ! * c := by grind
  have hc : 0 < a ! * c := Nat.mul_pos (by positivity) <|
    Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity)
  apply Nat.eq_of_mul_eq_mul_right hc
  calc
    _ = (m.sum + a)! := by
      have hq := Multiset.bell_mul_eq (a ::ₘ m)
      rw [← Finset.mul_prod_erase _ _ (a := a) (by simp [*]), ← hrest] at hq
      simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq
    _ = ((m.sum + a).choose a * m.bell) * (a ! * c) := by
      simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, hm]

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

Goal state before:
pp: case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)

Tactic:
rw [← mul_assoc, ← uniformBell_mul_eq _ hn]

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

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hx0 : x ≠ 0
hprod : g x = 0
⊢ x ∣ g x

Tactic:
simp [hprod]

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

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hx0 : x ≠ 0
i : ℕ
hprod : g x = x * (i + 1)
⊢ x ∣ g x

Tactic:
simp [hprod]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
i : ℕ
h : g i ≠ 0
⊢ i ≠ 0

Tactic:
contrapose hs0 with rfl
      exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 (by simpa using h)

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ (∑ x_1 > x, if x_1 ≤ x then f x else 0) = 0

Tactic:
exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
        parts_pos := ⋯, parts_sum := ⋯ }.toFinsuppAntidiag =
    g

Tactic:
ext x

Goal state after:
case refine_4
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
x : ℕ
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
          parts_pos := ⋯, parts_sum := ⋯ }.toFinsuppAntidiag
      x =
    g x
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s ∧ x ∉ p.parts
hx0 : x ≠ 0
hsum :
  constantCoeff (∑' (i : ℕ), f x (i + 1) • X ^ (x * (i + 1))) =
    ∑' (i : ℕ), constantCoeff (f x (i + 1) • X ^ (x * (i + 1)))
⊢ (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1

Tactic:
simp [toFinsuppAntidiag, hsum, hx.2, hx0]

Goal state after: