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

Goal state before:
pp: case inr
α : 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
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
have htα : t ≤ #(univ : Finset α) :=
    (initialBound_le_bound _ _).trans (by rwa [Finset.card_univ])

Goal state after:
case inr
α : 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
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
⊢ G.degree v ≤ (induce s G).maxDegree

Tactic:
by_cases hv : G.IsIsolated v

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
hv : G.IsIsolated v
⊢ G.degree v ≤ (induce s G).maxDegree

case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
hv : ¬G.IsIsolated v
⊢ G.degree v ≤ (induce s G).maxDegree
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A ≠ ⊥
⊢ A.Free ⊥

Tactic:
← edgeSet_nonempty

Goal state after:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
⊢ A.Free ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
t : Finset V
ht : ↑t = G.neighborSet v
h : ↑↑t ≃ ↑↑s
⊢ H.neighborSet v ⊆ ↑t

Tactic:
ht

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
t : Finset V
ht : ↑t = G.neighborSet v
h : ↑↑t ≃ ↑↑s
⊢ H.neighborSet v ⊆ G.neighborSet v
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 2 ^ #P.parts * ε ^ 2 / 10 = 2 ^ #P.parts * (ε * (ε / 10))

Tactic:
by rw [mul_div_assoc, sq, mul_div_assoc]

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 : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑(#s) * (↑m / (↑m + 1)) ≤ ↑(#(𝒜.sup id))

Tactic:
rw [mul_div_assoc', div_le_iff₀ coe_m_add_one_pos, mul_right_comm]

Goal state after:
α : 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
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m * ↑(#s) ≤ ↑(#(𝒜.sup id)) * (↑m + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).support = p.support ++ [w]

Tactic:
by
  induction p <;> simp [*, concat_nil]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).darts = p.darts.concat { fst := v, snd := w, adj := h }

Tactic:
by
  induction p <;> simp [*, concat_nil]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
this : p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
⊢ False

Tactic:
have := dropLast_support_concat _ ▸ p.count_support_takeUntil_eq_one h

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
this✝ : p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
this : List.count (p.getVert n) ((p.takeUntil (p.getVert n) h).support.dropLast ++ [p.getVert n]) = 1
⊢ False
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
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.support[k]? = none
ht : q.support[k]? = none
⊢ none = q.support[k]?

Tactic:
ht

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.support[k]? = none
ht : q.support[k]? = none
⊢ none = none
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:
· rw [← Equiv.coe_toEmbedding, ← map_symm]
    exact LocallyLinear.map _

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
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
⊢ ∀ (a b : Finset α),
    a ∈ A →
      b ∈ B →
        ↑(#(interedges G.Adj a b)) / (↑(#a) * ↑(#b) * (↑(#A) * ↑(#B))) ≤
          ↑(#(interedges G.Adj a b)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))

Tactic:
intro x y hx hy

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
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
⊢ ↑(#(interedges G.Adj x y)) / (↑(#x) * ↑(#y) * (↑(#A) * ↑(#B))) ≤
    ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hab : a = b <;> by_cases hbc : b = c

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
⊢ ¬⊥.IsNClique n t

Tactic:
ht

Goal state after:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : ⊥.IsNClique n t
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).LocallyLinear

Tactic:
classical
  refine ⟨?_, fun x y hxy ↦ ?_⟩
  · unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]
  · obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
    exact ⟨_, toTriangle_is3Clique hz, hxy⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A, B⁻¹] = δₘ[A, B]

Tactic:
mulConst,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#(A * B⁻¹)) / ↑(#A) = δₘ[A, B]
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A, B⁻¹] = σₘ[A, B]

Tactic:
mulConst,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A, B⁻¹] = ↑(#(A * B)) / ↑(#A)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 ≤ σₘ[A, B]

Tactic:
mulConst,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 ≤ ↑(#(A * B)) / ↑(#A)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ σₘ[A, B] ≤ ↑(#B)

Tactic:
mulConst,

Goal state after:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * B)) / ↑(#A) ≤ ↑(#B)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A⁻¹, B] = δₘ[A, B]

Tactic:
mulConst,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#(A⁻¹ * B)) / ↑(#A⁻¹) = δₘ[A, B]
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A⁻¹, B] = σₘ[A, B]

Tactic:
mulConst,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A⁻¹, B] = ↑(#(A * B)) / ↑(#A)
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:

Tactic:
_ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia

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}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
h : (∀ a ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, (starRingEnd ℂ) (d a) ≠ 0
⊢ t \ u ∈ {t | ↑t ⊆ {ψ | d ψ ≠ 0}}

Tactic:
by simpa only [map_ne_zero] using! h.2

Goal state after:
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ (Fintype.card α).choose r

Tactic:
Fintype.card,

Goal state after:
α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ (#univ).choose r
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| v.submodule

Tactic:
rw [← v.mk_rep]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| (mk K v.rep ⋯).submodule
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K ↥v.submodule

Tactic:
rw [← v.mk_rep]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K ↥(mk K v.rep ⋯).submodule
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ #s - 1 ≤ #(t.erase m)

Tactic:
card_erase_of_mem (min'_mem _ _)

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ #s - 1 ≤ #t - 1
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v w : ℙ F (m → F)
⊢ v.orthogonal w ↔ w.orthogonal v

Tactic:
induction v with

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬v.orthogonal w

Tactic:
induction v with

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬v.orthogonal w

Tactic:
exact exists_not_self_orthogonal v

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

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

Tactic:
induction v with

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

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

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

Tactic:
induction v with

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∈ fixedPoints ⇑f ↔ fixedPoints ⇑f = {a}

Tactic:
rw [Set.eq_singleton_iff_unique_mem, and_comm]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ a ∈ fixedPoints ⇑f ∧ fixedPoints ⇑f ⊆ {a} ↔ a ∈ fixedPoints ⇑f ∧ ∀ x ∈ fixedPoints ⇑f, x = a
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
⊢ Fintype.card P ≤ Fintype.card L

Tactic:
classical
  by_contra hc₂
  obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
  have :=
    calc
      ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
      _ ≤ ∑ l, lineCount L (f l) :=
        (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
      _ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
      _ < ∑ p, lineCount L p := by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · 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⟩⟩
  exact lt_irrefl _ this

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:
rw [← Int.cast_natCast, 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✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
l : L
x✝ : l ∈ univ
⊢ pointCount P l • lineCount L (f l) = lineCount L (f l) • lineCount L (f l)

Tactic:
rw [hf2]

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

Goal state before:
pp: case neg
m : Multiset ℕ
this :
  (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
hm : 0 ∉ m.toFinset
⊢ (∏ 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:
· 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.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

Tactic:
rw! [← p.cons_tail_dropLast_concat h]
    simp

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
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun x_1 ↦ aux k x_1 x) atTop (𝓝 0)

Tactic:
rw [show 𝓝 0 = 𝓝 (0 * (0 - 1) * ∏' i, (1 - x ^ (k + i + 2))) by simp]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun x_1 ↦ aux k x_1 x) atTop (𝓝 (0 * (0 - 1) * ∏' (i : ℕ), (1 - x ^ (k + i + 2))))
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingFirst 1 = n !

Tactic:
by
  induction n with
  | zero => rfl
  | succ n hn =>
    rw [stirlingFirst_succ_succ, zero_add, hn, stirlingFirst_succ_zero]
    simp [Nat.factorial_succ]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
n : ℕ
hn : n ∉ Set.range pentagonal
⊢ C ((coeff n) (pentagonalSeries R)) * X ^ n = 0

Tactic:
by simp [coeff_pentagonalSeries_eq_zero R hn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e✝ : β
G✝ H : Graph α β
F F₀ : Set β
X : Set α
G : Graph α β
E₀ : Set β
e : β
h : e ∈ E(G) ∩ E₀
⊢ ∃ x y, e ∈ E₀ ∧ G.IsLink e x y

Tactic:
by simp [G.exists_isLink_of_mem_edgeSet h.1, h.2]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ G₁.IsLink e x y ↔ G₂.IsLink f x y

Tactic:
rw [isLink_iff_inc, isLink_iff_inc, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
inst✝ : G.Loopless
e : β
he : e ∈ E(G)
x y : α
hxy : G.IsLink e x y
⊢ V(G).Nontrivial

Tactic:
exact ⟨x, hxy.left_mem, y, hxy.right_mem, hxy.adj.ne⟩

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

Goal state before:
pp: α : Type u_1
H : Hypergraph α
h : H.IsTrivial
⊢ H.IsNonempty

Tactic:
by
  grind [IsNonempty, IsTrivial, Set.nonempty_iff_ne_empty]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.head'
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ (Stream'.corec elem succ p).head ∈ ↑p

Tactic:
rw [Stream'.corec_eq, Stream'.head_cons]

Goal state after:
case h.head'
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ elem p ∈ ↑p
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h :=
      Nat.succ_le_of_lt (Finset.min'_lt_of_mem_erase_min' _ _ <| Finset.min'_mem _ _)

Goal state after:
case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hsn : #s ≤ ↑n
⊢ (fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s))
      ((fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩)) n) =
    n

Tactic:
· simp [hsn.not_gt, hsn, mem_compl.1 <| Subtype.prop _]

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
⊢ ¬f.IsPrefix t

Tactic:
ht

Goal state after:
X : Type u_1
inst✝¹ : Fintype X
s t : Finset X
inst✝ : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
⊢ False