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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
this : Subsingleton ↑G'.verts
⊢ G'.coe.degree ⟨v, hv⟩ = 0

Tactic:
exact G'.coe.degree_eq_zero_of_subsingleton ⟨v, hv⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), e ≠ b

Tactic:
have : t ∉ e := by
    rw [mem_sdiff, mem_incidenceFinset] at he
    obtain ⟨_, h⟩ := he
    contrapose h
    simp_all [incidenceSet]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
this : t ∉ e
⊢ ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), e ≠ b
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : 0 ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert 0 = (cons h✝ p✝).support[0]

Tactic:
| zero =>

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ 4 ^ #P.parts - (Fintype.card α / #P.parts - m * 4 ^ #P.parts) + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) =
    4 ^ #P.parts

Tactic:
tsub_add_cancel_of_le

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ 4 ^ #P.parts = 4 ^ #P.parts

case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ Fintype.card α / #P.parts - m * 4 ^ #P.parts ≤ 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h : ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
h₀ : p.support[k]? = some [u', v'][0]
h₁ : p.support[k + 1]? = some [u', v'][1]
⊢ G.Adj u' v'

Tactic:
← getVert_eq_support_getElem? _ <| by grind,

Goal state after:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h : ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
h₀ : some (p.getVert k) = some [u', v'][0]
h₁ : some (p.getVert (k + 1)) = some [u', v'][1]
⊢ G.Adj u' v'
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
q₂ : G.Walk u₃ u₂
r₂ : G.Walk v₂ v₃
⊢ p₁.IsSubwalk ((q₂.append ((q₁.append p₁).append r₁)).append r₂)

Tactic:
use q₂.append q₁, r₁.append r₂

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
q₂ : G.Walk u₃ u₂
r₂ : G.Walk v₂ v₃
⊢ (q₂.append ((q₁.append p₁).append r₁)).append r₂ = ((q₂.append q₁).append p₁).append (r₁.append r₂)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
h : u ∈ (cons h✝ p✝).support
⊢ ((cons h✝ p✝).takeUntil u h).append ((cons h✝ p✝).dropUntil u h) = cons h✝ p✝

Tactic:
· cases h
    · simp!
    · simp! only
      split_ifs with h' <;> subst_vars <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
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₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ some p₂.darts[i + k] = some p₁.darts[i]

Tactic:
Option.some_inj

Goal state after:
case refine_1
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₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k] = p₁.darts[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_2
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
⊢ some p₂.support[i + k] = some p₁.support[i]

Tactic:
Option.some_inj

Goal state after:
case refine_2
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
⊢ p₂.support[i + k] = p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case zero
V : Type u_1
G : SimpleGraph V
v : V
n k : ℕ
u : V
p : G.Walk u v
⊢ (p.drop (0 + 1)).IsSubwalk (p.drop 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case zero
V : Type u
G : SimpleGraph V
v u : V
p : G.Walk u v
h : p.length ≤ 0
⊢ p.take 0 = p.copy ⋯ ⋯

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ t ⊆ Set.range ⇑f

Tactic:
intro x hxt

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
x : β
hxt : x ∈ t
⊢ x ∈ Set.range ⇑f
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
rw [← p.cons_tail_eq hpc.not_nil] at hpc

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
⊢ Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case zero
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
hs : G.IsNClique 0 s
⊢ G.IsNClique 0 (insert a (s.erase b))

Tactic:
| zero =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p = ⋯.toWalk

Tactic:
by
  apply p.ext_getVert_le_length <| by simp [hp.length_eq_one_of_mem_edges h]
  intro _ hl
  cases Nat.le_one_iff_eq_zero_or_eq_one.mp (hp.length_eq_one_of_mem_edges h ▸ hl) with
  | inl hl => simp [hl]
  | inr hl =>
    rw [hl, getVert_cons_succ, getVert_zero, ← hp.length_eq_one_of_mem_edges h, getVert_length]

Goal state after:
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
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ ↑((SimpleGraph.map (⇑e) G).cliqueFinset n) = ↑(map { toFun := map e.toEmbedding, inj' := ⋯ } (G.cliqueFinset n))

Tactic:
push_cast; exact cliqueSet_map_of_equiv _ _ _

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ sSup {n | ∃ s, G.IsNIndepSet n s}

Tactic:
← isNClique_compl

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ sSup {n | ∃ s, Gᶜ.IsNClique n s}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
⊢ ∃ s, G.IsNIndepSet (sSup {n | ∃ s, G.IsNIndepSet n s}) s

Tactic:
← isNClique_compl

Goal state after:
α : Type u_3
G : SimpleGraph α
⊢ ∃ s, Gᶜ.IsNClique (sSup {n | ∃ s, Gᶜ.IsNClique n s}) s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = sSup {n | ∃ s, G.IsNIndepSet n s}

Tactic:
← isNClique_compl

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = sSup {n | ∃ s, Gᶜ.IsNClique n s}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(G.edgeDensity (G.badVertices ε s t) t) ≤ ↑(G.edgeDensity s t) - ε

Tactic:
edgeDensity_def

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(↑(#(G.interedges (G.badVertices ε s t) t)) / (↑(#(G.badVertices ε s t)) * ↑(#t))) ≤ ↑(G.edgeDensity s t) - ε
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
pp : p.IsPath
⊢ (p.transfer H hp).IsPath

Tactic:
induction p with
  | nil => simp
  | cons _ _ ih =>
    simp only [Walk.transfer, cons_isPath_iff, support_transfer _] at pp ⊢
    exact ⟨ih _ pp.1, pp.2⟩

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Tactic:
have := Finset.Nonempty.card_pos ⟨_, hX⟩

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
this : 0 < #P.parts
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this : ε ≤ ↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))

Tactic:
edgeDensity_def

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) /
        (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y}))))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))
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
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₂ + y₁ - (x₂ + x₁) = y₁ - x₁ + (y₁ - x₁)

Tactic:
add_sub_add_comm,

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₂ - x₂ + (y₁ - x₁) = y₁ - x₁ + (y₁ - x₁)
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ ∀ x ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ^ 2 ≠ 0 → x ∈ s * t

Tactic:
aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #u * ∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 ≤ #u * ∑ c ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2

Tactic:
by
        refine mul_le_mul_right (sum_le_sum_of_ne_zero ?_) _
        aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∀ (a : K), ∏ j, ↑(e a) j ^ d j = (∏ j, x₀ j ^ d ↑j) * a ^ d i

Tactic:
intro a

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
⊢ ∏ j, ↑(e a) j ^ d j = (∏ j, x₀ j ^ d ↑j) * a ^ d i
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
j : σ
hj : j ≠ i
⊢ ↑(e a) j ^ d j = x₀ ⟨j, hj⟩ ^ d j

Tactic:
Equiv.subtypeEquivCodomain_symm_apply_ne

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
j : σ
hj : j ≠ i
⊢ x₀ ⟨j, ?h⟩ ^ d j = x₀ ⟨j, hj⟩ ^ d j

case h
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
j : σ
hj : j ≠ i
⊢ j ≠ i
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_2
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
        ↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts)) ^
      2

Tactic:
rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]

Goal state after:
case refine_2
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) / ↑((4 * 4) ^ #P.parts)) ^ 2
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ #(A.erase 0).subsetSum = #A.subsetSum

Tactic:
by rw [subsetSum_erase_zero]

Goal state after:
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r ≤ Fintype.card α, #(𝒜 # r) = #𝒜

Tactic:
← card_biUnion,

Goal state after:
α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ #((Iic (Fintype.card α)).biUnion 𝒜.slice) = #𝒜

α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ (↑(Iic (Fintype.card α))).PairwiseDisjoint 𝒜.slice
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case zero
⊢ (bitIndices 0).SortedLT

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case zero
n : ℕ
⊢ (2 ^ 0 * n).bitIndices = map (fun x ↦ x + 0) n.bitIndices

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * 0 - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = 0 ∧ ↑0 ∣ ∑ i ∈ t, a i

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case zero
⊢ (map (fun i ↦ 2 ^ i) (bitIndices 0)).sum = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case zero
i : ℕ
⊢ i ∈ bitIndices 0 ↔ testBit 0 i = true

Tactic:
| zero =>

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

Goal state before:
pp: case composite.zero
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
hk : 0 ≤ 2 * m - 1
⊢ ∃ 𝒜, #𝒜 = 0 ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : toColex s ≤ toColex t
hts : toColex t ≤ toColex s
⊢ s ⊆ t

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : toColex s ≤ toColex t
hts : toColex t ≤ toColex s
a : α
⊢ a ∈ s → a ∈ t
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ ofColex (toColex t)
hbc : b ≤ c
⊢ b < a

Tactic:
exact hbc.trans_lt <| ht _ hct

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

Goal state before:
pp: case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

pp: case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

Tactic:
· rintro ⟨a, ha⟩
    exact ⟨a, ha⟩

Goal state after:
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
h✝ : (crossProduct ↑x✝⁴) ↑x✝¹ = 0
⊢ x✝⁵ ≈ x✝⁴

pp: case neg
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
h✝ : ¬(crossProduct ↑x✝⁴) ↑x✝¹ = 0
⊢ ⟨(a * b) • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩ ≈ ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h✝⟩

Tactic:
· use a

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
h✝ : ¬(crossProduct ↑x✝⁴) ↑x✝¹ = 0
⊢ ⟨(a * b) • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩ ≈ ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h✝⟩