mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case hb
α : 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.biUnion id).Nonempty

Tactic:
biUnion_nonempty

Goal state after:
case hb
α : 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 ∈ B, (id x).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
he : e ∈ G.edgeSet
⊢ {b | b ∈ sᶜ ∧ b ∈ e}.Nonempty

Tactic:
by
  obtain ⟨v, w⟩ := e
  by_contra! c
  refine indA ?_ ?_ he.ne he
  · exact Set.not_notMem.mp <| not_and'.mp (c ▸ Set.notMem_empty v) <| Sym2.mem_mk_left ..
  · exact Set.not_notMem.mp <| not_and'.mp (c ▸ Set.notMem_empty w) <| Sym2.mem_mk_right ..

Goal state after:
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 α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ #({x ∈ s ×ˢ t ×ˢ u |
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) ≤
    #(G.cliqueFinset 3)

Tactic:
refine card_le_card_of_injOn (fun (x, y, z) ↦ {x, y, z}) ?_ ?_

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (x, y, z) => {x, y, z})
    ↑({x ∈ s ×ˢ t ×ˢ u |
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})
    ↑(G.cliqueFinset 3)

case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ Set.InjOn
    (fun x ↦
      match x with
      | (x, y, z) => {x, y, z})
    ↑({x ∈ s ×ˢ t ×ˢ u |
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
by
    by_cases a ∈ t <;> by_cases a ∈ u <;> simp [*]

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∑ x, (eval x) f = 0

Tactic:
calc
    ∑ x, eval x f = ∑ x : σ → K, ∑ d ∈ f.support, f.coeff d * ∏ i, x i ^ d i := by
      simp only [eval_eq']
    _ = ∑ d ∈ f.support, ∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i := sum_comm
    _ = 0 := sum_eq_zero ?_

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∀ x ∈ f.support, ∑ x_1, coeff x f * ∏ i, x_1 i ^ x i = 0
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = if x ∈ S then 1 else 0

Tactic:
split_ifs with hx

Goal state after:
case pos
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∈ S
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = 1

case neg
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∉ S
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = 0
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ p - 1 + (p - 1) < 2 * p - 1

Tactic:
by have := (Fact.out : p.Prime).two_le; lia

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

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0

Tactic:
have : NeZero p := inferInstance

Goal state after:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0
key : ∑ x, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })
⊢ ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }) = 0

Tactic:
← key

Goal state after:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0
key : ∑ x, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })
⊢ ∑ x, (eval x) F = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b ≤ a

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a

Tactic:
· exact ht _ ‹_›

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b < a

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a

Tactic:
· exact ht _ ‹_›

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a
Module: Mathlib.Combinatorics.Colex

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

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

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
p₁ p₂ : P
hp₁ : ∀ x ∈ s, p₁ ∈ x
hp₂ : ∀ x ∈ s, p₂ ∈ x
l₁ l₂ : L
hl₁ : l₁ ∈ s
hl₂ : l₂ ∈ s
hl₃ : l₁ ≠ l₂
⊢ p₁ = p₂

Tactic:
exact (eq_or_eq (hp₁ l₁ hl₁) (hp₂ l₁ hl₁) (hp₁ l₂ hl₂) (hp₂ l₂ hl₂)).resolve_right hl₃

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

Goal state before:
pp: case mp.some
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : some ((removeNone F) x) = some x
y : α
Fx : F (some x) = some y
⊢ x ∈ {a}

Tactic:
· exfalso
      rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
      exact F_derangement _ x_fixed

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg
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
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
let f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } := fun q =>
        ⟨mkLine (this q), (mkLine_ax (this q)).1⟩

Goal state after:
case neg
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
l₁ l₂ : L
hl : l₁ ≠ l₂
f✝ : L → P
left✝ : Function.Bijective f✝
hf2 : ∀ (l : L), pointCount P l = lineCount L (f✝ l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
f : { q // q ∈ l₂ } → { l // p ∈ l } := fun q ↦ ⟨mkLine ⋯, ⋯⟩
⊢ ∃ p ∈ l₁, p ∈ l₂
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
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
this :
  ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) + ↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) =
    ↑(#(A ∩ (c * d) •> A)) + ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ ↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) ≤ ↑(#A)

Tactic:
rw [Nat.cast_le, ← inter_union_distrib_left]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
this :
  ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) + ↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) =
    ↑(#(A ∩ (c * d) •> A)) + ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ #(A ∩ ((c * d) •> A ∪ (a * b)⁻¹ •> A)) ≤ #A
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
i j : Fin 2
⊢ (A * Bᵀ) i j = 0 i j

Tactic:
fin_cases i <;> fin_cases j <;> assumption

Goal state after:
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))!
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) = (m.sum + a).choose a * m.bell

Tactic:
let c := (m.map (· !)).prod * (m.count a)! * rest

Goal state after:
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
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) = (m.sum + a).choose a * m.bell
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
⊢ count D (List.take i (↑p).dropLast.tail) ≤ count U (List.take i (↑p).dropLast.tail)

Tactic:
have l3 : p.toList.length - 1 = p.toList.length - 1 - 1 + 1 := by
      rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
      · tauto
      · rename_i bal _
        cases s <;> simp at bal
      · tauto

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.take i (↑p).dropLast.tail) ≤ count U (List.take i (↑p).dropLast.tail)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case inr.intro.calc_1
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
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
this : 0 < #A
ineq : ↑(#S) ≤ (2 - K) * K * ↑l + (K - 1) * K * ↑(#S)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑l

Tactic:
calc
          (φ - K) * (K - ψ) / ((2 - K) * K) * #S
      _ = (φ - K) * (K - ψ) * #S / ((2 - K) * K) := div_mul_eq_mul_div ..
      _ ≤ (2 - K) * K * l / ((2 - K) * K) := by
        have := Real.goldenRatio_mul_goldenConj
        have := Real.goldenRatio_add_goldenConj
        rw [show (φ - K) * (K - ψ) = 1 - (K - 1) * K by grind]
        gcongr ?_ / _
        linarith [ineq]
      _ = l := by field

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

Goal state before:
pp: 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
⊢ ∏ a ∈ (Multiset.toFinsupp p.parts).support, f a ((Multiset.toFinsupp p.parts) a) =
    ∏ i ∈ s, (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))

Tactic:
Multiset.toFinsupp_support,

Goal state after:
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
⊢ ∏ a ∈ p.parts.toFinset, f a ((Multiset.toFinsupp p.parts) a) =
    ∏ i ∈ s, (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
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
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ (1 + 1) * x ^ k * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))

Tactic:
one_add_one_eq_two,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
k : ℕ
| x ^ 2 * x ^ k * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Summable fun n ↦ X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))

pp: case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Multipliable fun n ↦ 1 - X ^ (n + k + 1)

pp: case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)

Tactic:
· exact Pentagonal.summable_pow_mul_prod_one_sub_pow R

Goal state after:
case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Multipliable fun n ↦ 1 - X ^ (n + k + 1)

case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)

Tactic:
· rw [tendsto_iff_coeff_tendsto]
    refine fun n ↦ tendsto_atTop_of_eventually_const fun k (hk : k ≥ n) ↦ ?_
    rw [map_zero]
    apply coeff_of_lt_order
    grw [← le_order_mul, ← le_order_mul]
    refine (lt_add_of_lt_of_nonneg (lt_add_of_nonneg_of_lt (by simp) ?_) (by simp))
    rw [order_X_pow, Nat.cast_lt, ← Nat.add_one_le_iff, Nat.le_div_iff_mul_le (by simp)]
    apply Nat.mul_le_mul <;> linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)

Tactic:
rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α⦄, G.IsLink e x y → G.IsLink e v w → x = v ∨ x = w

Tactic:
exact G.eq_or_eq_of_isLink_of_isLink

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e : β
x y : α'
f : α → α'
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α'⦄, Relation.Map (G.IsLink e) f f x y → x ∈ f '' V(G)

Tactic:
rintro e - - ⟨x, y, h, rfl, rfl⟩

Goal state after:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
h : G.IsLink e x y
⊢ f x ∈ f '' V(G)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
hef : e ≠ f
⊢ False

Tactic:
simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i

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

Goal state before:
pp: case inl
α : Type u_1
H : Hypergraph α
empty : V(H) = ∅ ∧ E(H) = ∅
⊢ H = ⊥ ∨ H.IsNonempty

Tactic:
(
    left
    apply Hypergraph.ext empty.1 empty.2
  )

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M ＼ D).Indep X ∧ X ⊆ (M ＼ D).E ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D

Tactic:
delete_indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ (M ＼ D).E ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).Indep {e} ↔ M.IsNonloop e ∧ e ∉ D

Tactic:
delete_indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ M.Indep {e} ∧ Disjoint {e} D ↔ M.IsNonloop e ∧ e ∉ D