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

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : False ↔ (completeGraph (Fin n)).Adj x y
⊢ completeGraph (Fin n) ⊑ G

Tactic:
top_adj,

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : False ↔ x ≠ y
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp ≠ q.takeUntil w hwq
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
have := ih _ (hs ▸ length_takeUntil_lt_length hwp hwv) (hp.takeUntil hwp) (hq.takeUntil hwq)
      grind [isSubwalk_takeUntil, IsSubwalk.trans]

Goal state after:
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:
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.Data.Finset.CastCard

Goal state before:
pp: α : Type u_1
R : Type u_2
s : Finset α
a : α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
hs : a ∈ s
⊢ ↑(#(s.erase a)) = ↑(#(s.erase a) + 1) - 1

Tactic:
cast_add,

Goal state after:
α : Type u_1
R : Type u_2
s : Finset α
a : α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
hs : a ∈ s
⊢ ↑(#(s.erase a)) = ↑(#(s.erase a)) + ↑1 - 1
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
by_contra! +distrib rfl | rfl

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

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
h : 0 < Eₘ[s, ∅]
⊢ False
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:
have := (Fact.out : p.Prime).two_le; lia

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R

Tactic:
apply LinearMap.mk₂ R fun a b : Fin 3 → R =>
      ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]
  · intros
    simp_rw [vec3_add, Pi.add_apply]
    apply vec3_eq <;> ring
  · intros
    simp_rw [smul_vec3, Pi.smul_apply, smul_sub, smul_mul_assoc]
  · intros
    simp_rw [vec3_add, Pi.add_apply]
    apply vec3_eq <;> ring
  · intros
    simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ toColex {a} < toColex {b} ↔ a < b

Tactic:
by
  simp [toColex_lt_singleton]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ ∃ a ∈ ofColex (toColex t), a ∉ ofColex (toColex s) ∧ ∀ b ∈ ofColex (toColex s), b ∉ ofColex (toColex t) → b < a

Tactic:
refine ⟨w, hwt, hws, fun a has hat ↦ ?_⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
⊢ a < w
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (↑x✝⁵ ⬝ᵥ ↑x✝⁴ = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)

Tactic:
← h1,

Goal state after:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (w✝¹ • ↑x✝³ ⬝ᵥ ↑x✝⁴ = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ t ∈ initSeg (𝒜.sup' h𝒜₀ ⇑toColex)

Tactic:
rw [mem_initSeg]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ #(𝒜.sup' h𝒜₀ ⇑toColex) = #t ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ ⇑toColex) = #t
le : toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
p : toColex t < toColex (𝒜.sup' h𝒜₀ ⇑toColex)
⊢ t ∈ 𝒜

Tactic:
· exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct ((crossProduct u) v)) w = (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u

Tactic:
by
  simp_rw [cross_apply, vec3_dotProduct]
  ext i
  fin_cases i <;>
  · simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∈ fixedPoints ⇑↑f } ≃ { f // fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f }

Tactic:
exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∈ fixedPoints ·)

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) < 2 * #A
z : G
⊢ z ∈ A⁻¹ * A → z ∈ A * A⁻¹

Tactic:
simp only [mem_mul, forall_exists_index, and_imp, mem_inv,
    exists_exists_and_eq_and]

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

Goal state before:
pp: case intro.intro
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
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
⊢ lineCount L p = lineCount L q

Tactic:
have hl₃ : pointCount P l₃ = n := (HasLines.lineCount_eq_pointCount h h₃₃).symm.trans hp₃

Goal state after:
case intro.intro
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
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
⊢ lineCount L p = lineCount L q
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
Ne,

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ ∃ a b c, ¬a = b ∧ ¬a = c ∧ ¬b = c
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ Fintype.card P = order P L ^ 2 + order P L + 1

Tactic:
← h1,

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ Fintype.card { q // q ≠ p } + 1 = order P L ^ 2 + order P L + 1
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)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * A
⊢ 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))

Tactic:
convert! lt_card_mul_inv_eq (by simpa using Rat.cast_strictMono (K := ℝ) h) ha

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * A
⊢ 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) ↔
    (2 - 3 / 2) * ↑(#A) < ↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a}))
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).1 < n.succ

Tactic:
simp_wf

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).1 < n + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n.succ

Tactic:
simp_wf

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n + 1
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
⊢ #r = #A

Tactic:
rw [hr, card_smul_finset, card_inv]

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

Goal state before:
pp: case e_a.a.hx
m : Multiset ℕ
x : ℕ
hx : ¬x = 0 ∧ x ∈ m
⊢ x ≠ 0

Tactic:
simp only [ne_eq, hx.1, not_false_eq_true]

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

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

pp: case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U])

Tactic:
· simp [hi]

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

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

Tactic:
have l1 : p.toList.take 1 = [p.toList.head h] := by rcases p with - | - <;> tauto

Goal state after:
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)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m n : ℕ
⊢ m.uniformBell n = ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
unfold uniformBell bell
  rw [toFinset_replicate]
  split_ifs with hm
  · simp [hm]
  · by_cases hn : n = 0
    · simp [hn]
    · rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
      simp [count_replicate]

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ 0 < p.firstReturn

Tactic:
by
  rw [← not_le, Nat.le_zero, firstReturn, findIdx_eq, getElem_range]
  · rw! [← p.cons_tail_dropLast_concat h]
    simp
  · rw [length_range, length_pos_iff]
    exact toList_ne_nil.mpr h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
hi : i ≠ 0
⊢ Summable fun j ↦ f i (j + 1) • X ^ (i * (j + 1))

Tactic:
obtain ⟨a, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hi

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : TopologicalSpace R
f : ℕ → ℕ → R
a : ℕ
hi : a + 1 ≠ 0
⊢ Summable fun j ↦ f (a + 1) (j + 1) • X ^ ((a + 1) * (j + 1))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.outsidePart = 0

Tactic:
simp_rw [outsidePart, nest_ne_zero, dite_false, firstReturn_nest]

Goal state after:
p : DyckWord
⊢ p.nest.drop ((↑p).length + 1 + 1) ⋯ = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case pos
p : DyckWord
h : p = 0
⊢ p.toTree.numNodes = p.semilength

pp: case neg
p : DyckWord
h : ¬p = 0
⊢ p.toTree.numNodes = p.semilength

Tactic:
· simp [h, toTree]

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.toTree.numNodes = p.semilength
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
| fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else (∑' (j : ℕ), (X ^ (b + 1)) ^ j) * (1 - X ^ (b + 1))

Tactic:
ext b
    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)]

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
b : ℕ
| if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 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
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ HasSum (fun b ↦ powMulProdOneSubPow k b x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) b x) (0 - aux k 0 x)

Tactic:
((hsum _).add ((hsum _).mul_left _)).hasSum_iff_tendsto_nat

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto
    (fun n ↦ ∑ i ∈ Finset.range n, (powMulProdOneSubPow k i x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) i x))
    atTop (𝓝 (0 - aux k 0 x))
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.IsLoopAt e x ↔ G.IsLoopAt e x

Tactic:
unfold Graph.IsLoopAt
  rw [hHG.isLink_iff he]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsNonloopAt G.IsNonloopAt E(H)

Tactic:
rintro e he
  ext x
  exact hHG.isNonloopAt_congr he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ noEdge ∅ β ≤ G

Tactic:
by constructor <;> simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁

Tactic:
rw [delete_delete, union_comm, delete_delete]

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥sᶜ)
⊢ ↑n < Fintype.card X - #s

Tactic:
by simpa using n.2

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis' I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
⊢ (M ／ C).IsBasis (I \ C) ((X ∩ M.E) \ C)

Tactic:
exact h.isBasis_inter_ground.contract_isBasis_of_isBasis' hJC h_ind

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X \ I ⊆ (M ／ I).loops

Tactic:
sdiff_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ I ∪ (M ／ I).loops
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
e : α
heK : e ∈ K
heC : e ∉ C
⊢ K \ {e} ∪ C ⊆ K \ {e}

Tactic:
by
    simp [subset_sdiff_singleton hC.subset heC]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case hcard
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 < #(S none)

Tactic:
apply lt_of_le_of_lt _ (Hdeg none)

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) := ⋯
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (Polynomial.map (eval x) Q).natDegree ≤ degreeOf none P
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
⊢ (o fun j ↦ ![![a, b], ![b, a]] j 0) = o fun j ↦ ![![a, b], ![b, a]] j 1

Tactic:
convert! symmega ![a, b] ![b, a] (by simp [List.Perm.swap]) o in_omega using 2 <;>
    simp [Matrix.const_fin1_eq]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
R : Type u_2
inst✝ : Monoid R
w : V → V → R
a b c : V
p : Path a b
q : Path b c
⊢ weightOfEPs w (p.comp q) = weightOfEPs w p * weightOfEPs w q

Tactic:
by
  simp [weightOfEPs, weight_comp]

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

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ (p'.cons e).length
⊢ ∃ v p₁ p₂, p'.cons e = p₁.comp p₂ ∧ p₁.length = n

Tactic:
| @cons _ c p' e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : h i = 0
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

pp: case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
· simp [hi]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0