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

Goal state before:
pp: case mpr.refine_1
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

Tactic:
simp [*]

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

Goal state before:
pp: case mpr.refine_2
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj d e ∧ G.Adj d f ∧ G.Adj e f ∧ {d, e, f} = {d, e, f}

Tactic:
simp [*]

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

Goal state before:
pp: case ha
α : 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
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ A, (id x).Nonempty

pp: case hb
α : 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
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ B, (id x).Nonempty

Tactic:
· exact ⟨_, hx, nonempty_of_mem_parts _ (hA hx)⟩

Goal state after:
case hb
α : 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
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ B, (id x).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
q : G.Walk u u
qc : q.IsCycle
hq : ∀ e ∈ q.edges, e ∈ H.edgeSet
⊢ (q.transfer H hq).IsCycle

Tactic:
cases q with

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h : (graph t).IsNClique 3 s
⊢ ∃ x ∈ t, toTriangle x = s

Tactic:
rw [is3Clique_iff] at h

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h : ∃ a b c, (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}
⊢ ∃ x ∈ t, toTriangle x = s
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
⊢ (graph t).IsNClique 3 s ↔ ∃ x ∈ t, toTriangle x = s

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [is3Clique_iff] at h
    obtain ⟨x, y, z, hxy, hxz, hyz, rfl⟩ := h
    obtain ⟨a, b, c, habc, hab, hac, hbc⟩ := graph_triple hxy hxz hyz
    refine ⟨(a, b, c), ?_, habc⟩
    obtain ⟨c', hc'⟩ := in₀₁_iff.1 hab
    obtain ⟨b', hb'⟩ := in₀₂_iff.1 hac
    obtain ⟨a', ha'⟩ := in₁₂_iff.1 hbc
    obtain rfl | rfl | rfl := NoAccidental.eq_or_eq_or_eq ha' hb' hc' <;> assumption
  · rintro ⟨x, hx, rfl⟩
    exact toTriangle_is3Clique hx

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
⊢ Pi.single a 1 a = -1 ∨ Pi.single a 1 a = 0 ∨ Pi.single a 1 a = 1

Tactic:
simp [*]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
hab : a ≠ b
⊢ Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∈ t
h✝ : a ∈ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∈ t
h✝ : a ∉ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∉ t
h✝ : a ∈ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h✝¹ : a ∉ t
h✝ : a ∉ u
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
⊢ a ∈ s'.mulSpan

Tactic:
by_cases ha' : a ∈ s'

Goal state after:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∈ s'
⊢ a ∈ s'.mulSpan

case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
⊢ a ∈ s'.mulSpan
Module: Mathlib.Combinatorics.Additive.Randomisation

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) = 𝔼 i, ∏ x, (↑(c x) + (d x * x i + (starRingEnd ℂ) (d x * x i)) / 2)

