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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
classical
  refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
  · have := h (sdiff_subset (t := H.edgeFinset))
    simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset,
      card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
    exact this hH
  · classical
    simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG

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

Goal state before:
pp: case injective'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective ⇑(g.toHom.comp f.toHom)

Tactic:
rw [Hom.coe_comp]

Goal state after:
case injective'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective (⇑g.toHom ∘ ⇑f.toHom)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr.calc_2.hf
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
v w : V
⊢ s(v, w) ∈ G.edgeFinset \ (Set.range f).toFinset ↔ s(v, w) ∈ (G.killCopies H).edgeFinset

Tactic:
| hf v w
   => 

Goal state after:
case inr.calc_2.hf
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
v w : V
⊢ s(v, w) ∈ G.edgeFinset \ (Set.range f).toFinset ↔ s(v, w) ∈ (G.killCopies H).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ Subgraph.coeSubgraph H' ≤ H

Tactic:
by
  constructor
  · simp
  · rintro v w ⟨_, _, h, rfl, rfl⟩
    exact H'.adj_sub h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges s ≤ G'

Tactic:
by
  constructor <;> simp +contextual

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} = sSup (Set.range fun i ↦ fromEdgeSet {↑i})

Tactic:
Set.range,

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} = sSup {x | ∃ y, fromEdgeSet {↑y} = x}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')

Tactic:
by
  constructor
  · simp
  · simp only [sup_adj, induce_adj, Set.mem_union]
    rintro v w (h | h) <;> simp [h]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.darts.Nodup
h : (cons h✝ p').support.Nodup
⊢ (cons h✝ p').darts.Nodup

Tactic:
| cons _ p' ih =>

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) p'.support p'.support.tail
⊢ (cons h✝ p').edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) (cons h✝ p').support (cons h✝ p').support.tail

Tactic:
| cons _ p' ih =>

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.edges.Nodup
h : (cons h✝ p').support.Nodup
⊢ (cons h✝ p').edges.Nodup

Tactic:
| cons _ p' ih =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ w ∈ (c.rotate u h).support ↔ w ∈ c.support

Tactic:
by
  grind [rotate, take_spec, mem_support_append_iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges

Tactic:
have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : 0 < n
h : (p.drop 1).IsPath
⊢ (((p.drop (Nat.succ 0)).drop (n - Nat.succ 0)).copy ⋯ ⋯).IsPath

Tactic:
simp [h.drop (n - 1), -drop_drop]

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

Goal state before:
pp: case h₂
α : 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
⊢ ↑(#B) * ↑(#y) * (↑m / (↑m + 1)) ≤ ↑(#(B.sup id))

Tactic:
apply le_sum_card_subset_chunk_parts hB hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : G.CliqueFree n
⊢ H.CliqueFree n

Tactic:
contrapose h
  rw [not_cliqueFree_iff_top_isContained] at h ⊢
  exact h.trans hle

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

Goal state before:
pp: case neg
α : 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
ms : s ∉ Set.range ⇑φ
⊢ completeGraph (Fin n) ⊑ G

Tactic:
· unfold replaceVertex at hφ
      refine Embedding.isContained ⟨φ.setValue x s, fun {a b} ↦ ?_⟩
      simp only [Embedding.coeFn_mk, Embedding.setValue, not_exists.mp ms, ite_false]
      rw [apply_ite (G.Adj · _), apply_ite (G.Adj _ ·), apply_ite (G.Adj _ ·)]
      convert! @hφ a b <;> simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

Tactic:
have (a b) (hab : a ≠ b) : {s ∈ (G.cliqueSet 3 : Set (Finset α)) | s(a, b) ∈ (s : Finset α).sym2}
    = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}} := by
    ext s
    simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq,
      mem_cliqueSet_iff, Set.mem_ofPred_eq,
      is3Clique_iff]
    constructor
    · rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, hab⟩
      simp only [mem_insert, mem_singleton] at hab
      obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
      any_goals
        simp only [*, adj_comm, true_and, Ne, not_true] at *
      any_goals
        first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩
    · rintro ⟨hab, c, hac, hbc, rfl⟩
      refine ⟨⟨a, b, c, ?_⟩, ?_⟩ <;> simp [*]
  constructor
  · rw [Sym2.forall]
    rintro hG a b hab
    simp only [Sym2.mk_isDiag_iff] at hab
    rw [this _ _ (Sym2.mk_isDiag_iff.not.2 hab)]
    rintro _ ⟨hab, c, hac, hbc, rfl⟩ _ ⟨-, d, had, hbd, rfl⟩
    refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩) <;>
      simp [is3Clique_triple_iff, *]
  · simp only [EdgeDisjointTriangles, is3Clique_iff, Set.Pairwise, mem_cliqueSet_iff, Ne,
      forall_exists_index, and_imp, ← Set.not_nontrivial_iff (s := _ ∩ _), not_imp_not,
      Set.Nontrivial, Set.mem_inter_iff, mem_coe]
    rintro hG _ a b c hab hac hbc rfl _ d e f hde hdf hef rfl g hg₁ hg₂ h hh₁ hh₂ hgh
    refine hG (Sym2.mk_isDiag_iff.not.2 hgh) ⟨⟨a, b, c, ?_⟩, by simpa using And.intro hg₁ hh₁⟩
      ⟨⟨d, e, f, ?_⟩, by simpa using And.intro hg₂ hh₂⟩ <;> simp [*]

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

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G = ⊥

Tactic:
simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x y : α), ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg.refine_1
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∀ w ∈ p.support, w ∈ q.support → w ≠ u → w = v
x✝ : V
⊢ x✝ ∈ p.support.tail → x✝ ∈ q.reverse.support.tail → False

Tactic:
grind [dropLast_support_concat, IsPath.support_nodup, support_reverse, cons_tail_support]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
⊢ (cons h✝ p').bypass.IsPath

Tactic:
| cons _ p' ih =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
⊢ Rel t y x

Tactic:
by cases h <;> constructor <;> assumption

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ExplicitDisjoint (triangleIndices A)

Tactic:
by
  constructor <;> simp +contextual

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

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

Tactic:
by
  -- We show that `insert 0 A` and `a +ᵥ A.subsetSum` are disjoint subsets of
  -- `(insert a A).subsetSum`, and their combined cardinality gives the result.
  -- The sets are disjoint.
  have disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum) := by
    have := nonneg_of_mem_subsetSum (fun y hy ↦ (hA y hy).le)
    simpa [disjoint_left, mem_insert, mem_vadd_finset] using
      ⟨fun x hx => (add_pos_of_pos_of_nonneg ha <| this _ hx).ne',
        fun x hx y hy ↦ (lt_add_of_lt_of_nonneg (hAa x hx) <| this _ hy).ne'⟩
  -- Both sets are subsets of `(insert a A).subsetSum`.
  have insert_subset : insert 0 A ⊆ (insert a A).subsetSum := by
    grw [insert_subset_iff, ← subset_insert]; exact ⟨zero_mem_subsetSum, subset_subsetSum⟩
  have vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum :=
    vadd_finset_subsetSum_subset_subsetSum_insert fun ha => (hAa a ha).false
  -- Count the sizes.
  calc #A + #A.subsetSum
    _ < #A + 1 + #A.subsetSum := by gcongr; exact Nat.lt_add_one _
    _ = #(insert 0 A) + #A.subsetSum := by rw [card_insert_of_notMem fun h => (hA 0 h).false]
    _ = #(insert 0 A) + #(a +ᵥ A.subsetSum) := by simp [vadd_finset_def, card_image_of_injOn]
    _ = #((insert 0 A) ∪ (a +ᵥ A.subsetSum)) := by rw [card_union_of_disjoint disjoint]
    _ ≤ #(insert a A).subsetSum := by grw [union_subset insert_subset vadd_subset]

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 has

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : toColex s ≤ toColex t
hts : toColex t ≤ toColex s
a : α
has : a ∈ s
⊢ a ∈ t
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ + m₂✝) 1 * n✝ 2 - (m₁✝ + m₂✝) 2 * n✝ 1, (m₁✝ + m₂✝) 2 * n✝ 0 - (m₁✝ + m₂✝) 0 * n✝ 2,
      (m₁✝ + m₂✝) 0 * n✝ 1 - (m₁✝ + m₂✝) 1 * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1 + (m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1),
      m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2 + (m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2),
      m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0 + (m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0)]

Tactic:
Pi.add_apply

Goal state after:
case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ 1 + m₂✝ 1) * n✝ 2 - (m₁✝ 2 + m₂✝ 2) * n✝ 1, (m₁✝ 2 + m₂✝ 2) * n✝ 0 - (m₁✝ 0 + m₂✝ 0) * n✝ 2,
      (m₁✝ 0 + m₂✝ 0) * n✝ 1 - (m₁✝ 1 + m₂✝ 1) * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1 + (m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1),
      m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2 + (m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2),
      m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0 + (m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0)]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ + n₂✝) 2 - m✝ 2 * (n₁✝ + n₂✝) 1, m✝ 2 * (n₁✝ + n₂✝) 0 - m✝ 0 * (n₁✝ + n₂✝) 2,
      m✝ 0 * (n₁✝ + n₂✝) 1 - m✝ 1 * (n₁✝ + n₂✝) 0] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1 + (m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1),
      m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2 + (m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2),
      m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0 + (m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0)]

Tactic:
Pi.add_apply

Goal state after:
case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ 2 + n₂✝ 2) - m✝ 2 * (n₁✝ 1 + n₂✝ 1), m✝ 2 * (n₁✝ 0 + n₂✝ 0) - m✝ 0 * (n₁✝ 2 + n₂✝ 2),
      m✝ 0 * (n₁✝ 1 + n₂✝ 1) - m✝ 1 * (n₁✝ 0 + n₂✝ 0)] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1 + (m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1),
      m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2 + (m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2),
      m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0 + (m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0)]
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
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
⊢ #s ≤ #(s.biUnion t)

pp: case neg
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
⊢ #s ≤ #(s.biUnion t)

Tactic:
· simp_rw [hs₀, zero_le]

Goal state after:
case neg
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
⊢ #s ≤ #(s.biUnion t)
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)) < 3 / 2 * ↑(#A)
⊢ ∃ H x, ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A) ∧ ∀ a ∈ A, ↑A ⊆ a •> ↑H ∧ a •> ↑H = ↑H <• a

Tactic:
by
  let H := invMulSubgroup A h
  refine ⟨H, inferInstance, ?_, fun a ha ↦ ⟨?_, ?_⟩⟩
  · simp only [invMulSubgroup, ← coe_mul, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,
      mem_coe, ← Nat.card_eq_fintype_card, H]
    rwa [Nat.card_eq_finsetCard, card_inv_mul_of_doubling_lt_three_halves h]
  · rw [invMulSubgroup_eq_inv_mul]
    exact_mod_cast A_subset_aH a ha
  · simpa [H, invMulSubgroup_eq_inv_mul, ← coe_inv, ← coe_mul, ← coe_smul_finset]
      using smul_inv_mul_eq_inv_mul_opSMul h ha

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) +
      count D (List.take (i - [U].length) ↑p) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U]) +
      count U (List.take (i - [U].length) ↑p)

Tactic:
apply add_le_add _ (p.count_D_le_count_U _)

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U])
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
hc : 0 < a ! * c
⊢ (m.sum + a)! = (m.sum + a).choose a * m.bell * (a ! * c)

Tactic:
by
      simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, hm]

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

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 + 1 < p.firstReturn + 1
⊢ count D (List.take (i - 1 + 1) ↑p) < count U (List.take (i - 1 + 1) ↑p)

Tactic:
rw [Nat.add_lt_add_iff_right] at ub

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 < p.firstReturn
⊢ count D (List.take (i - 1 + 1) ↑p) < count U (List.take (i - 1 + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
by
  simp_rw [insidePart, outsidePart, h, dite_false, nest_denest, DyckWord.ext_iff]
  apply take_append_drop

Goal state after:
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)})
this✝¹ : 0 < #A
ineq : ↑(#S) ≤ (2 - K) * K * ↑l + (K - 1) * K * ↑(#S)
this✝ : φ * ψ = -1
this : φ + ψ = 1
⊢ (φ - K) * (K - ψ) * ↑(#S) / ((2 - K) * K) ≤ (2 - K) * K * ↑l / ((2 - K) * K)

Tactic:
show (φ - K) * (K - ψ) = 1 - (K - 1) * K by grind

Goal state after:
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)})
this✝¹ : 0 < #A
ineq : ↑(#S) ≤ (2 - K) * K * ↑l + (K - 1) * K * ↑(#S)
this✝ : φ * ψ = -1
this : φ + ψ = 1
⊢ (1 - (K - 1) * K) * ↑(#S) / ((2 - K) * K) ≤ (2 - K) * K * ↑l / ((2 - K) * K)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: ⊢ Function.Injective pentagonal

Tactic:
intro x y h

Goal state after:
x y : ℤ
h : pentagonal x = pentagonal y
⊢ x = y
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
x : α × α × α
⊢ x ∈ triangleIndices s ↔ ∃ y, ∃ a ∈ s, (y, y + a, y + 2 * a) = x

Tactic:
by simp [triangleIndices]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ E(G) = ∅ ↔ G = noEdge V(G) β

Tactic:
refine ⟨fun h ↦ Graph.ext rfl ?_, fun h ↦ by rw [h, edgeSet_noEdge]⟩
  simp only [noEdge_isLink, iff_false]
  refine fun e x y he ↦ ?_
  have := h ▸ he.edge_mem
  simp at this

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

Tactic:
cases h : l.idxFun (eι.symm i) <;> simp [h, reindex, coe_apply]

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

Goal state before:
pp: α : Type u_1
e f : Set α
H : Hypergraph α
h : H.EAdj e f
⊢ ∃ x ∈ V(H), x ∈ e ∧ x ∈ f

Tactic:
obtain ⟨x, hx⟩ := h.2.2

Goal state after:
α : Type u_1
e f : Set α
H : Hypergraph α
h : H.EAdj e f
x : α
hx : x ∈ e ∧ x ∈ f
⊢ ∃ x ∈ V(H), x ∈ e ∧ x ∈ f
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)

Tactic:
by
  rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, sdiff_union_self, union_comm]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧
      ∀ ⦃t : Set α⦄, (Disjoint t I ∧ M.Indep (t ∪ I)) ∧ t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
and_imp

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
⊢ M.IsBasis (J ∪ I) (X ∪ I)