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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinset, G.degree v = ∑ v, G.degree v

Tactic:
← sum_add_sum_compl G.support.toFinset,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinset, G.degree v = ∑ v ∈ G.support.toFinset, G.degree v + ∑ v ∈ G.support.toFinsetᶜ, G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
⊢ Injective ⇑f

Tactic:
by
  intro v w h
  contrapose! h
  exact G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h))

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
by
  refine ⟨?_, fun ⟨b, hb⟩ x y hx hy => by grw [(hb x hx).2, (hb y hy).1]⟩
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · simp
  intro hs
  by_cases! h : ∀ y ∈ s, f x ≤ f y
  · exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩
  obtain ⟨w, hw, hwx⟩ := h
  refine ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ ?_, hs hy hw⟩⟩
  rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]
  exact hs hx hy

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
⊢ Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v}

Tactic:
simp only [neighborFinset, neighborSet_compl, Set.toFinset_sdiff, Set.toFinset_compl,
    Set.toFinset_singleton]

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

Goal state before:
pp: case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]

Goal state after:
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s|
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
htcard : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
h : δ < 1
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ

Tactic:
exact (abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq r hs ht hδ h hscard htcard).trans
      ((sub_le_self_iff _).2 <| sq_nonneg δ)

Goal state after:
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 α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ε ^ 5 * ↑i ≤ 4
⊢ ↑i ≤ 4 / ε ^ 5

Tactic:
le_div_iff₀' (pow_pos hε _)

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 α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ε ^ 5 * ↑i ≤ 4
⊢ ε ^ 5 * ↑i ≤ 4
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
u v : V
⊢ (G.deleteEdges s).Adj u v ↔ G.Adj u v

Tactic:
simpa using (·.ne <| hs ·)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ (G.deleteIncidenceSet x).Adj v₁ v₂ ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x