Tactic:
Complex.re_eq_add_conj

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) =
    ∑ t, (𝔼 a, ∏ ψ ∈ t, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, ↑(c ψ)

Tactic:
simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x : ℕ
hx : x ∈ L
⊢ x - (a + 1) + (a + 1) = x

Tactic:
rw [tsub_add_cancel_of_le (haL _ hx)]

Goal state after:
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Set α) → s.Finite → (a : ↑s) → β ↑a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ t, ∃ (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g ↑t ⋯ (inclusion hst x)
s : Set α
hs : s.Finite
t : Finset α
ht : hs.toFinset ⊆ t
hst : ∀ (x : ↥hs.toFinset), χ ↑x = g ↑t ⋯ (inclusion ht x)
⊢ ∃ t, ∃ (ht : t.Finite) (hst : s ⊆ t), ∀ (x : ↑s), χ ↑x = g t ht (inclusion hst x)

Tactic:
simp only [Set.Finite.toFinset_subset] at ht

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Set α) → s.Finite → (a : ↑s) → β ↑a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ t, ∃ (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g ↑t ⋯ (inclusion hst x)
s : Set α
hs : s.Finite
t : Finset α
ht✝ : hs.toFinset ⊆ t
hst : ∀ (x : ↥hs.toFinset), χ ↑x = g ↑t ⋯ (inclusion ht✝ x)
ht : s ⊆ ↑t
⊢ ∃ t, ∃ (ht : t.Finite) (hst : s ⊆ t), ∀ (x : ↑s), χ ↑x = g t ht (inclusion hst x)
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ 2 * ?m.31 - 1 ≤ #s.toEnumFinset

Tactic:
by simpa using hs

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

Goal state before:
pp: n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ 2 * n - 1 ≤ #s.toEnumFinset

Tactic:
by simpa using hs

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ t ∈ 𝒜 ↔ #(𝒜.sup' h𝒜₀ ⇑toColex) = #t ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)

Tactic:
refine ⟨fun p ↦ ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ #(𝒜.sup' h𝒜₀ ⇑toColex) = #t ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)

case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
⊢ #(𝒜.sup' h𝒜₀ ⇑toColex) = #t ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex) → t ∈ 𝒜
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
ha : p a
hfa :
  ↑({ toFun := fun f ↦ ⟨Perm.ofSubtype f, ⋯⟩, invFun := fun f ↦ (↑f).subtypePerm ⋯, left_inv := ⋯, right_inv := ⋯ } f)
      a =
    a
⊢ ↑(f ⟨a, ha⟩) = ↑⟨a, ha⟩

Tactic:
Equiv.coe_fn_mk,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
ha : p a
hfa : (Perm.ofSubtype f) a = a
⊢ ↑(f ⟨a, ha⟩) = ↑⟨a, ha⟩
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) → f ∈ {f | fixedPoints ⇑f ⊆ {a}}

Tactic:
rw [RemoveNone.mem_fiber]
    rintro ⟨F, F_derangement, F_none, rfl⟩ x x_fixed
    rw [mem_fixedPoints_iff] at x_fixed
    apply_fun some at x_fixed
    rcases Fx : F (some x) with - | y
    · rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
    · exfalso
      rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
      exact F_derangement _ x_fixed

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

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ↑(numDerangements (n + 1)) = ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n + 1 - k))

Tactic:
rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ∀ x ∈ Finset.range (n + 1),
    (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))
Module: Mathlib.Combinatorics.Configuration

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

Tactic:
refine tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)

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

Goal state before:
pp: case h
K : Type u_3
inst✝ : Field K
b c d : ℙ K (Fin 3 → K)
hbc : b.orthogonal c
hbd : b.orthogonal d
a : Fin 3 → K
ha : a ≠ 0
hac : (Projectivization.mk K a ha).orthogonal c
had : (Projectivization.mk K a ha).orthogonal d
⊢ Projectivization.mk K a ha = b ∨ c = d

Tactic:
induction b with | h b hb =>
  induction c with | h c hc =>
  induction d with | h d hd =>
  rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
  exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

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

Goal state before:
pp: m : Multiset ℕ
this : ?m.115
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
by
      by_cases hm : 0 ∈ m.toFinset
      · rw [← Finset.prod_erase_mul _ _ hm]
        rw [← Finset.prod_erase_mul _ _ hm]
        simp only [factorial_zero, one_pow, mul_one, zero_mul]
        exact this
      · nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]
        nth_rewrite 3 [← Finset.erase_eq_of_notMem hm]
        exact this

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

Goal state before:
pp: m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0

Tactic:
rw [← Nat.pos_iff_ne_zero]

Goal state after:
m : Multiset ℕ
⊢ 0 < (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
A : Finset G
⊢ ∃ Z ⊆ A, ↑H * ↑Z = ↑H * ↑A ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z

Tactic:
by
  obtain ⟨Z, hZA, hZinj, hHZA⟩ :=
    ((A : Set G).surjOn_image ((H : Set G) <• ·)).exists_subset_injOn_image_eq
  lift Z to Finset G using A.finite_toSet.subset hZA
  refine ⟨Z, mod_cast hZA, ?_, hZinj⟩
  simpa [-SetLike.mem_coe, Set.iUnion_op_smul_set] using congr(Set.sUnion $hHZA)

Goal state after:
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
hq :
  (a ::ₘ m).bell * (map (fun j ↦ j !) (a ::ₘ m)).prod * ∏ j ∈ (a ::ₘ m).toFinset.erase 0, (count j (a ::ₘ m))! =
    (a ::ₘ m).sum !
⊢ a ∈ (a ::ₘ m).toFinset.erase 0

Tactic:
simp [*]

Goal state after:
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✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (1 * f) a✝¹ b✝ = f a✝¹ b✝

Tactic:
simp [*]

Goal state after:
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✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f * 1) a✝¹ b✝ = f a✝¹ b✝

Tactic:
simp [*]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(#(Icc a b))

Tactic:
rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
  refine sum_congr rfl fun x hx ↦ ?_
  rw [mem_Icc] at hx
  rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a : α
⊢ (mu 𝕜) a a = 1

Tactic:
simp [mu_apply]

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

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ (if p = 0 then BinaryTree.nil else node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.semilength

Tactic:
simp_rw [h, ite_false, numNodes]

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 = p.semilength
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: k : ℤ
⊢ ↑(pentagonal k) = k * (3 * k - 1) / 2

Tactic:
rcases k with (_ | _) | _ <;> grind [pentagonal_def]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ (coeff d) (∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))) =
    (coeff d) (genFun f)

Tactic:
rw [coeff_genFun, coeff_prod]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ ∑ l ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
      ∏ i ∈ Finset.map (addRightEmbedding 1) s, (coeff (l i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) =
    ∑ p, (Multiset.toFinsupp p.parts).prod f
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
⊢ 0 ≤ connectivity K S

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ Fintype.card α * addRothNumber (Iio ⟨n, ⋯⟩) ≤ Fintype.card α * addRothNumber univ

Tactic:
gcongr; exact subset_univ _

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case refine_3
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop ((fun n ↦ -4 * √(Real.log ↑n)) - fun n ↦ -4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
refine ⟨0, ?_⟩

Goal state after:
case refine_3
⊢ ∀ᶠ (x : ℝ) in Filter.map ((fun n ↦ -4 * √(Real.log ↑n)) - fun n ↦ -4 * √(Real.log ↑((n - 3) / 6))) atTop,
    (fun x1 x2 ↦ x1 ≤ x2) x 0
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : x ∈ V(H) → y ∈ V(H)
tfae_2_to_3 : y ∈ V(H) → e ∈ E(H)
⊢ [x ∈ V(H), y ∈ V(H), e ∈ E(H)].TFAE

Tactic:
tfae_have 3 → 1 := (he.anti_of_mem hHG.le · |>.left_mem)

Goal state after:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : x ∈ V(H) → y ∈ V(H)
tfae_2_to_3 : y ∈ V(H) → e ∈ E(H)
tfae_3_to_1 : e ∈ E(H) → x ∈ V(H)
⊢ [x ∈ V(H), y ∈ V(H), e ∈ E(H)].TFAE
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
y z : α
e : β
G : Graph α β
h : G.IsLink e y y
h' : G.IsLink e y z
⊢ y = z

Tactic:
obtain rfl | rfl := h'.right_eq_or_eq h.symm <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ ¬G ≠ ⊥ ↔ ¬V(G).Nonempty

Tactic:
simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ ¬V(G).Nonempty ↔ G = ⊥

Tactic:
simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G✝ H✝ G H : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄,
    { vertexSet := V(G) ∩ V(H), IsLink := fun e x y ↦ G.IsLink e x y ∧ H.IsLink e x y,
            edgeSet := {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}, isLink_symm := ⋯,
            eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }.IsLink
        e x y →
      G.IsLink e x y

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G✝ H✝ G H : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄,
    { vertexSet := V(G) ∩ V(H), IsLink := fun e x y ↦ G.IsLink e x y ∧ H.IsLink e x y,
            edgeSet := {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}, isLink_symm := ⋯,
            eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }.IsLink
        e x y →
      H.IsLink e x y

Tactic:
by simp +contextual

Goal state after: