mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
hi' : i = p₁.length
⊢ p₂.support[i + k] = p₁.support[i]

Tactic:
have := h <| i - 1

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
hi' : i = p₁.length
this : ∀ (h : i - 1 < p₁.darts.length), p₂.darts[i - 1 + k]? = some p₁.darts[i - 1]
⊢ p₂.support[i + k] = p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCircuit
⊢ 3 ≤ p.length

Tactic:
match p with
  | .cons hadj .nil => simp at hadj
  | .cons _ <| .cons _ .nil => simpa using hp.isTrail
  | .cons _ <| .cons _ <| .cons _ _ => grind [length_cons]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
⊢ (p.take n).IsPath

Tactic:
suffices ((p.take (p.length - 1)).take n).IsPath by
    rwa [take_take, isPath_copy, show min (p.length - 1) n = n by omega] at this

Goal state after:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
⊢ ((p.take (p.length - 1)).take n).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
hm0 : ¬m = 0
⊢ n = m

pp: case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m

pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m

Tactic:
· simp only [hn0, getVert_zero, Walk.getVert_cons p h hm0] at hnm
      have hvp : v ∉ p.support := by aesop
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(m - 1), ⟨hnm.symm, by lia⟩⟩)).elim

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m

case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsClique ↑s ∧ #s = n → H.IsClique ↑s ∧ #s = n

Tactic:
exact And.imp_left (IsClique.mono h)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ ¬G.CliqueFree n ↔ Nonempty ((completeGraph (Fin n)).Copy G)

Tactic:
exact not_cliqueFree_iff_top_isContained n

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

Goal state before:
pp: case neg
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
h : ¬Infinite ι
this : Fintype ι
hc : n ≤ Fintype.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
exact not_cliqueFree_of_le_card V f hc

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Set α
t' : Finset ↑s
tc : (induce s G).IsNClique (induce s G).cliqueNum t'
⊢ (induce s G).cliqueNum ≤ G.cliqueNum

Tactic:
isNClique_induce_iff

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Set α
t' : Finset ↑s
tc : G.IsNClique (induce s G).cliqueNum (map (Embedding.subtype fun x ↦ x ∈ s) t')
⊢ (induce s G).cliqueNum ≤ G.cliqueNum
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Set α
⊢ (induce s G).cliqueNum ≤ G.cliqueNum

Tactic:
have ⟨t', tc⟩ := (G.induce s).exists_isNClique_cliqueNum
  rw [isNClique_induce_iff] at tc
  exact tc.card_eq ▸ tc.isClique.card_le_cliqueNum

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
⊢ G.IsIndepSet (G.neighborSet v)

Tactic:
by_contra nind

Goal state after:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ¬G.IsIndepSet (G.neighborSet v)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).IsPath
⊢ p.IsPath

Tactic:
by
  rw [isPath_def]
  rw [isPath_def, support_map] at hp
  exact hp.of_map

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ 0 < triangleRemovalBound ε

Tactic:
by
  have : 0 < 1 - min 1 ε / 4 := by have := min_le_left 1 ε; linarith
  unfold triangleRemovalBound
  positivity

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

Goal state before:
pp: case hab.refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ ↑(G.edgeDensity U V) - ε ^ 5 / 50 ≤
    ↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) - ε ^ 5 / 50

Tactic:
rw [biUnion_parts, biUnion_parts]

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 : cornersTheoremBound ε ≤ Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ¬IsCornerFree ↑A

Tactic:
rintro hA
  rw [cornersTheoremBound, Nat.add_one_le_iff] at hG
  have hε₁ : ε ≤ 1 := by
    have := hAε.trans (Nat.cast_le.2 A.card_le_univ)
    simp only [sq, Nat.cast_mul, Fintype.card_prod] at this
    rwa [mul_le_iff_le_one_left] at this
    positivity
  have := noAccidental hA
  rw [Nat.floor_lt' (by positivity), inv_lt_iff_one_lt_mul₀' (by positivity)] at hG
  refine hG.not_ge (le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < card G ^ 2))
  classical
  have h₁ := (farFromTriangleFree_graph hAε).le_card_cliqueFinset
  rw [card_triangles, card_triangleIndices] at h₁
  convert! h₁.trans (Nat.cast_le.2 <| card_le_univ _) using 1 <;> simp <;> ring

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ Eₘ[s, t] = Eₘ[t, s]

Tactic:
by
  rw [mulEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]
  simp [mulEnergy, mul_comm, map_eq_image]

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

Goal state before:
pp: case h₂
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ 1 ≤ n

Tactic:
unfold cornersTheoremBound at hG

Goal state after:
case h₂
n : ℕ
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 3 / 9) * 27)⁻¹⌋₊ + 1 ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ 1 ≤ n
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))
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }

Tactic:
have hF : ∀ x, eval x F = if x ∈ S then 1 else 0 := by
    intro x
    calc
      eval x F = ∏ i ∈ s, eval x (1 - f i ^ (q - 1)) := eval_prod s _ x
      _ = if x ∈ S then 1 else 0 := ?_
    simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]
    split_ifs with hx
    · apply Finset.prod_eq_one
      intro i hi
      rw [hS] at hx
      rw [hx i hi, zero_pow hq.ne', sub_zero]
    · obtain ⟨i, hi, hx⟩ : ∃ i ∈ s, eval x (f i) ≠ 0 := by
        simpa [hS, not_forall, Classical.not_imp] using hx
      apply Finset.prod_eq_zero hi
      rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]

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
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H1
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m₁ m₂ n : Fin 3 → R),
    ![(m₁ + m₂) 1 * n 2 - (m₁ + m₂) 2 * n 1, (m₁ + m₂) 2 * n 0 - (m₁ + m₂) 0 * n 2,
        (m₁ + m₂) 0 * n 1 - (m₁ + m₂) 1 * n 0] =
      ![m₁ 1 * n 2 - m₁ 2 * n 1, m₁ 2 * n 0 - m₁ 0 * n 2, m₁ 0 * n 1 - m₁ 1 * n 0] +
        ![m₂ 1 * n 2 - m₂ 2 * n 1, m₂ 2 * n 0 - m₂ 0 * n 2, m₂ 0 * n 1 - m₂ 1 * n 0]

Tactic:
intros

Goal state after:
case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ + m₂✝) 1 * n✝ 2 - (m₁✝ + m₂✝) 2 * n✝ 1, (m₁✝ + m₂✝) 2 * n✝ 0 - (m₁✝ + m₂✝) 0 * n✝ 2,
      (m₁✝ + m₂✝) 0 * n✝ 1 - (m₁✝ + m₂✝) 1 * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1, m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2, m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0] +
      ![m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1, m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2, m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H2
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
intros

Goal state after:
case H2
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![(c✝ • m✝) 1 * n✝ 2 - (c✝ • m✝) 2 * n✝ 1, (c✝ • m✝) 2 * n✝ 0 - (c✝ • m✝) 0 * n✝ 2,
      (c✝ • m✝) 0 * n✝ 1 - (c✝ • m✝) 1 * n✝ 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m n₁ n₂ : Fin 3 → R),
    ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
        m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
      ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
        ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]

Tactic:
intros

Goal state after:
case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ + n₂✝) 2 - m✝ 2 * (n₁✝ + n₂✝) 1, m✝ 2 * (n₁✝ + n₂✝) 0 - m✝ 0 * (n₁✝ + n₂✝) 2,
      m✝ 0 * (n₁✝ + n₂✝) 1 - m✝ 1 * (n₁✝ + n₂✝) 0] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1, m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2, m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0] +
      ![m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1, m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2, m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
intros

Goal state after:
case H4
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![m✝ 1 * (c✝ • n✝) 2 - m✝ 2 * (c✝ • n✝) 1, m✝ 2 * (c✝ • n✝) 0 - m✝ 0 * (c✝ • n✝) 2,
      m✝ 0 * (c✝ • n✝) 1 - m✝ 1 * (c✝ • n✝) 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]
Module: Mathlib.Combinatorics.Derangements.Basic

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

Tactic:
apply_fun some at x_fixed

Goal state after:
case mp
α : 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
⊢ x ∈ {a}
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
⊢ a •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A

Tactic:
by
  have smul_A {a} (ha : a ∈ A) : a •> A = A * A :=
    eq_of_subset_of_card_le (smul_finset_subset_mul ha) (by simpa)
  have A_smul {a} (ha : a ∈ A) : A <• a = A * A :=
    eq_of_subset_of_card_le (op_smul_finset_subset_mul ha) (by simpa)
  have smul_A_eq_A_smul {a} (ha : a ∈ A) : a •> A = A <• a := by rw [smul_A ha, A_smul ha]
  have mul_mem_A_comm {x a} (ha : a ∈ A) : x * a ∈ A ↔ a * x ∈ A := by
    rw [← smul_mem_smul_finset_iff a, smul_A_eq_A_smul ha, ← op_smul_eq_mul, smul_comm,
      smul_mem_smul_finset_iff, smul_eq_mul]
  let H := stabilizer G A
  have inv_smul_A {a} (ha : a ∈ A) : a⁻¹ • (A : Set G) = H := by
    ext x
    rw [Set.mem_inv_smul_set_iff, smul_eq_mul]
    refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
    · simpa [← smul_A ha, mul_smul] using! smul_A hx
    · norm_cast
      rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]
  refine ⟨?_, ?_⟩
  · rw [← inv_smul_A ha, smul_inv_smul]
  · rw [← inv_smul_A ha, smul_comm]
    norm_cast
    rw [← smul_A_eq_A_smul ha, inv_smul_smul]

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

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)

Tactic:
rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']
    · apply sum_congr rfl
      rintro ⟨i, j⟩ H
      rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]
    · simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]
      aesop

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

Goal state before:
pp: p q r : DyckWord
h : ↑((fun x ↦ x + p) q) = ↑((fun x ↦ x + p) r)
⊢ ↑q = ↑r

Tactic:
exact append_cancel_right h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ ↑H <• x = (fun m ↦ m •> ↑H) { unop' := a }

Tactic:
change _ = _ <• _

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ ↑H <• x = ↑H <• a
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.semilength = p.semilength + 1

Tactic:
by simp [semilength, nest]

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

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

Tactic:
· rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
      simp only [Finset.prod_singleton, count_replicate_self]

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

Goal state before:
pp: case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) ↑p) = count D (List.take (j + 1) ↑p)) = false

Tactic:
simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (C (f (i + 1) (m + 1))).order + (X ^ ((i + 1) * (m + 1))).order

Tactic:
refine lt_add_of_nonneg_of_lt (by simp) ?_

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (X ^ ((i + 1) * (m + 1))).order
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p✝ q✝ : DyckWord
h : p✝ ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
h₁ : ↑p <:+: ↑q
⊢ p = q

Tactic:
have h₂ := infix_of_le qp

Goal state after:
p✝ q✝ : DyckWord
h : p✝ ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
h₁ : ↑p <:+: ↑q
h₂ : ↑q <:+: ↑p
⊢ p = q
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
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
⊢ Multiset.count i p.parts * i ≠ i * (b + 1)

Tactic:
rw [mul_comm i, (mul_left_inj' (Nat.ne_zero_of_lt (p.parts_pos hi))).ne]

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
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
⊢ Multiset.count i p.parts ≠ b + 1
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
⊢ HasProd (fun i ↦ 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) (genFun f)

Tactic:
HasProd,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
⊢ Filter.Tendsto (fun s ↦ ∏ b ∈ s, (1 + ∑' (j : ℕ), f (b + 1) (j + 1) • X ^ ((b + 1) * (j + 1))))
    (SummationFilter.unconditional ℕ).filter (nhds (genFun f))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
x : α × α × α
⊢ x ∈ triangleIndices s ↔ ∃ y, ∃ a ∈ s, (y, y + a, y + 2 * a) = x

Tactic:
simp [triangleIndices]

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
⊢ #(triangleIndices s) = Fintype.card α * #s

Tactic:
simp [triangleIndices]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h : HasProd (fun n ↦ 1 - X ^ (n + 1)) (pentagonalSeries R)
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)

Tactic:
HasProd,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h : Tendsto (fun s ↦ ∏ b ∈ s, (1 - X ^ (b + 1))) (SummationFilter.unconditional ℕ).filter (𝓝 (pentagonalSeries R))
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasProd (fun n ↦ 1 - X ^ (n + 1)) (pentagonalSeries R)

Tactic:
HasProd,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ Tendsto (fun s ↦ ∏ b ∈ s, (1 - X ^ (b + 1))) (SummationFilter.unconditional ℕ).filter (𝓝 (pentagonalSeries R))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ (fun n ↦ ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n ↦
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

pp: ⊢ (fun n ↦ (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) =O[atTop] fun n ↦
    ↑(ruzsaSzemerediNumberNat n)

Tactic:
· simp_rw [sq]
    refine (IsBigO.mul ?_ ?_).mul ?_
    · trans fun n ↦ n / 3
      · simp_rw [div_eq_inv_mul]
        exact (isBigO_refl ..).const_mul_right (by simp)
      refine IsLittleO.right_isBigO_sub ?_
      simpa [div_eq_inv_mul, Function.comp_def] using
        .atTop_of_const_mul₀ zero_lt_three (by simp [tendsto_natCast_atTop_atTop])
    · rw [IsBigO_def]
      refine ⟨12, ?_⟩
      simp only [IsBigOWith, norm_natCast, eventually_atTop]
      exact ⟨15, fun x hx ↦ by norm_cast; lia⟩
    · rw [isBigO_exp_comp_exp_comp]
      refine ⟨0, ?_⟩
      simp only [neg_mul, eventually_map, Pi.sub_apply, sub_neg_eq_add, neg_add_le_iff_le_add,
        add_zero, eventually_atTop]
      refine ⟨9, fun x hx ↦ ?_⟩
      gcongr
      · simp
        lia
      · lia

Goal state after:
⊢ (fun n ↦ (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) =O[atTop] fun n ↦
    ↑(ruzsaSzemerediNumberNat n)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
h : H.IsNonloopAt e x
⊢ G.IsNonloopAt e x

Tactic:
obtain ⟨y, hxy, he⟩ := h

Goal state after:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
y : α
hxy : y ≠ x
he : H.IsLink e x y
⊢ G.IsNonloopAt e x
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
⊢ G₁.IsLink e = G₂.IsLink f

Tactic:
ext x y
    rw [isLink_iff_inc, isLink_iff_inc, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
⊢ Disjoint G H ↔ Disjoint V(G) V(H)

Tactic:
disjoint_iff,

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
⊢ G ⊓ H = ⊥ ↔ Disjoint V(G) V(H)