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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ K ^ (3 * (m - 2)) * ↑(#A)

Tactic:
by
  have hm₀ : m ≠ 0 := by positivity
  have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i
  obtain rfl | hA₀ := A.eq_empty_or_nonempty
  · simp [hm₀, hε₀]
  have hK₁ : 1 ≤ K :=
    one_le_of_le_mul_right₀ (by positivity)
      (hA.trans' <| by norm_cast; exact card_le_card_pow (by simp))
  rw [pow_mul]
  refine inductive_claim_mul hm (fun δ hδ ↦ ?_) ε hε
  simp only [finRange_succ, Nat.reduceAdd, isValue, finRange_zero, map_nil, List.map_cons,
    succ_zero_eq_one, succ_one_eq_two, List.prod_cons, prod_nil, mul_one, ← mul_assoc]
  simp only [zero_le_one, abs_eq, Int.reduceNeg, forall_iff_succ, isValue, succ_zero_eq_one,
    succ_one_eq_two, IsEmpty.forall_iff, and_true] at hδ
  have : K ^ 2 ≤ K ^ 3 := by gcongr; simp
  obtain ⟨hδ₀ | hδ₀, hδ₁ | hδ₁, hδ₂ | hδ₂⟩ := hδ <;> simp [hδ₀, hδ₁, hδ₂]
  · simp [pow_succ] at hA
    nlinarith
  · nlinarith [small_pos_pos_neg_mul hA]
  · nlinarith [small_pos_neg_pos_mul hA]
  · nlinarith [small_pos_neg_neg_mul hA]
  · nlinarith [small_neg_pos_pos_mul hA]
  · nlinarith [small_neg_pos_neg_mul hA]
  · nlinarith [small_neg_neg_pos_mul hA]
  · simp [*, pow_succ', ← mul_inv_rev] at hA ⊢
    nlinarith

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

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ G₁.edgeFinset = G₂.edgeFinset ↔ G₁ = G₂

Tactic:
by simp [edgeFinset]

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

Goal state before:
pp: V : Type u_1
⊢ ⊥.edgeFinset = ∅

Tactic:
by simp [edgeFinset]

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

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝³ : Fintype ↑G₁.edgeSet
inst✝² : Fintype ↑G₂.edgeSet
inst✝¹ : Fintype ↑(G₁ ⊔ G₂).edgeSet
inst✝ : DecidableEq V
⊢ (G₁ ⊔ G₂).edgeFinset = G₁.edgeFinset ∪ G₂.edgeFinset

Tactic:
by simp [edgeFinset]

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

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

Tactic:
by simp [edgeFinset]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
⊢ (↑P.parts).PairwiseDisjoint f

Tactic:
by
  intro _ hx _ hy hxy
  have := (P.disjoint hx hy hxy).eq_bot
  simp_all [disjoint_iff, ← hf]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
b : α
⊢ b ∈ P.parts ↔ b ∈ (indiscrete ⋯).parts

Tactic:
refine Iff.trans ⟨h b, ?_⟩ mem_singleton.symm

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
b : α
⊢ b = a → b ∈ P.parts
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
let el := {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
  let es := {p ∈ P.parts | #p = #s / #P.parts}.equivFin
  simp_rw [mem_filter, hP.card_large_parts_eq_mod] at el
  simp_rw [mem_filter, hP.card_small_parts_eq_mod] at es
  let sneg :
      {x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1} ≃ {x // x ∈ P.parts ∧ #x = #s / #P.parts} := by
    apply (Equiv.refl _).subtypeEquiv
    simp only [Equiv.refl_apply, and_congr_right_iff]
    exact fun _ ha ↦ by rw [hP.card_part_eq_average_iff ha, ne_eq]
  replace el : { x : P.parts // #x.1 = #s / #P.parts + 1 } ≃
      Fin (#s % #P.parts) := (Equiv.Set.sep ..).symm.trans el
  replace es : { x : P.parts // ¬#x.1 = #s / #P.parts + 1 } ≃
      Fin (#P.parts - #s % #P.parts) := (Equiv.Set.sep ..).symm.trans (sneg.trans es)
  let f := (Equiv.sumCompl _).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
  use f.trans (finCongr (Nat.add_sub_of_le P.card_mod_card_parts_le))
  intro ⟨p, _⟩
  simp_rw [f, Equiv.trans_apply, Equiv.sumCongr_apply, finCongr_apply, Fin.val_cast]
  by_cases hc : #p = #s / #P.parts + 1 <;> simp [hc]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : x ∈ ↑(image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset)
y : Finset α
hy : y ∈ ↑(image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset)
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
⊢ x = y

Tactic:
rw [mem_coe, mem_image] at hx hy
            obtain ⟨Q, hQ, rfl⟩ := hx
            obtain ⟨R, hR, rfl⟩ := hy
            suffices h' : Q = R by
              subst h'
              exact of_eq_true (eq_self {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
            rw [id, mem_filter] at hz1 hz2
            rw [mem_powerset] at hQ hR
            ext i
            refine ⟨fun hi ↦ ?_, fun hi ↦ ?_⟩
            · rwa [hz2.2 _ (hQ hi), ← hz1.2 _ (hQ hi)]
            · rwa [hz1.2 _ (hR hi), ← hz2.2 _ (hR hi)]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : b ≤ a
X : C
⊢ (t.eTruncLTLTIsoLT a b hab).inv.app X ≫ (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) = 𝟙 ((t.eTruncLT.obj b).obj X)

Tactic:
simpa using (t.eTruncLTLTIsoLT a b hab).inv_hom_id_app X

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ interedges r s t = s.biUnion fun x ↦ map { toFun := fun x_1 ↦ (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ interedges r s t ↔
    (x, y) ∈ s.biUnion fun x ↦ map { toFun := fun x_1 ↦ (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ G.nonuniformWitness ε s t ⊆ s

Tactic:
by
  unfold nonuniformWitness
  split_ifs
  · exact G.left_nonuniformWitnesses_subset h
  · exact G.right_nonuniformWitnesses_subset fun i => h i.symm

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

Goal state before:
pp: case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)

Tactic:
exact Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ {x ∈ A ×ˢ A |
      match x with
      | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y} ⊆
    ((P.nonUniforms G (ε / 8)).biUnion fun x ↦
          match x with
          | (U, V) => U ×ˢ V) ∪
        P.parts.biUnion offDiag ∪
      (P.sparsePairs G (ε / 4)).biUnion fun x ↦
        match x with
        | (U, V) => G.interedges U V

Tactic:
rintro ⟨x, y⟩

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
⊢ (x, y) ∈
      {x ∈ A ×ˢ A |
        match x with
        | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y} →
    (x, y) ∈
      ((P.nonUniforms G (ε / 8)).biUnion fun x ↦
            match x with
            | (U, V) => U ×ˢ V) ∪
          P.parts.biUnion offDiag ∪
        (P.sparsePairs G (ε / 4)).biUnion fun x ↦
          match x with
          | (U, V) => G.interedges U V
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ #⊥.parts ∧ #⊥.parts ≤ bound ε l ∧ ⊥.IsUniform G ε

Tactic:
card_bot,

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ #univ ∧ #univ ≤ bound ε l ∧ ⊥.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∉ (G.incidenceSet x).toFinset ↔ x ∉ x✝

Tactic:
Set.mem_toFinset,

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∉ G.incidenceSet x ↔ x ∉ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case mp
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ f.toCopy.toSubgraph.IsInduced

Tactic:
simp [Subgraph.IsInduced, Relation.map_apply_apply, f.injective]

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
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ G.copyCount H = #(image Copy.toSubgraph univ)

Tactic:
by
  rw [copyCount]
  congr
  refine Finset.coe_injective ?_
  simpa [-Copy.range_toSubgraph] using Copy.range_toSubgraph.symm

Goal state after:
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
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Fintype G.Subgraph

Tactic:
by
  refine .ofBijective
    (α := {H : Finset V × (V → V → Bool) //
      (∀ a b, H.2 a b → G.Adj a b) ∧ (∀ a b, H.2 a b → a ∈ H.1) ∧ ∀ a b, H.2 a b = H.2 b a})
    (fun H ↦ ⟨H.1.1, fun a b ↦ H.1.2 a b, @H.2.1, @H.2.2.1, by simp [symm_def, H.2.2.2]⟩)
    ⟨?_, fun H ↦ ?_⟩
  · rintro ⟨⟨_, _⟩, -⟩ ⟨⟨_, _⟩, -⟩
    simp [funext_iff]
  · classical
    exact ⟨⟨(H.verts.toFinset, fun a b ↦ H.Adj a b), fun a b ↦ by simpa using H.adj_sub,
      fun a b ↦ by simpa using H.edge_vert, by simp [H.adj_comm]⟩, by simp⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
t : Finset V
ht : ↑t = G.neighborSet v
h : ↑↑t ≃ ↑↑s
⊢ s ⊆ t

Tactic:
← Finset.coe_subset,

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
t : Finset V
ht : ↑t = G.neighborSet v
h : ↑↑t ≃ ↑↑s
⊢ ↑s ⊆ ↑t
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
⊢ Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)

Tactic:
by
  ext <;> simp only [Relation.Map, Subgraph.map_adj, singletonSubgraph_adj, Pi.bot_apply,
    exists_and_left, and_iff_left_iff_imp, Subgraph.map_verts,
    singletonSubgraph_verts, Set.image_singleton]
  exact False.elim

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ ∈ {v}
ha2 : x✝ ∈ {v}
⊢ False

Tactic:
Set.mem_singleton_iff

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ = v
ha2 : x✝ = v
⊢ False
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
⊢ Disjoint (G.edgeFinset \ G.incidenceFinset t) (image (fun x ↦ s(x, t)) (G.neighborFinset s))

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

Goal state after:
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
⊢ G.Adj u' v'

Tactic:
by
  have ⟨k, hk, h⟩ := List.infix_iff_getElem?.mp h
  have h₀ := Nat.zero_add _ ▸ h 0 Nat.zero_lt_two
  have h₁ := Nat.add_comm .. ▸ h 1 Nat.one_lt_two
  rw [← getVert_eq_support_getElem? _ <| by grind, Option.some.injEq] at h₀ h₁
  exact h₀ ▸ h₁ ▸ p.adj_getVert_succ (i := k) <| by grind

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

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

Tactic:
by
  obtain ⟨_ | _, h⟩ := p
  · rfl
  · simp at h

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
k✝ : ℕ
hl : k✝ ≤ p.length
x✝ : k✝ = 0 ∨ k✝ = 1
⊢ p.getVert k✝ = ⋯.toWalk.getVert k✝

Tactic:
cases Nat.le_one_iff_eq_zero_or_eq_one.mp (hp.length_eq_one_of_mem_edges h ▸ hl) with

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
⊢ False

Tactic:
obtain ⟨t, hts, ht⟩ := exists_subset_card_eq (h.trans hs.card_eq.ge)

Goal state after:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
t : Finset α
hts : t ⊆ s
ht : #t = m
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3

Tactic:
refine card_mul_le_card_mul (fun e s ↦ e ∈ s.sym2) ?_ ?_

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun e s ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)

case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ b ∈ G.cliqueFinset 3, #(bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3
Module: Mathlib.Data.Finset.CastCard

Goal state before:
pp: α : Type u_1
R : Type u_2
s : Finset α
a : α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
hs : a ∈ s
⊢ ↑(#(s.erase a)) = ↑(#s) - 1

Tactic:
rw [← card_erase_add_one hs, cast_add, cast_one, eq_sub_iff_add_eq]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ ↑(#(A ∪ B)) + ↑(#C) ≤ ↑(#A) + ↑(#B) + ↑(#C)

Tactic:
gcongr; exact mod_cast card_union_le _ _

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ δₘ[A, B] ≤ ↑(#B)

Tactic:
rw [divConst, div_le_iff₀' (by positivity)]

Goal state after:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / B)) ≤ ↑(#A) * ↑(#B)
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ ∑ b ∈ insert a B, b = a +ᵥ ∑ b ∈ B, b

Tactic:
by rw [sum_insert (fun h => a_notin_A (hB h))]; simp

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

Goal state before:
pp: case refine_2.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
⊢ 2 * p - 1 < 2 * p

Tactic:
exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 - v 2 * w 1 = 0 ∧ v 2 * w 0 - v 0 * w 2 = 0 ∧ v 0 * w 1 - v 1 * w 0 = 0
⊢ False

Tactic:
sub_eq_zero

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
⊢ False
Module: Mathlib.Combinatorics.Colex

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

Tactic:
have hma : m < a := (min'_le _ _ hwt).trans_lt hwa
    refine (lt_iff_exists_forall_lt.2 ⟨a, mem_erase.2 ⟨hma.ne', (hw hwa).1 ha⟩,
      notMem_erase _ _, fun b hbs hbt ↦ ?_⟩).le
    change b ∉ t.erase m at hbt
    rw [mem_erase, not_and_or, not_ne_iff] at hbt
    obtain rfl | hbt := hbt
    · assumption
    · by_contra! hab
      exact hbt <| (hw <| hwa.trans_le hab).1 <| mem_of_mem_erase hbs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(derangements (Subtype p)) ≃ { f // ∀ a ∈ fixedPoints ⇑↑f, ¬p a }

Tactic:
refine (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => ?_, ?_⟩
      · refine hf ⟨a, ha⟩ (Subtype.ext ?_)
        simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm,
        Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa
        assumption
      rintro hf ⟨a, ha⟩ hfa
      refine hf _ ?_ ha
      simp only [Perm.subtypeEquivSubtypePerm_apply_coe, mem_fixedPoints]
      dsimp [IsFixedPt]
      simp_rw [Perm.ofSubtype_apply_of_mem _ ha, hfa]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : ∀ x ∈ s, p₁ ∉ {p | p ∉ x}.toFinset
hp₂ : ∀ x ∈ s, p₂ ∉ {p | p ∉ x}.toFinset
⊢ p₁ = p₂

Tactic:
Set.mem_toFinset,

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : ∀ x ∈ s, p₁ ∉ {p | p ∉ x}
hp₂ : ∀ x ∈ s, p₂ ∉ {p | p ∉ x}
⊢ p₁ = p₂
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
x a : G
ha : a ∈ A
⊢ a •> x <• a ∈ A <• a ↔ a * x ∈ A

Tactic:
smul_mem_smul_finset_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
x a : G
ha : a ∈ A
⊢ a •> x ∈ A ↔ a * x ∈ A
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, ↑(r z) = ∑ z ∈ S with (K - 1) * ↑(#A) < ↑(r z), ↑(r z) + ∑ z ∈ S with ↑(r z) ≤ (K - 1) * ↑(#A), ↑(r z)

Tactic:
norm_cast; simp_rw [← not_lt, sum_filter_add_sum_filter_not]

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

Goal state before:
pp: case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ ∀ j < p.firstReturn, decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
intro j hj
      rw [take_append, show j + 1 - p.toList.length = 0 by lia,
        take_zero, append_nil]
      simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength + p.outsidePart.semilength + 1 = p.insidePart.semilength + 1 + p.outsidePart.semilength

Tactic:
add_right_comm

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength + 1 + p.outsidePart.semilength = p.insidePart.semilength + 1 + p.outsidePart.semilength
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

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

Tactic:
have : b + 1 < m := by grind

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
this : b + 1 < m
⊢ X ^ ((i + 1) * (b + 1)) = (if b + 1 < m then 1 else 0) • X ^ ((i + 1) * (b + 1))