mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ #(induce {x}ᶜ G).edgeFinset = #(G.deleteIncidenceSet x).edgeFinset

Tactic:
have h_notMem : x ∉ ({x}ᶜ : Set V) := Set.notMem_compl_iff.mpr (Set.mem_singleton x)
  simp_rw [edgeFinset, Set.toFinset_card,
    ← G.induce_deleteIncidenceSet_of_notMem h_notMem, ← Set.toFinset_card]
  apply card_edgeFinset_induce_of_support_subset
  trans G.support \ {x}
  · exact support_deleteIncidenceSet_subset G x
  · rw [Set.compl_eq_univ_sdiff]
    exact Set.sdiff_subset_sdiff_left (Set.subset_univ G.support)

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
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∈ G.edgeSet → x ∉ x✝ ↔ x ∉ x✝

Tactic:
Classical.imp_iff_right_iff

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.edgeSet ∨ x ∉ x✝
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:
by
  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.Regularity.Chunk

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m

Tactic:
· convert! card_parts_equitabilise_subset_le _ (card_aux₂ hP hU h₁) hB

Goal state after:
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:
simp [mem_edgeSet, killCopies_of_ne_bot hH, f, eq_comm]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
exact degree_of_notMem_verts hv

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 (G'.edgeSet ∩ s) = G'.deleteEdges s

Tactic:
by
  ext <;> simp +contextual

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.getVert 0 = u

Tactic:
cases w <;> rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s

Tactic:
by
  ext <;> simp +contextual

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s

Tactic:
by
  ext <;> simp +contextual

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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
⊢ { fst := u', snd := v', adj := h✝ } ∈ p.darts

Tactic:
have := h 0
    have := h 1
    convert! p.darts.getElem_mem (n := i) (by grind)
      <;> grind [fst_darts_getElem, snd_darts_getElem]

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

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

Tactic:
by
  intro p p' h
  induction p with
  | nil => cases p' <;> simp at h ⊢
  | cons _ _ ih =>
    cases p' with
    | nil => simp at h
    | cons _ _ =>
      simp only [map_cons, cons.injEq] at h
      grind

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
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.edges, e ∈ H.edgeSet

Tactic:
exact hp

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
⊢ p.support.dropLast ++ [v] = p.support

Tactic:
cases p with | nil => rfl | cons h p
  have ⟨_, _, _, hp⟩ := p.exists_cons_eq_concat h
  simp [hp]

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 v w
h : u ∈ p.support
⊢ (p.dropUntil u h).support <:+ p.support

Tactic:
dropUntil_eq_drop,

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ ((p.drop (List.idxOf u p.support)).copy ⋯ ⋯).support <:+ p.support
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 v w
h : u ∈ p.support
⊢ (p.dropUntil u h).darts <:+ p.darts

Tactic:
dropUntil_eq_drop,

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ ((p.drop (List.idxOf u p.support)).copy ⋯ ⋯).darts <:+ p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p₁ p₂ : G.Walk u v
h₁ : p₁.IsSubwalk p₂
h₂ : p₂.IsSubwalk p₁
⊢ p₁ = p₂

Tactic:
rw [isSubwalk_iff_support_isInfix] at h₁ h₂
  exact ext_support <| List.infix_antisymm h₁ h₂

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).IsPath → p.IsPath

Tactic:
simp only [isPath_def, support_append]
  exact List.Nodup.of_append_left

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

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

Tactic:
exact hy.resolve_left hyv

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
hp : ¬p.Nil
⊢ p.tail.length + 1 = p.length

Tactic:
rw [← length_cons (p.adj_snd hp), cons_tail_eq _ hp]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m

Tactic:
· simp only [Walk.getVert_cons _ _ hn0, Walk.getVert_cons _ _ hm0] at hnm
      have := ihp hp.of_cons (by lia : (n - 1) ≤ p.length)
        (by lia : (m - 1) ≤ p.length) hnm
      lia

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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49

Tactic:
add_le_add_iff_left

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ ε ^ 5 / 49 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 49
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ G.IsClique (⇑f ⁻¹' t)

pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ ⇑f '' ⇑f ⁻¹' t = t

Tactic:
· rintro x (hx : f x ∈ t) y (hy : f y ∈ t) hne
    obtain ⟨-, u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
    rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy
    rwa [← hux, ← hvy]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ ⇑f '' ⇑f ⁻¹' t = t
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e) G).LocallyLinear

Tactic:
← Equiv.coe_toEmbedding,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e.toEmbedding) G).LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u ↔ i = 0 ∨ i = p.length

Tactic:
by
  refine ⟨?_, by aesop⟩
  rw [or_iff_not_imp_left]
  intro h hi
  exact hpc.getVert_injOn (by simp only [Set.mem_ofPred_eq]; lia)
    (by simp only [Set.mem_ofPred_eq]; lia) (h.symm ▸ (Walk.getVert_length p).symm)

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

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

Tactic:
← edgeSet_eq_empty,

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G.edgeSet = ∅
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.EdgeDisjointTriangles
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset

Tactic:
← mul_one #G.edgeFinset

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1
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✝¹ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
inst✝ : DecidableRel H.Adj
hG : H ≤ G
⊢ H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
hH

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
inst✝ : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
⊢ ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) * (↑m + 1) * ((1 - (↑m)⁻¹) / (4 ^ #P.parts * ↑m)) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

Tactic:
rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts * ((↑m + 1) * ((1 - (↑m)⁻¹) / ↑m)) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ Eₘ[s] = 0 ↔ s = ∅

Tactic:
mulEnergy_eq_zero_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ s = ∅ ∨ s = ∅ ↔ s = ∅
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A B : Finset M
hB : B ⊆ A
hx : ∑ b ∈ B, b ∈ A.subsetSum
⊢ ∑ b ∈ B, b ∈ (A.erase 0).subsetSum

Tactic:
refine mem_subsetSum_iff.mpr ⟨B.erase 0, ?_, sum_erase _ (by simp)⟩

Goal state after:
M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A B : Finset M
hB : B ⊆ A
hx : ∑ b ∈ B, b ∈ A.subsetSum
⊢ B.erase 0 ⊆ A.erase 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
⊢ a ∈ s'

Tactic:
simp [s', has, hat]

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ (crossProduct v) w = -(crossProduct w) v

Tactic:
cross_anticomm

Goal state after:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ (crossProduct v) w = (crossProduct v) w
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)) →
    ∃ a ∈ ofColex (toColex t), a ∉ ofColex (toColex s) ∧ ∀ b ∈ ofColex (toColex s), b ∉ ofColex (toColex t) → b < a

Tactic:
· rintro ⟨w, hwt, hws, hw⟩
    refine ⟨w, hwt, hws, fun a has hat ↦ ?_⟩
    by_contra! hwa
    exact hat <| (hw <| hwa.lt_of_ne <| ne_of_mem_of_not_mem hwt hat).1 has

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
v : ℙ K V
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v

Tactic:
induction v using ind with | h v hv =>
  simp only [map_mk, mk_eq_mk_iff'] at h ⊢
  rcases h with ⟨a, ha⟩
  refine ⟨τ a, hf ?_⟩
  rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]

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

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑↑(numDerangements n) / ↑n.factorial = s (n + 1)

Tactic:
numDerangements_sum

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))) / ↑n.factorial = s (n + 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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
⊢ lineCount L p = pointCount P l

Tactic:
obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
    let s : Finset (P × L) := Set.toFinset { i | i.1 ∈ i.2 }
    have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 := by
      rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
      simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
    have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 := by
      rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
      on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
      all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
    have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
      rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
    rw [← Set.toFinset_compl] at step3
    exact
      ((Finset.sum_eq_sum_iff_of_le fun i hi =>
              HasLines.pointCount_le_lineCount (by exact Set.mem_toFinset.mp hi)).mp
          step3.symm (p, l) (Set.mem_toFinset.mpr hpl)).symm

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1) =
    (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !

Tactic:
rw [bell_mul_eq_lemma hx]

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !
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✝¹ : AddGroup 𝕜
inst✝ : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (-⇑f) a b = 0

Tactic:
Pi.neg_apply,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ -f a b = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a

Tactic:
by
  let : DecidableLE α := Classical.decRel _
  let mud : IncidenceAlgebra 𝕜 αᵒᵈ :=
    { toFun := fun a b ↦ mu 𝕜 (ofDual b) (ofDual a)
      eq_zero_of_not_le' := fun a b hab ↦ apply_eq_zero_of_not_le (by exact hab) _ }
  suffices mu 𝕜 = mud by simp_rw [this, mud, coe_mk, ofDual_toDual]
  suffices mud * zeta 𝕜 = 1 by
    rw [← mu_mul_zeta] at this
    apply_fun (· * mu 𝕜) at this
    symm
    simpa [mul_assoc, zeta_mul_mu] using this
  clear a b
  ext a b
  simp only [mul_boole, one_apply, mul_apply, zeta_apply]
  calc
    ∑ x ∈ Icc a b, (if x ≤ b then mud a x else 0) = ∑ x ∈ Icc a b, mud a x := by
      congr! with x hx; exact if_pos (mem_Icc.1 hx).2
    _ = ∑ x ∈ Icc (ofDual b) (ofDual a), mu 𝕜 x (ofDual a) := by simp [Icc_orderDual_def, mud]
    _ = if ofDual b = ofDual a then 1 else 0 := sum_Icc_mu_left ..
    _ = if a = b then 1 else 0 := by simp [eq_comm]

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

Goal state before:
pp: p : DyckWord
h✝ : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

pp: p : DyckWord
h✝ : ¬p = 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
exacts [semilength_insidePart_lt ‹_›, semilength_outsidePart_lt ‹_›]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ Multipliable fun x_1 ↦ 1 - x ^ (x_1 + 1)

Tactic:
by simpa using h 0

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha : a ∈ n⁻¹ •> ↑N
⊢ a⁻¹ ∈ n⁻¹ •> ↑N

Tactic:
rw [← coe_smul_finset, mem_coe] at *
      apply smul_mem_smul_finset (a := a⁻¹) at ha
      rw [smul_eq_mul, inv_mul_cancel] at ha
      have : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty := ⟨1, by simpa using! ⟨one_mem_carrier, ha⟩⟩
      simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a⁻¹) this] using! self_mem_smul_carrier a⁻¹

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.succ
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
specialize ihα ((ι → Option α) → κ)

Goal state after:
case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
ihα : ∃ ι_1 x, ∀ (C : (ι_1 → α) → (ι → Option α) → κ), ∃ l, IsMono C l
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l