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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x✝ y✝ : V
he : s(x✝, y✝) ∈ G'.edgeSet
hv : v ∈ s(x✝, y✝)
⊢ v ∈ G'.verts

Tactic:
rcases Sym2.mem_iff.mp hv with (rfl | rfl)

Goal state after:
case h.inl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v y✝ : V
he : s(v, y✝) ∈ G'.edgeSet
hv : v ∈ s(v, y✝)
⊢ v ∈ G'.verts

case h.inr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x✝ : V
he : s(x✝, v) ∈ G'.edgeSet
hv : v ∈ s(x✝, v)
⊢ v ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
⊢ ∀ (a b : W), Relation.Map H.Adj (⇑f) (⇑f) a b → Relation.Map H.Adj (⇑f) (⇑f) b a

Tactic:
by
    rintro _ _ ⟨u, v, h, rfl, rfl⟩
    exact ⟨v, u, h.symm, rfl, rfl⟩

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

Goal state before:
pp: case refine_3
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts

Tactic:
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
    rintro w hw rfl
    exact h.1 hw

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
⊢ Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty

Tactic:
by
  obtain ⟨e, he⟩ := edgeSet_nonempty.2 hH
  rw [← Subgraph.image_coe_edgeSet_coe]
  exact fun ⟨f⟩ ↦ Set.Nonempty.image _ ⟨_, f.map_mem_edgeSet_iff.2 he⟩

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 ∧ e ∉ G.incidenceSet t
⊢ t ∉ e

Tactic:
obtain ⟨_, h⟩ := he

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
left✝ : e ∈ G.edgeFinset
h : e ∉ G.incidenceSet t
⊢ t ∉ e
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
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - G.degree t = #G.edgeFinset + G.degree s - G.degree t

Tactic:
congr 2

Goal state after:
case e_a.e_a
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) = G.degree s
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
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) - G.degree t - #{s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
congr 2

Goal state after:
case e_a.e_a
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
w✝¹ w✝ : ↑H.verts
h : H'.Adj w✝¹ w✝
⊢ H.Adj (H.hom w✝¹) (H.hom w✝)

Tactic:
exact H'.adj_sub h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support ≠ []

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.head ⋯ = a

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u :: p.support.tail = p.support

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support = u :: p.support.tail

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.support

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support[0] = u

Tactic:
cases p <;> simp

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

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

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
⊢ Walk.map f p = nil ↔ p = nil

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.Nil ↔ p.support = [v]

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.darts = [] ↔ p.Nil

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.edges = [] ↔ p.Nil

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.length = 0 ↔ p.Nil

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ 0 < p.length

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
⊢ p = nil ↔ p.Nil

Tactic:
cases p <;> simp

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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) * ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id)))) ≤
    ↑(#(G.interedges x y)) / (↑(#x) * ↑(#A) * (↑(#y) * ↑(#B)))

Tactic:
mul_comm (#x : ℝ),

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
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) * ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id)))) ≤
    ↑(#(G.interedges x y)) / (↑(#A) * ↑(#x) * (↑(#y) * ↑(#B)))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.reverse.Nil ↔ p.Nil

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
w✝ : ℕ
hn : w✝ + 1 ≠ 0
⊢ ((cons h p).drop (w✝ + 1)).support = ((p.drop (w✝ + 1 - 1)).copy ⋯ ⋯).support

Tactic:
conv_lhs => unfold drop

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
w✝ : ℕ
hn : w✝ + 1 ≠ 0
⊢ (p.drop w✝).support = ((p.drop (w✝ + 1 - 1)).copy ⋯ ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.support.tail

Tactic:
mem_support_iff

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x = v ∨ x ∈ q.support.tail
hq : ¬q.Nil
⊢ x ∈ q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.tail.length = p.length - 1

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ p.tail.getVert n = p.getVert (n + 1)

Tactic:
cases p <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.tail ~ p.support.dropLast

Tactic:
by
  cases p with | nil => rfl | cons h p
  simpa using support_tail_perm_support_dropLast <| p.cons h

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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) / (↑(#x) * ↑(#A) * (↑(#y) * ↑(#B))) ≤
    ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))

Tactic:
mul_comm (#x : ℝ),

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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) / (↑(#A) * ↑(#x) * (↑(#y) * ↑(#B))) ≤
    ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
t : Finset ↑s
n : ℕ
⊢ (induce s G).IsNClique n t ↔ G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)

Tactic:
simp [isNClique_iff, isClique_induce_iff]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
⊢ (List.map (⇑f) p.support).Nodup ↔ p.support.Nodup

Tactic:
List.nodup_map_iff hinj

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
⊢ p.support.Nodup ↔ p.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsClique ↑s ↔ Maximal G.IsIndepSet ↑s

Tactic:
by
  simp [isMaximalIndepSet_iff, isMaximalClique_iff]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsIndepSet ↑s ↔ Maximal G.IsClique ↑s

Tactic:
by
  simp [isMaximalIndepSet_iff, isMaximalClique_iff]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬p.Nil ∧ (List.map (⇑f) p.support.tail).Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup

Tactic:
List.nodup_map_iff hinj

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n < 2 * k * (n / k)

Tactic:
rw [mul_assoc, two_mul, ← add_lt_add_iff_right (n % k), add_right_comm, add_assoc,
    mod_add_div n k, add_comm, add_lt_add_iff_right]
  apply (mod_lt n hk).trans_le
  simpa using Nat.mul_le_mul_left k ((Nat.one_le_div_iff hk).2 hn)

Goal state after:
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 α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ ↑(#({x ∈ s ×ˢ t ×ˢ u |
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) ≤
    ↑(#(G.cliqueFinset 3))

Tactic:
rw [Nat.cast_le]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ #({x ∈ s ×ˢ t ×ˢ u |
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) ≤
    #(G.cliqueFinset 3)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 ≤ ↑(#(A * B)) / ↑(#A)

Tactic:
one_le_div₀

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ ↑(#A) ≤ ↑(#(A * B))

G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 0 < ↑(#A)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * (↑(#A) * ↑(#A)) = ↑(#(A / A)) * ↑(#A)

Tactic:
by rw [← mul_assoc, divConst_mul_card]

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
⊢ ∀ x ∈ f.support, ∑ x_1, coeff x f * ∏ i, x_1 i ^ x i = 0

Tactic:
intro d

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 : σ →₀ ℕ
⊢ d ∈ f.support → ∑ x, coeff d f * ∏ i, x i ^ d i = 0
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:
rw [Equiv.subtypeEquivCodomain_symm_apply_ne]

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 σ
⊢ ∑ x, (eval x) f = 0

Tactic:
by
  have : DecidableEq K := Classical.decEq K
  calc
    ∑ x, eval x f = ∑ x : σ → K, ∑ d ∈ f.support, f.coeff d * ∏ i, x i ^ d i := by
      simp only [eval_eq']
    _ = ∑ d ∈ f.support, ∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i := sum_comm
    _ = 0 := sum_eq_zero ?_
  intro d hd
  obtain ⟨i, hi⟩ : ∃ i, d i < q - 1 := f.exists_degree_lt (q - 1) h hd
  calc
    (∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i) = f.coeff d * ∑ x : σ → K, ∏ i, x i ^ d i :=
      (mul_sum ..).symm
    _ = 0 := (mul_eq_zero.mpr ∘ Or.inr) ?_
  calc
    (∑ x : σ → K, ∏ i, x i ^ d i) =
        ∑ x₀ : { j // j ≠ i } → K, ∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j :=
      (Fintype.sum_fiberwise _ _).symm
    _ = 0 := Fintype.sum_eq_zero _ ?_
  intro x₀
  let e : K ≃ { x // x ∘ ((↑) : _ → σ) = x₀ } := (Equiv.subtypeEquivCodomain _).symm
  calc
    (∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j) =
        ∑ a : K, ∏ j : σ, (e a : σ → K) j ^ d j := (e.sum_comp _).symm
    _ = ∑ a : K, (∏ j, x₀ j ^ d j) * a ^ d i := Fintype.sum_congr _ _ ?_
    _ = (∏ j, x₀ j ^ d j) * ∑ a : K, a ^ d i := by rw [mul_sum]
    _ = 0 := by rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]
  intro a
  let e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl _
  let : Unique { j // j = i } :=
    { default := ⟨i, rfl⟩
      uniq := fun ⟨j, h⟩ => Subtype.val_injective h }
  calc
    (∏ j : σ, (e a : σ → K) j ^ d j) =
        (e a : σ → K) i ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by
      rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]; rfl
    _ = a ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by
      rw [Equiv.subtypeEquivCodomain_symm_apply_eq]
    _ = a ^ d i * ∏ j, x₀ j ^ d j := congr_arg _ (Fintype.prod_congr _ _ ?_)
    -- see below
    _ = (∏ j, x₀ j ^ d j) * a ^ d i := mul_comm _ _
  -- the remaining step of the calculation above
  rintro ⟨j, hj⟩
  change (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j
  rw [Equiv.subtypeEquivCodomain_symm_apply_ne]

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: case pos
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∈ S
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = 1

Tactic:
apply Finset.prod_eq_one
      intro i hi
      rw [hS] at hx
      rw [hx i hi, zero_pow hq.ne', sub_zero]

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

Goal state before:
pp: case refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ #(Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}) = p

pp: case refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ ∑ i ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}, a i = 0

Tactic:
· rw [card_map]
    refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_
    -- This number is nonzero because `x ≠ 0`.
    · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
      exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
    · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
    -- And it is at most `2 * p - 1`, so it must be `p`.
    · rw [univ_eq_attach, card_attach, hs]
      exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one

Goal state after:
case refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ ∑ i ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}, a i = 0
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
v : ℙ K V
⊢ finrank K ↥v.submodule = 1

Tactic:
rw [submodule_eq]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K ↥(K ∙ v.rep) = 1
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 : α) × ↑(Equiv.RemoveNone.fiber (some a)) ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}

Tactic:
simp_rw [Equiv.RemoveNone.fiber_some]
      rfl

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

Goal state before:
pp: case refine_2
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)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ ↑(stabilizer G A) <• a = ↑A

Tactic:
rw [← inv_smul_A ha, smul_comm]

Goal state after:
case refine_2
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)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ a⁻¹ •> (↑A <• a) = ↑A