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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
refine (lt_iff_exists_forall_lt.2 ⟨a, mem_erase.2 ⟨hma.ne', (hw hwa).1 ha⟩,
      notMem_erase _ _, fun b hbs hbt ↦ ?_⟩).le

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ ofColex { val := t.val.erase m, nodup := ⋯ }
⊢ b < a
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mk
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map LinearMap.id ⋯ (Quot.mk (⇑(projectivizationSetoid K V)) v) = id (Quot.mk (⇑(projectivizationSetoid K V)) v)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mk
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : DivisionRing F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
g : W →ₛₗ[τ] U
hg : Function.Injective ⇑g
hgf : Function.Injective ⇑(g ∘ₛₗ f)
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map (g ∘ₛₗ f) hgf (Quot.mk (⇑(projectivizationSetoid K V)) v) =
    (map g hg ∘ map f hf) (Quot.mk (⇑(projectivizationSetoid K V)) v)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
⊢ D' = mk K D.rep ⋯

Tactic:
← mk_rep D',

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
⊢ mk K D'.rep ⋯ = mk K D.rep ⋯
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w = 0
⊢ Quotient.mk'' (if h : True then ⟨v, hv⟩ else ⟨0, ⋯⟩) = mk F v hv

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : ¬(crossProduct v) w = 0
⊢ Quotient.mk'' (if h : False then ⟨v, hv⟩ else ⟨(crossProduct v) w, ⋯⟩) = mk F ((crossProduct v) w) h

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
⊢ ∃ s, #s = r ∧ 𝒜 = initSeg s

Tactic:
have hs := sup'_mem (ofColex ⁻¹' 𝒜) (LinearOrder.supClosed _) 𝒜 h𝒜₀ toColex
    (fun a ha ↦ by simpa using ha)

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
⊢ ∃ s, #s = r ∧ 𝒜 = initSeg s
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case inl
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v.cross v

Tactic:
rfl

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 : Perm α
⊢ a ∈ fixedPoints ⇑f ∧ fixedPoints ⇑f ⊆ {a} ↔ a ∈ fixedPoints ⇑f ∧ ∀ x ∈ fixedPoints ⇑f, x = a

Tactic:
rfl

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
⊢ a •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A

Tactic:
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]

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)
⊢ a •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case zero
⊢ ↑(numDerangements (0 + 1)) = (↑0 + 1) * ↑(numDerangements 0) - (-1) ^ 0

Tactic:
rfl

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

Goal state before:
pp: case ind.zero
hyp : ∀ m < 0, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin 0)) = numDerangements 0

Tactic:
rfl

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

Goal state before:
pp: case ind.succ.zero
hyp : ∀ m < 0 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (0 + 1))) = numDerangements (0 + 1)

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ ↑(numDerangements 0) = ∑ k ∈ Finset.range (0 + 1), (-1) ^ k * ↑((k + 1).ascFactorial (0 - k))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ∀ (a : ↑(Equiv.RemoveNone.fiber none)), False
⊢ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}} ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}

Tactic:
rfl

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

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(numDerangements n) / ↑n.factorial = s (n + 1)

Tactic:
← Int.cast_natCast,

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑↑(numDerangements n) / ↑n.factorial = s (n + 1)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ i ∈ s, pointCount P i.2

Tactic:
rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]

Goal state after:
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset
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
⊢ (order P L + 1) * order P L + 1 = order P L ^ 2 + order P L + 1

Tactic:
Nat.succ_mul,

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
⊢ order P L * order P L + order P L + 1 = order P L ^ 2 + order P L + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]
      aesop

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

Goal state before:
pp: p : DyckWord
⊢ ↑(0 + p) = ↑p

Tactic:
rfl

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

Goal state before:
pp: p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0

Tactic:
rfl

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = [U] ++ (↑p).dropLast.tail ++ [D]

Tactic:
rfl

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))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
⊢ m.sum ! * a ! = m.bell * a ! * c

Tactic:
grind

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

Goal state before:
pp: p : DyckWord
⊢ ([U] ++ ↑p).tail = ↑p

Tactic:
rfl

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

Goal state before:
pp: p : DyckWord
⊢ p.semilength = count U ↑p

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
⊢ a ≠ 0

Tactic:
grind

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

Goal state before:
pp: n : ℕ
x : (p : (n + 1).Partition) × ↥p.parts.toFinset
⊢ ↑x.snd - 1 < n.succ

Tactic:
grind

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

Goal state before:
pp: n : ℕ
x : (p : (n + 1).Partition) × ↥p.parts.toFinset
⊢ ↑⟨↑x.snd - 1, ⋯⟩ + 1 ∈ x.fst.parts

Tactic:
grind

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

Goal state before:
pp: n : ℕ
x : (p : (n + 1).Partition) × ↥p.parts.toFinset
⊢ (fun x ↦ ⟨↑x.snd, ⟨↑x.fst + 1, ⋯⟩⟩) ((fun x ↦ ⟨⟨↑x.snd - 1, ⋯⟩, ⟨x.fst, ⋯⟩⟩) x) = x

Tactic:
grind

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
a✝ : Nontrivial R
⊢ n < (i + 1) * (m + 1)

Tactic:
grind

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 : ℕ
⊢ Summable fun j ↦ f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))

Tactic:
apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
⊢ Filter.Tendsto (fun i_1 ↦ (f (i + 1) (i_1 + 1) • X ^ ((i + 1) * (i_1 + 1))).order) Filter.atTop (nhds ⊤)
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
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 : ℕ
⊢ i ≠ 0 ∧ i ≤ g i → g i ≠ 0

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝² : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
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)
this✝ : φ * ψ = -1
this : φ + ψ = 1
⊢ (φ - K) * (K - ψ) = 1 - (K - 1) * K

Tactic:
grind

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

Goal state before:
pp: case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
⊢ ↑p <:+: ↑r

Tactic:
grind

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

Goal state before:
pp: case 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
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
i : ℕ
h : g i ≠ 0
⊢ i ≤ g i

Tactic:
· exact Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg hprod _

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

Goal state before:
pp: case a
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≤ x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) (toDual x) (toDual x✝) = (mu 𝕜) x x✝

Tactic:
rfl

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

Goal state before:
pp: case refl
p q : DyckWord
⊢ p.semilength ≤ p.semilength

Tactic:
rfl

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
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
this : ∀ (i : ℕ), g i ≠ 0 → i ≠ 0
⊢ ∀ {i : ℕ}, i ∈ Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ } → 0 < i

Tactic:
simpa [Nat.pos_iff_ne_zero]

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

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

Tactic:
simp [h, toTree, ofTree]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ ∑' (j : ℕ), X ^ ((i + 1) * j) = 1 + ∑' (j : ℕ), 1 • X ^ ((i + 1) * (j + 1))

Tactic:
rw [tsum_eq_zero_add' ?_]

Goal state after:
case pos
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ X ^ ((i + 1) * 0) + ∑' (b : ℕ), X ^ ((i + 1) * (b + 1)) = 1 + ∑' (j : ℕ), 1 • X ^ ((i + 1) * (j + 1))

R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ Summable fun n ↦ X ^ ((i + 1) * (n + 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: k : ℤ
⊢ pentagonal k = (k * (3 * k - 1) / 2).toNat

Tactic:
rfl

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

Goal state before:
pp: k : ℤ
⊢ Even (k * (3 * k - 1))

Tactic:
grind

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

Goal state before:
pp: case inl
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
h✝ : 3 * (x + y) - 1 = 0
⊢ x = y

Tactic:
grind

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

Goal state before:
pp: case inr
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
h✝ : x - y = 0
⊢ x = y

Tactic:
grind

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

Goal state before:
pp: case h
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
⊢ p.parts.toFinset ⊆ s

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
⊢ b + 1 < m

Tactic:
grind

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
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
⊢ Multiset.count i p.parts ≠ b + 1

Tactic:
grind

Goal state after:
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
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
⊢ j ≠ 0

Tactic:
grind

Goal state after:
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
i : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
⊢ (↑i + 1) * m - 1 + 1 = (↑i + 1) * m

Tactic:
grind

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 ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 ∈ range d

Tactic:
grind

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 + 1 = i

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
⊢ ¬IsFragment K S ∅

Tactic:
simp [IsFragment, (connectivity_pos hK hS).ne]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ n < (k + 1) * m

Tactic:
grind

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

Goal state before:
pp: n l : ℕ
hk : l + succ 0 ≠ 0
⊢ (n + 1).stirlingFirst (l + succ 0) = n * n.stirlingFirst (l + succ 0) + n.stirlingFirst (l + succ 0 - 1)

Tactic:
rfl

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

Goal state before:
pp: k l : ℕ
hn : l + succ 0 ≠ 0
⊢ (l + succ 0).stirlingFirst (k + 1) =
    (l + succ 0 - 1) * (l + succ 0 - 1).stirlingFirst (k + 1) + (l + succ 0 - 1).stirlingFirst k

Tactic:
rfl

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).stirlingFirst (k + 1) = n * n.stirlingFirst (k + 1) + n.stirlingFirst k

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ (0 + 1).stirlingFirst 1 = 0!

Tactic:
rfl

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

Goal state before:
pp: n l : ℕ
hk : l + succ 0 ≠ 0
⊢ (n + 1).stirlingSecond (l + succ 0) = (l + succ 0) * n.stirlingSecond (l + succ 0) + n.stirlingSecond (l + succ 0 - 1)

Tactic:
rfl

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

Goal state before:
pp: k l : ℕ
hn : l + succ 0 ≠ 0
⊢ (l + succ 0).stirlingSecond (k + 1) =
    (k + 1) * (l + succ 0 - 1).stirlingSecond (k + 1) + (l + succ 0 - 1).stirlingSecond k

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ (0 + 1).stirlingSecond 1 = 1

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ∀ (n : ℕ), (∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) → ∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear

Tactic:
rintro n ⟨G, _, rfl, hG⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∃ G_1 x, #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
d i : ℕ
hi : i ≥ d + 1
⊢ (coeff d) (X ^ i) = (coeff d) 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : CommRing α
s✝ : Finset α
x✝ : α × α × α
s : Finset α
x a : α
h : x = x ∧ x + a = x + a ∧ x + 2 * a = x + 2 * a
⊢ (x, a) = (x, a)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
⊢ ∀ ⦃a a' b b' c c' : α⦄,
    (a', b, c) ∈ triangleIndices s →
      (a, b', c) ∈ triangleIndices s → (a, b, c') ∈ triangleIndices s → a = a' ∨ b = b' ∨ c = c'

Tactic:
simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]
    rintro _ _ _ _ _ _ d a ha rfl rfl rfl b' b hb rfl rfl h₁ d' c hc rfl h₂ rfl
    have : a + c = b + b := by linear_combination h₁.symm - h₂.symm
    obtain rfl := hs ha hb hc this
    simp_all

Goal state after: