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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
⊢ ↑(#s) * 1 ≤ ↑(#s') → ↑(#t) * 1 ≤ ↑(#t') → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1

Tactic:
hs

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * 1 ≤ ↑(#s')
⊢ ↑(#t) * 1 ≤ ↑(#t') → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
⊢ t.Nonempty

Tactic:
← card_pos,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
⊢ 0 < #t
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#((P.nonUniforms G ε).biUnion fun x ↦
          match x with
          | (U, V) => U ×ˢ V)) ≤
    ∑ i ∈ P.nonUniforms G ε, ↑(#i.1) * ↑(#i.2)

Tactic:
by
        norm_cast; simp_rw [← card_product]; exact card_biUnion_le

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
⊢ t.Nonempty

Tactic:
← card_pos,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
⊢ 0 < #t
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ (↑P.parts.offDiag.attach).Pairwise fun x y ↦
    ∀ ⦃a : Finset α × Finset α⦄,
      a.1 ∈ (chunk hP G ε ⋯).parts ∧ a.2 ∈ (chunk hP G ε ⋯).parts →
        ¬(a.1 ∈ (chunk hP G ε ⋯).parts ∧ a.2 ∈ (chunk hP G ε ⋯).parts)

Tactic:
rintro ⟨⟨s₁, s₂⟩, hs⟩ _ ⟨⟨t₁, t₂⟩, ht⟩ _ hst ⟨u, v⟩ huv₁ huv₂

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs : (s₁, s₂) ∈ P.parts.offDiag
a✝¹ : ⟨(s₁, s₂), hs⟩ ∈ ↑P.parts.offDiag.attach
t₁ t₂ : Finset α
ht : (t₁, t₂) ∈ P.parts.offDiag
a✝ : ⟨(t₁, t₂), ht⟩ ∈ ↑P.parts.offDiag.attach
hst : ⟨(s₁, s₂), hs⟩ ≠ ⟨(t₁, t₂), ht⟩
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : ↑s
⊢ (G.deleteIncidenceSet x).Adj ((Function.Embedding.subtype fun x ↦ x ∈ s) v₁)
      ((Function.Embedding.subtype fun x ↦ x ∈ s) v₂) ↔
    G.Adj ((Function.Embedding.subtype fun x ↦ x ∈ s) v₁) ((Function.Embedding.subtype fun x ↦ x ∈ s) v₂)

Tactic:
Function.Embedding.coe_subtype,

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : ↑s
⊢ (G.deleteIncidenceSet x).Adj ↑v₁ ↑v₂ ↔ G.Adj ↑v₁ ↑v₂
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝ : Fintype V
⊢ G.copyCount H = 0 ↔ H.Free G

Tactic:
by
  simp [copyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,
    filter_eq_empty_iff]

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

Goal state before:
pp: V : Type u_1
s t v w : V
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

Tactic:
by
  rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]

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
x✝¹ x✝ : V
⊢ Decidable ((edge s t).Adj x✝¹ x✝)

Tactic:
edge_adj

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ Decidable ((x✝¹ = s ∧ x✝ = t ∨ x✝¹ = t ∧ x✝ = s) ∧ x✝¹ ≠ x✝)
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
s x✝¹ x✝ : V
⊢ (edge s s).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
edge_adj

Goal state after:
V : Type u_1
s x✝¹ x✝ : V
⊢ (x✝¹ = s ∧ x✝ = s ∨ x✝¹ = s ∧ x✝ = s) ∧ x✝¹ ≠ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
h' : ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s

Tactic:
hs

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
h' : ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∈ s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e

Tactic:
by
  induction p <;> aesop

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
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
h : v ∈ (cons r p).support
⊢ G.Walk v w

Tactic:
exact cons r p

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
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
h : u ∈ (cons r p).support
hx : ¬v = u
⊢ u ∈ p.support

Tactic:
by
      cases h
      · exact (hx rfl).elim
      · assumption

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

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

Tactic:
grind [darts_append, IsSubwalk]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.Nil ↔ u = v

Tactic:
by
  refine ⟨fun ⟨⟩ ↦ rfl, ?_⟩
  rintro rfl
  exact isPath_iff_nil.mp 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.dropLast.edges = p.edges.dropLast

Tactic:
simp [dropLast, edges_take, List.dropLast_eq_take]

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
this : ∀ {p q : G.Walk u v}, (∀ (k : ℕ), p.getVert k = q.getVert k) → p.length ≤ q.length → p = q
hpq : ¬p.length ≤ q.length
⊢ p = q

Tactic:
exact (this (h · |>.symm) (le_of_not_ge hpq)).symm

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

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

Tactic:
hs

Goal state after:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ ↑{a, b} ⊆ s

Tactic:
push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩

Goal state after:
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
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ #{s(a, b), s(a, c), s(b, c)} = 3

Tactic:
refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩ <;> simp [hab.ne, hac.ne, hbc.ne]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
⊢ ∃ s, G.IsNIndepSet G.indepNum s

Tactic:
by
  simp_rw [indepNum, ← isNClique_compl]
  exact exists_isNClique_cliqueNum

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

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n % k < k * (n / k)

Tactic:
apply (mod_lt n hk).trans_le

Goal state after:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ k ≤ k * (n / k)
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
a : α
⊢ MulDissociated {a} ↔ a ≠ 1

Tactic:
by
  simp [MulDissociated, ofPred_or, -subset_singleton_iff,
    Finset.coe_subset_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

Tactic:
f,

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : ((a₁ * c₁, a₁ * b₁), b₁, c₁) = ((a₂ * c₂, a₂ * b₂), b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_2.refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ #s < 2 * p

Tactic:
hs

Goal state after:
case refine_2.refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ 2 * p - 1 < 2 * p
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Colex (Finset α)
⊢ s < t ↔ ∃ (h : s ≠ t), (ofColex s ∆ ofColex t).max' ⋯ ∈ ofColex t

Tactic:
rw [lt_iff_le_and_ne, le_iff_max'_mem]; aesop

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: 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)

Tactic:
rw [h𝒜.1 p, h𝒜.1 hs]
    exact ⟨rfl, le_sup' _ p⟩

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

Goal state before:
pp: case inr
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ v.cross w = w.cross v

Tactic:
· induction v with | h v hv =>
    induction w with | h w hw =>
    rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

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

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
let s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
⊢ Tendsto (fun n ↦ ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
⊢ (A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)).Nonempty

Tactic:
← card_pos,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
⊢ 0 < #(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
this : count U ↑p = count D ↑p
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑p)

Tactic:
rw [← take_append_drop i p.toList, count_append, count_append] at this

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
this : count U (List.take i ↑p) + count U (List.drop i ↑p) = count D (List.take i ↑p) + count D (List.drop i ↑p)
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (0 • f) a✝¹ b✝ = 0 a✝¹ b✝

Tactic:
exact sum_eq_zero fun x _ ↦ zero_smul _ _

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

Goal state before:
pp: case inr
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
a b : α
a✝ : a ≤ b
h : a ≠ b
⊢ ((algebraMap 𝕜 𝕝) (c * d) • 1) a b = ((algebraMap 𝕜 𝕝) c • 1 * (algebraMap 𝕜 𝕝) d • 1) a b

Tactic:
· simp only [one_apply, mul_one, smul_eq_mul, mul_apply, zero_mul,
            constSMul_apply, ← ite_and, ite_mul, mul_ite, map_mul, mul_zero, if_neg h]
          refine (sum_eq_zero fun x _ ↦ ?_).symm
          exact if_neg fun hx ↦ h <| hx.2.trans hx.1

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

Goal state before:
pp: case a
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 := ⋯
H : Subgroup G := ⋯
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 → ℕ := ⋯
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := ⋯
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
z : G
hz : z ∈ {z ∈ S | (K - 1) * ↑(#A) < ↑(r z)}
⊢ r z ≤ #A

Tactic:
exact convolution_le_card_left

Goal state after:
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 : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = 1
⊢ mu 𝕜 = mud

Tactic:
rw [← mu_mul_zeta] at this

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = mu 𝕜 * zeta 𝕜
⊢ mu 𝕜 = mud
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)
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x

Tactic:
have hsum := hsum 0

Goal state after:
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 ↦ powMulProdOneSubPow 0 x_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
⊢ ∏' (i : ℕ), (1 - X ^ ((i + 1) * m)) = (∏' (i : ℕ), ∑ j ∈ range m, X ^ ((i + 1) * j)) * ∏' (i : ℕ), (1 - X ^ (i + 1))

Tactic:
rw [← (multipliable_powerSeriesMk_card_countRestricted R m).tprod_mul
    (multipliable_one_sub_X_pow _)]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
⊢ ∏' (i : ℕ), (1 - X ^ ((i + 1) * m)) = ∏' (b : ℕ), (∑ j ∈ range m, X ^ ((b + 1) * j)) * (1 - X ^ (b + 1))
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 b : G
ha : a ∈ n⁻¹ •> ↑N
hb : b ∈ n⁻¹ •> ↑N
⊢ a * b ∈ n⁻¹ •> ↑N

Tactic:
rw [← coe_smul_finset, mem_coe] at *

Goal state after:
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 b : G
ha : a ∈ n⁻¹ •> N
hb : b ∈ n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
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 *

Goal state after:
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
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
by
  simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ vertexSet

Tactic:
← hvertexSet

Goal state after:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G)
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: case map_rel_iff'
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
⊢ ∀ {a b : ↑V(ofSimpleGraph G)},
    G.Adj ((Equiv.Set.univ α) a) ((Equiv.Set.univ α) b) ↔ (ofSimpleGraph G).toSimpleGraph.Adj a b

Tactic:
refine ⟨fun h ↦ ⟨fun h' ↦ h.ne (congrArg Subtype.val h'), ?_⟩, fun ⟨_, h⟩ ↦ ?_⟩ <;>
    revert h

Goal state after:
case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → (ofSimpleGraph G).Adj ↑a✝ ↑b✝

case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ (ofSimpleGraph G).Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)