Tactic:
rw [deleteIncidenceSet, deleteEdges_adj, mk'_mem_incidenceSet_iff]
  tauto

Goal state after:
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
⊢ (G.deleteIncidenceSet x).edgeFinset = {x_1 ∈ G.edgeFinset | x ∉ x_1}

Tactic:
edgeFinset_deleteIncidenceSet_eq_sdiff,

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
⊢ G.edgeFinset \ G.incidenceFinset x = {x_1 ∈ G.edgeFinset | x ∉ x_1}
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 / 7 * ↑(#P.parts) ^ 2 * ε ^ 5 * (7 / 24) ≤ ↑(#P.parts.offDiag) * ε ^ 5 * (22 / 75)

Tactic:
gcongr ?_ * _ * ?_
        · rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
          norm_cast
          rw [tsub_mul]
          refine le_tsub_of_add_le_left ?_
          nlinarith
        · norm_num

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
ha : G.Adj s t
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
  rw [G.edgeFinset_replaceVertex_of_adj ha, card_sdiff_of_subset (by simp [ha]),
    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
    ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]
  congr 2
  rw [card_image_of_injective, card_neighborFinset_eq_degree]
  unfold Function.Injective
  aesop

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.coeSubgraph (Subgraph.restrict H')).Adj x✝¹ x✝ ↔ (H ⊓ H').Adj x✝¹ x✝

Tactic:
simp_rw [coeSubgraph_adj, restrict_adj]
    simp only [exists_and_left, exists_prop, inf_adj, and_congr_right_iff]
    intro h
    simp [H.edge_vert h, H.edge_vert h.symm]

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
⊢ (cons h✝ p✝).getVert (n + 1) = (cons h✝ p✝).support[n + 1]

Tactic:
support_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
⊢ (cons h✝ p✝).getVert (n + 1) = (u :: p✝.support)[n + 1]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' w✝ : V
p✝¹ : G.Walk u✝¹ v✝¹
u✝ v✝ : V
p✝ : G.Walk u✝ v✝
H : SimpleGraph V
u w v : V
h✝ : G.Adj u v
p : G.Walk v w
h : ∀ e ∈ (cons' u v w h✝ p).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (cons' u v w h✝ p).edges

Tactic:
by simp [he]

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w✝ : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (p.append q).edges

Tactic:
by simp [he]

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w✝ : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ q.edges
⊢ e ∈ (p.append q).edges

Tactic:
by simp [he]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat (cons ⋯ p.reverse) ≍ Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)

Tactic:
rw [concatRecAux, eqRec_heq_iff]

Goal state after:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ Hconcat p.reverse.reverse ⋯ (concatRecAux Hnil Hconcat p.reverse) ≍
    Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h : p₂.IsSubwalk p₁
f : G →g G'
⊢ (Walk.map f p₂).IsSubwalk (Walk.map f p₁)

Tactic:
by
  simp [isSubwalk_iff_support_isInfix, isSubwalk_iff_support_isInfix.mp h, List.IsInfix.map]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ w ∉ (p.takeUntil x ⋯).support

Tactic:
by
  rw [← takeUntil_takeUntil p hw hx]
  intro hw'
  have h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length
      < ((p.takeUntil w hw).takeUntil x hx).length := by
    exact length_takeUntil_lt_length _ h.symm
  have h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length := by
    exact length_takeUntil_lt_length _ h
  simp only [takeUntil_takeUntil] at h1 h2
  lia

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
n m : ℕ
⊢ p.drop (n + m) ≍ (p.drop n).drop m

Tactic:
by
  rw [add_comm]
  induction p generalizing n <;> cases n <;> simp [*, drop]

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
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
⊢ q.IsPath

Tactic:
by
  have := hcyc.2
  rw [tail_support_append, List.nodup_append'] at this
  rw [isPath_def, ← cons_tail_support, List.nodup_cons]
  exact ⟨this.2.2 (p.end_mem_tail_support h), this.2.1⟩

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
n m : ℕ
⊢ ((p.drop n).drop m).support = ((p.drop (n + m)).copy ⋯ ⋯).support

Tactic:
simp_rw [support_copy, drop_support_eq_support_drop_min, drop_length, List.drop_drop]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ List.drop (min n p.length + min m (p.length - n)) p.support = List.drop (min (n + m) p.length) p.support
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.Nil
⊢ p = Walk.nil.copy ⋯ ⋯

Tactic:
by
  grind [eq_nil_iff_nil, copy_rfl_rfl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab
  exact ⟨hab, a, b, h ha hb <| ne_of_apply_ne _ hab, rfl, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
by
  obtain (ht | ht) := le_or_gt #t 1
  · simp only [ht, true_or, iff_true]
    exact IsClique.of_subsingleton <| card_le_one.1 ht
  rw [isClique_map_finset_iff_of_nontrivial, ← not_lt]
  · simp [ht]
  exact Finset.one_lt_card_iff_nontrivial.mp ht

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f : G →g G'
h : (Walk.map f p).IsPath
⊢ Set.InjOn ⇑f {w | w ∈ p.support}

Tactic:
intro u hu v hv hf
  obtain ⟨u, rfl⟩ := List.get_of_mem hu
  obtain ⟨v, rfl⟩ := List.get_of_mem hv
  congr
  have := List.nodup_iff_injective_getElem.mp h.support_nodup
  rw! (castMode := .all) [support_map, List.length_map] at this
  apply this
  simpa

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).support <:+: (cons hadj p).support

Tactic:
support_cons,

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ u :: (p.takeUntil u hup).support <:+: (cons hadj p).support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

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

Tactic:
simp [hp.length_eq_one_of_mem_edges h]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ G.CliqueFree (Fintype.card β) ↔ ⊤.Free G

Tactic:
rw [← not_iff_not, not_free, not_cliqueFree_iff_top_isContained,
    isContained_congr (Iso.completeGraph (equivFin β)) Iso.refl]

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

Goal state before:
pp: case mk.refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).1 ∈ s

pp: case mk.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).2 ∈ s

Tactic:
· exact Set.not_notMem.mp <| not_and'.mp (c ▸ Set.notMem_empty v) <| Sym2.mem_mk_left ..

Goal state after:
case mk.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).2 ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ 0 < triangleRemovalBound ε

Tactic:
have : 0 < 1 - min 1 ε / 4 := by have := min_le_left 1 ε; linarith
  unfold triangleRemovalBound
  positivity

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 α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this✝ :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
this : 0 ≤ ε
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ ↑(#X') * (ε ^ 3 * ↑(#t) * ↑(#u))

Tactic:
suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this✝ :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
this : 0 ≤ ε
⊢ (1 - 2 * ε) * ↑(#s) ≤ ↑(#X')
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, hj⟩ ^ d ↑⟨j, hj⟩ = x₀ ⟨j, hj⟩ ^ d ↑⟨j, hj⟩

Tactic:
change (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R

Tactic:
by
  apply LinearMap.mk₂ R fun a b : Fin 3 → R =>
      ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]
  · intros
    simp_rw [vec3_add, Pi.add_apply]
    apply vec3_eq <;> ring
  · intros
    simp_rw [smul_vec3, Pi.smul_apply, smul_sub, smul_mul_assoc]
  · intros
    simp_rw [vec3_add, Pi.add_apply]
    apply vec3_eq <;> ring
  · intros
    simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ ((∀ (a : α), ¬p a → a ∈ fixedPoints ⇑f) ∧ ∀ a ∈ fixedPoints ⇑f, ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ⇑f

Tactic:
← forall_and,

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ (∀ (x : α), (¬p x → x ∈ fixedPoints ⇑f) ∧ (x ∈ fixedPoints ⇑f → ¬p x)) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ⇑f
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:
by rw [sum_map]; dsimp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)

Tactic:
swap_apply_of_ne_of_ne ne_1 ne_2,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ some (f x) ≠ some x
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case refine_2
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
p : P
hp : ¬∃ a, f a = p
⊢ 0 < lineCount L p

Tactic:
rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
a b : G
hA : ↑(#(B * A)) ≤ K * ↑(#A)
ha : a ∈ B
hb : b ∈ B
⊢ (2 - K) * ↑(#A) ≤ ↑(#(a •> A ∩ b •> A))

Tactic:
have : 2 * (#A : ℝ) ≤ #(a •> A ∩ b •> A) + #(B * A) := mod_cast big_intersection ha hb

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
a b : G
hA : ↑(#(B * A)) ≤ K * ↑(#A)
ha : a ∈ B
hb : b ∈ B
this : 2 * ↑(#A) ≤ ↑(#(a •> A ∩ b •> A)) + ↑(#(B * A))
⊢ (2 - K) * ↑(#A) ≤ ↑(#(a •> A ∩ b •> A))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
a b : G
hA : ↑(#(B * A)) < K * ↑(#A)
ha : a ∈ B
hb : b ∈ B
⊢ (2 - K) * ↑(#A) < ↑(#(a •> A ∩ b •> A))

Tactic:
have : 2 * (#A : ℝ) ≤ #(a •> A ∩ b •> A) + #(B * A) := mod_cast big_intersection ha hb

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
a b : G
hA : ↑(#(B * A)) < K * ↑(#A)
ha : a ∈ B
hb : b ∈ B
this : 2 * ↑(#A) ≤ ↑(#(a •> A ∩ b •> A)) + ↑(#(B * A))
⊢ (2 - K) * ↑(#A) < ↑(#(a •> A ∩ b •> A))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ ∑ k ∈ m.toFinset, k * count k m = m.sum

Tactic:
Finset.sum_multiset_count

Goal state after:
case e_a
m : Multiset ℕ
⊢ ∑ k ∈ m.toFinset, k * count k m = ∑ m_1 ∈ m.toFinset, count m_1 m • m_1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.semilength = count D ↑p

Tactic:
← count_U_eq_count_D

Goal state after:
p : DyckWord
⊢ p.semilength = count U ↑p
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
⊢ (f • g) • h = f • g • h

Tactic:
by
    ext a b
    simp only [smul_apply, sum_smul, smul_sum, sum_sigma']
    apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;> aesop (add unsafe le_trans)

Goal state after: