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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t ≤ bound ε l

Tactic:
rw [iterate_succ_apply', stepBound, bound]

Goal state after:
case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound^[⌊4 / ε ^ 5⌋₊] t * 4 ^ stepBound^[⌊4 / ε ^ 5⌋₊] t ≤
    stepBound^[⌊4 / ε ^ 5⌋₊] (initialBound ε l) * 16 ^ stepBound^[⌊4 / ε ^ 5⌋₊] (initialBound ε l)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ ε ^ 5 / 4 * (↑⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)

Tactic:
← Nat.cast_add_one

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G.edgeSet
s : Finset (Sym2 V)
inst✝ : Fintype ↑(G.deleteEdges ↑s).edgeSet
⊢ (G.deleteEdges ↑s).edgeFinset = G.edgeFinset \ s

Tactic:
ext e

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G.edgeSet
s : Finset (Sym2 V)
inst✝ : Fintype ↑(G.deleteEdges ↑s).edgeSet
e : Sym2 V
⊢ e ∈ (G.deleteEdges ↑s).edgeFinset ↔ e ∈ G.edgeFinset \ s
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
ext e

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet

Tactic:
rw [edgeSet_coe, Set.image_preimage_eq_iff]
  rintro e he
  induction e using Sym2.ind with | h a b =>
  rw [Subgraph.mem_edgeSet] at he
  exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_mk ..⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sSup s).edgeSet = ⋃ G' ∈ s, G'.edgeSet

Tactic:
ext e

Goal state after:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sSup s).edgeSet ↔ e ∈ ⋃ G' ∈ s, G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sInf s).edgeSet = (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
ext e

Goal state after:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ Nonempty (⊥ ≃g { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.coe) ∧
    ∀ (x : G.Subgraph) (a : ⊥ ≃g x.coe), x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

Tactic:
refine ⟨⟨⟨(Equiv.Set.univ _).symm, by simp⟩⟩, fun H' e ↦
    Subgraph.ext ((set_fintype_card_eq_univ_iff _).1 <| Fintype.card_congr e.toEquiv.symm) ?_⟩

Goal state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
H' : G.Subgraph
e : ⊥ ≃g H'.coe
⊢ H'.Adj = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.Adj
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr.calc_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ G.edgeFinset \ (Set.range f).toFinset = (G.killCopies H).edgeFinset

Tactic:
ext e

Goal state after:
case inr.calc_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
e : Sym2 V
⊢ e ∈ G.edgeFinset \ (Set.range f).toFinset ↔ e ∈ (G.killCopies H).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : ↑G'.verts
inst✝¹ : Fintype ↑(G'.coe.neighborSet v)
inst✝ : Fintype ↑(G'.neighborSet ↑v)
⊢ G'.coe.degree v = G'.degree ↑v

Tactic:
by
  rw [← card_neighborSet_eq_degree]
  exact Fintype.card_congr (coeNeighborSetEquiv v)

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
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
ext e

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔ e ∈ G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
⊢ (G.replaceVertex s t).edgeSet = (G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
ext e

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔
    e ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s

Tactic:
tsub_mul,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ n * (#s / n) - #s % n * (#s / n) + #s % n * (#s / n + 1) = #s
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).edgeSet = {s(v, w)}

Tactic:
ext e

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ e ∈ {s(v, w)}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ (G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯

Tactic:
simp [edgeFinset, edgeSet_edge_of_ne h]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n : ℕ
h : n + 1 ≤ (cons h✝ p✝).length
⊢ p✝.getVert (n + 1 - 1) = (u :: p✝.support)[n + 1]

Tactic:
List.getElem_cons

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n : ℕ
h : n + 1 ≤ (cons h✝ p✝).length
⊢ p✝.getVert (n + 1 - 1) = if h : n + 1 = 0 then u else p✝.support[n + 1 - 1]
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mpr.inl.inl
V : Type u
G : SimpleGraph V
w x✝ : V
hvw : G.Adj x✝ w
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝

Tactic:
exact (ha.ne rfl).elim

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

Goal state before:
pp: case Adj.mpr.inl.inr
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha hvw : G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
exact (ha.ne rfl).elim

Goal state after:
case Adj.mpr.inl.inr
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha hvw : G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mpr.inr.inl
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha : G.Adj x✝¹ x✝
hvw : G.Adj x✝ x✝¹
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
exact (ha.ne rfl).elim

Goal state after:
case Adj.mpr.inr.inl
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha : G.Adj x✝¹ x✝
hvw : G.Adj x✝ x✝¹
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mpr.inr.inr
V : Type u
G : SimpleGraph V
v x✝ : V
hvw : G.Adj v x✝
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝

Tactic:
exact (ha.ne rfl).elim

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.edges ≠ []
⊢ p.edges.getLast hp = s(p.penultimate, w)

Tactic:
by
  simp [p.edge_lastDart, Walk.edges]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).length = nil.length + q.length

Tactic:
simp [*, add_comm, add_assoc]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (q : G.Walk w✝ w), (p✝.append q).length = p✝.length + q.length
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).length = (cons h✝ p✝).length + q.length

Tactic:
simp [*, add_comm, add_assoc]

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

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

Tactic:
induction p with
  | nil => simp
  | cons _ p' ih =>
    simp only [support_cons, List.nodup_cons, edges_cons] at h ⊢
    exact ⟨(h.1 <| fst_mem_support_of_mem_edges p' ·), ih h.2⟩

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
⊢ some (p.getVert 0) = p.support.getLast?

Tactic:
List.getLast?_eq_getElem?,

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ some (p.getVert 0) = p.support[p.support.length - 1]?
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsTrail
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail

Tactic:
← take_spec _ h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsPath
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath

Tactic:
← take_spec _ h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
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
this : p.length - 1 = 0
⊢ p.length = 1

Tactic:
grind [length_edges]

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

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

Tactic:
← hx,

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

Goal state before:
pp: α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∩ t)) = ↑(#s) + ↑(#t) - ↑(#(s ∪ t))

Tactic:
eq_sub_iff_add_eq,

Goal state after:
α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∩ t)) + ↑(#(s ∪ t)) = ↑(#s) + ↑(#t)
Module: Mathlib.Data.Finset.CastCard

Goal state before:
pp: α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∪ t)) = ↑(#s) + ↑(#t) - ↑(#(s ∩ t))

Tactic:
eq_sub_iff_add_eq,

Goal state after:
α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∪ t)) + ↑(#(s ∩ t)) = ↑(#s) + ↑(#t)
Module: Mathlib.Data.Finset.CastCard

Goal state before:
pp: α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
h : s ⊆ t
⊢ ↑(#(t \ s)) = ↑(#t) - ↑(#s)

Tactic:
by
  rw [card_sdiff_of_subset h, Nat.cast_sub (card_mono h)]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ↑((Fintype.card α).choose 2) < 2⁻¹ * ↑(Fintype.card α) ^ 2

Tactic:
simpa [← div_eq_inv_mul] using Nat.choose_lt_pow_div (by positivity) le_rfl

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
⊢ |(∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) -
        ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))| ≤
    ε ^ 5 / 49

Tactic:
rw [abs_sub_le_iff]
  constructor
  · rw [sub_le_iff_le_add']
    exact sum_density_div_card_le_density_add_eps hPα hPε hε₁ hA hB
  suffices (G.edgeDensity (A.biUnion id) (B.biUnion id) : ℝ) -
      (∑ ab ∈ A.product B, (G.edgeDensity ab.1 ab.2 : ℝ)) / (#A * #B) ≤ ε ^ 5 / 50 by
    apply this.trans
    gcongr <;> [sz_positivity; norm_num]
  rw [sub_le_iff_le_add, ← sub_le_iff_le_add']
  apply density_sub_eps_le_sum_density_div_card hPα hPε hA hB

Goal state after:
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}
⊢ ∀ (i : G × G), i ∈ univ ×ˢ A ↔ ((Equiv.refl G).prodShear fun a ↦ Equiv.addLeft a) i ∈ B

Tactic:
simp [B]

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

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

Tactic:
filter_eq_self.2,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s ^ 2 * #t ^ 2 = #(s ×ˢ t) ^ 2

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ x ∈ s ×ˢ t, x.1 * x.2 ∈ s * t
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
⊢ σₘ[A] ≤ δₘ[A] ^ 2

Tactic:
by
  obtain rfl | hA' := A.eq_empty_or_nonempty
  · simp
  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)
  calc
    _ = #(A * A) * (#A : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
    _ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
    _ = _ := by rw [← divConst_mul_card]; ring

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

Goal state before:

Tactic:
(#A).choose 2
    _ ≤ (#(A.erase 0) + 1).choose 2 := by grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]
    _ < #(A.erase 0).subsetSum :=
        card_succ_choose_two_lt_card_subsetSum_of_pos fun x hx =>
          (A_pos x (mem_of_mem_erase hx)).lt_of_ne (ne_of_mem_erase hx).symm
    _ = #A.subsetSum := by rw [subsetSum_erase_zero]

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

Goal state before:
pp: 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
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t

Tactic:
tsub_mul,

Goal state after:
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
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ 2 * m * n - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Perm α
⊢ f ∉ fiber none

Tactic:
hyp

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hyp : f ∈ fiber none
⊢ False
Module: Mathlib.Combinatorics.Derangements.Finite

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

pp: case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n < n + 1 + 1

Tactic:
hyp

Goal state after:
case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ (n + 1) * numDerangements n + (n + 1) * numDerangements (n + 1) =
    (n + 1) * numDerangements n + (n + 1) * numDerangements (n + 1)

case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n + 1 < n + 1 + 1

case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n < n + 1 + 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
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ p ∈ map { toFun := f, inj' := hf₁ } univ, lineCount L p

Tactic:
sum_map

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ x, lineCount L ({ toFun := f, inj' := hf₁ } x)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ = A⁻¹ * A

Tactic:
by
  refine Subset.antisymm ?_ (mul_inv_eq_inv_mul_of_doubling_lt_two_aux h)
  simpa using
    mul_inv_eq_inv_mul_of_doubling_lt_two_aux (A := A⁻¹) (by simpa [← mul_inv_rev] using h)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l m : L
⊢ pointCount P l = pointCount P m

Tactic:
by
  apply lineCount_eq_lineCount (Dual P)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

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

Tactic:
simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]

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