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

Goal state before:
pp: α : 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
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
⊢ ε ^ 5 / 50 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 50

Tactic:
refine mul_le_of_le_one_right (by sz_positivity) ?_

Goal state after:
α : 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
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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

Tactic:
by_cases! h' : w = a

Goal state after:
case pos
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w = a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

case neg
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w ≠ a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ h.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges

Tactic:
isSubwalk_toWalk_iff_mem_darts,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges

Tactic:
isSubwalk_toWalk_iff_mem_darts,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts ↔ s(u', v') ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : 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
⊢ ε ^ 5 / 49 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 49

Tactic:
refine mul_le_of_le_one_right (by sz_positivity) ?_

Goal state after:
α : 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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
by
  constructor
  · rw [isClique_map_iff_of_nontrivial (by simpa)]
    rintro ⟨s, hs, hst⟩
    obtain ⟨s, rfl⟩ := Set.Finite.exists_finset_coe <|
      (show s.Finite from Set.Finite.of_finite_image (by simp [hst]) f.injective.injOn)
    exact ⟨s,hs, Finset.coe_inj.1 (by simpa)⟩
  rintro ⟨s, hs, rfl⟩
  simpa using hs.map (f := f)

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

Goal state before:
pp: α : 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
| (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B))

Tactic:
simp only [SimpleGraph.edgeDensity, edgeDensity, sum_div, Rat.cast_div, div_div]

Goal state after:
α : 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 ∈ A.product B, ↑↑(#(interedges G.Adj x.1 x.2)) / (↑(↑(#x.1) * ↑(#x.2)) * (↑(#A) * ↑(#B)))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (List.map (⇑f) p.support)[↑i]
⊢ u = v

Tactic:
apply this

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (List.map (⇑f) p.support)[↑i]
⊢ (fun i ↦ (List.map (⇑f) p.support)[↑i]) u = (fun i ↦ (List.map (⇑f) p.support)[↑i]) v
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ G.CliqueFree (Fintype.card β) ↔ ⊤.Free G

Tactic:
← not_iff_not,

Goal state after:
α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ ¬G.CliqueFree (Fintype.card β) ↔ ¬⊤.Free 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
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
have ⟨w, hwp, hwq, hwu, hwv⟩ := hw

Goal state after:
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
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
⊢ (induce s G).CliqueFree n ↔ G.CliqueFreeOn s n

Tactic:
simp only [CliqueFree, isNClique_induce_iff]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
⊢ (∀ (t : Finset ↑s), ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)) ↔ G.CliqueFreeOn s n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
n : ℕ
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α ↪ β
hn : n ≠ 1
⊢ map f '' G.cliqueSet n = ⇑{ toFun := map f, inj' := ⋯ } '' G.cliqueSet n

Tactic:
Embedding.coeFn_mk

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ Eₘ[s, t] = ∑ a, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2

Tactic:
by
  rw [mulEnergy_eq_sum_sq']
  exact Fintype.sum_subset <| by aesop (add simp [filter_eq_empty_iff, mul_mem_mul])

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
⊢ insert 0 A ⊆ (insert a A).subsetSum

Tactic:
grw [insert_subset_iff, ← subset_insert]

Goal state after:
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
⊢ 0 ∈ A.subsetSum ∧ A ⊆ A.subsetSum
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬v.orthogonal w

Tactic:
induction v with | h v hv =>
  rw [ne_eq, ← dotProduct_eq_zero_iff, not_forall] at hv
  obtain ⟨w, hw⟩ := hv
  exact ⟨mk F w fun h ↦ hw (by rw [h, dotProduct_zero]), hw⟩

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
⊢ mk F v hv = mk F w hw ↔ (crossProduct v) w = 0

Tactic:
← not_iff_not,

Goal state after:
F : Type u_1
inst✝ : Field F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
⊢ ¬mk F v hv = mk F w hw ↔ ¬(crossProduct v) w = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ : toColex t₂ < toColex t₁ ∧ #t₂ = #s
⊢ toColex t₂ ≤ toColex s

Tactic:
rw [mem_initSeg] at ht₁

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : #s = #t₁ ∧ toColex t₁ ≤ toColex s
ht₂ : toColex t₂ < toColex t₁ ∧ #t₂ = #s
⊢ toColex t₂ ≤ toColex s
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v

Tactic:
by
  induction v with | h v hv =>
  induction w with | h w hw =>
  rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:

Tactic:
(Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } :=
        (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
      _ ≃ { x : L × P // x.2 ∈ x.1 } := (Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl
      _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l

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

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

Tactic:
tendsto_add_atTop_iff_nat
      (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial) atTop (𝓝 (Real.exp (-1)))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e'_2.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

pp: case e'_3
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum

Tactic:
· simp only [toFinset_replicate]
    split_ifs with hm
    · rw [hm, factorial_zero, eq_comm]
      rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]
    · rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
      simp only [Finset.prod_singleton, count_replicate_self]

Goal state after:
case e'_3
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum
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)})
⊢ ∑ z ∈ S with (K - 1) * ↑(#A) < ↑(r z), ↑(r z) + ∑ z ∈ S with ↑(r z) ≤ (K - 1) * ↑(#A), ↑(r z) ≤
    ∑ z ∈ S with (K - 1) * ↑(#A) < ↑(r z), ↑(#A) + ∑ z ∈ S with ↑(r z) ≤ (K - 1) * ↑(#A), (K - 1) * ↑(#A)

Tactic:
by
          gcongr with z hz z hz
          · exact convolution_le_card_left
          · simp_all

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu 𝕜) x b = if a = b then 1 else 0

Tactic:
by
  rw [mu_eq_mu', sum_Icc_mu'_left]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, (zeta 𝕜) y z * f z = ∑ y ≥ x, ∑ z ≥ y, (mu 𝕜) x y * (zeta 𝕜) y z * f z

Tactic:
simp [mul_sum]

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

Goal state before:
pp: case tail.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
⊢ p.semilength ≤ r.semilength

Tactic:
· rcases mq with hm | hm
      · exact ih.trans (hm ▸ semilength_insidePart_lt hr).le
      · exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

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

Goal state before:
pp: k : ℤ
⊢ 2 * ↑(pentagonal (-k)) = k * (3 * k + 1)

Tactic:
by
  grind [two_mul_natCast_pentagonal]

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

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

Tactic:
rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;>
      · #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
        we need to re-enable model-based theory combination in `lia` for this to go through. -/
        lia +mbtc

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)

Tactic:
by
  simp only [Inc, banana_isLink, exists_and_left, and_congr_right_iff]
  aesop

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
by
  rintro l m hlm
  ext i a
  obtain ⟨b, hba⟩ := exists_ne a
  simp only [funext_iff] at hlm ⊢
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · cases hi : idxFun m i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i
  · cases hi : idxFun l i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i

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)
⊢ Function.LeftInverse (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩

Tactic:
rintro ⟨x, hx⟩

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx : x ∈ sᶜ
⊢ (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩) ⟨x, hx⟩) = ⟨x, hx⟩
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ False

Tactic:
apply this

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ coeff (m.degree f) (m.subLTerm f) = 0
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
obtain ⟨g', r', H'⟩ := div hb (m.reduce (hb i) f)

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
by_cases heI : e ∈ I

Goal state after:
case pos
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
heI : e ∈ I
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

case neg
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
heI : e ∉ I
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case inl
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
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1

Tactic:
rw [ha0, hb1] at hab
      exact hab

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
this : ∀ (p q : Path r b), p = q
p : Path r b
⊢ p = default

Tactic:
apply this

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
⊢ ∃ p, 0 < p.length

Tactic:
obtain ⟨p₁⟩ := h_sc i i₀

Goal state after:
V : Type u_2
inst✝ : Quiver V
h_sc : IsStronglyConnected V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path i i₀
⊢ ∃ p, 0 < p.length
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case e'_2.e'_6
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
a✝ : i ∈ h.support
⊢ (eval x) (∏ r ∈ S i, (X i - C r)) = 0

Tactic:
_root_.map_prod

Goal state after:
case e'_2.e'_6
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
a✝ : i ∈ h.support
⊢ ∏ x_1 ∈ S i, (eval x) (X i - C x_1) = 0
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 : {i j : V} → (i ⟶ j) → R
a : V
⊢ weight (fun {i j} ↦ w) nil = 1

Tactic:
by
  simp [weight]

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 : {i j : V} → (i ⟶ j) → R
a b c : V
p : Path a b
e : b ⟶ c
⊢ weight (fun {i j} ↦ w) (p.cons e) = weight (fun {i j} ↦ w) p * w e

Tactic:
by
  simp [weight]

Goal state after: