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

Goal state before:
pp: case refine_3
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts

pp: case refine_4
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w

Tactic:
· simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
    rintro w hw rfl
    exact h.1 hw

Goal state after:
case refine_4
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i

Tactic:
have hunion :
    (P.equitabilise h).parts =
      {u ∈ (P.equitabilise h).parts | #u = m} ∪ {u ∈ (P.equitabilise h).parts | #u = m + 1} := by
    rw [← filter_or, filter_true_of_mem]
    exact fun x => card_eq_of_mem_parts_equitabilise

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion : (equitabilise h).parts = {u ∈ (equitabilise h).parts | #u = m} ∪ {u ∈ (equitabilise h).parts | #u = m + 1}
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ → G'.Adj x✝¹ x✝

Tactic:
simp +contextual only [induce_adj, imp_true_iff, and_true]

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

Goal state before:
pp: case Adj.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → (G'.induce G'.verts).Adj x✝¹ x✝

Tactic:
simp +contextual only [induce_adj, imp_true_iff, and_true]

Goal state after:
case Adj.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v' : V
p : G.Walk v' v
hwp : w ∈ p.support
h : u ≠ w
hadj : G.Adj u v'
⊢ (cons hadj p).takeUntil w ⋯ = cons hadj (p.takeUntil w hwp)

Tactic:
by
  simp [Walk.takeUntil, h]

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

Goal state before:
pp: case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
⊢ (if hx : u✝ = u then hx ▸ nil else cons h✝ (p✝.takeUntil u ⋯)).append
      (if hx : u✝ = u then Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) hx ⋯
      else p✝.dropUntil u ⋯) =
    cons h✝ p✝

Tactic:
split_ifs with h' <;> subst_vars

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u✝ ∈ p✝.support), (p✝.takeUntil u✝ h).append (p✝.dropUntil u✝ h) = p✝
a✝ : List.Mem u✝ p✝.support
⊢ (⋯ ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) ⋯ ⋯) =
    cons h✝ p✝

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝
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).IsTrail ↔ p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges

Tactic:
simp [Walk.isTrail_def, List.nodup_append']

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsCycle
⊢ p.reverse.IsCycle

Tactic:
by
  simp only [Walk.isCycle_def, nodup_tail_support_reverse] at h ⊢
  exact ⟨h.1.reverse, fun h' ↦ h.2.1 (by simp_all [← Walk.length_eq_zero_iff]), h.2.2⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (SimpleGraph.map (⇑f) G).EdgeDisjointTriangles

Tactic:
EdgeDisjointTriangles,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ ((SimpleGraph.map (⇑f) G).cliqueSet 3).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False

Tactic:
p.getVert_of_length_le (by lia : p.length ≤ i + 1),

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = u
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
h : ∀ (t : Finset ↑s), ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)
t : Finset α
ht : ↑t ⊆ s
this : ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) (Finset.subtype (fun x ↦ x ∈ s) t))
⊢ ¬G.IsNClique n t

Tactic:
← filter_eq_self.mpr ht,

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
h : ∀ (t : Finset ↑s), ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)
t : Finset α
ht : ↑t ⊆ s
this : ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) (Finset.subtype (fun x ↦ x ∈ s) t))
⊢ ¬G.IsNClique n (filter (Membership.mem s) t)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
⊢ s ∈ map f '' G.cliqueSet #s

Tactic:
have hs' : (s.preimage f f.injective.injOn).map f = s := by
      classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ s ∈ map f '' G.cliqueSet #s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.support <+ p.support ++ q.support.reverse.tail

Tactic:
use u', hp'.support_subset p'.start_mem_support, hq'.support_subset q'.start_mem_support

Goal state after:
case right
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ ∃ c, c.IsCycle ∧ c.support <+ p.support ++ q.support.reverse.tail
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✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H ↦ H.CliqueFree 3) (G.deleteEdges ∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#∅)
⊢ ε ≤ 0

Tactic:
Finset.card_empty,

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H ↦ H.CliqueFree 3) (G.deleteEdges ∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑0
⊢ ε ≤ 0
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ Int.subNatNat (2 * #G.edgeFinset) (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (#{x | G.Adj x.1 x.2}) #{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}

Tactic:
two_mul_card_edgeFinset,

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ Int.subNatNat
      (#{x |
          match x with
          | (x, y) => G.Adj x y})
      (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (#{x | G.Adj x.1 x.2}) #{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ (graph (triangleIndices A)).FarFromTriangleFree (ε / 9)

Tactic:
refine farFromTriangleFree _ ?_

Goal state after:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε / 9 * ↑((Fintype.card G + Fintype.card G + Fintype.card G) ^ 2) ≤ ↑(#(triangleIndices A))
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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 3 / 4 * ε ≤
    |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
          (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U))) -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts|

Tactic:
show (16 : ℝ) = ↑4 ^ 2 by norm_num,

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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 3 / 4 * ε ≤
    |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
          (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U))) -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
          (4 ^ 2) ^ #P.parts|
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₂
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
⊢ ε ^ 4 / 3 ≤ ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2

Tactic:
show (16 : ℝ) = ↑4 ^ 2 by norm_num,

Goal state after:
case h₂
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
⊢ ε ^ 4 / 3 ≤ ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / (4 ^ 2) ^ #P.parts * (9 / 4 ^ 2) * ε ^ 2
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₁ s a).totalDegree + (f₂ s a).totalDegree ≤ p - 1 + (p - 1)

Tactic:
gcongr <;> apply totalDegree_finsetSum_le <;> rintro i _
      · exact (totalDegree_X_pow ..).le
      · exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le

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

Goal state before:
pp: case refine_1
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ 3 / 4 * ε ≤
    |(∑ i ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((star hP G ε hU V).product (star hP G ε hV U))) -
        (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts))|

pp: case refine_2
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
        ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts))) ^
      2

Tactic:
· simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow]
        simpa using edgeDensity_star_not_uniform hPα hPε hε₁ hUVne hUV

Goal state after:
case refine_2
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
        ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts))) ^
      2
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
⊢ #A + 1 + #A.subsetSum = #(insert 0 A) + #A.subsetSum

Tactic:
rw [card_insert_of_notMem fun h => (hA 0 h).false]

Goal state after:
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.attach < 2 * p

Tactic:
card_attach,

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
⊢ #s < 2 * p
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
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ K ∙ ↑v = H

Tactic:
SetLike.ext'_iff,

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ ↑(K ∙ ↑v) = ↑H
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
this : ∑ p, lineCount L p < ∑ p, lineCount L p
⊢ False

Tactic:
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
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
by
    simp_rw [this]
    -- shift the function by 1, and then use the fact that the partial sums
    -- converge to the infinite sum
    rw [tendsto_add_atTop_iff_nat
      (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
    apply HasSum.tendsto_sum_nat
    -- there's no specific lemma for ℝ that ∑ x^k/k! sums to exp(x), but it's
    -- true in more general fields, so use that lemma
    rw [Real.exp_eq_exp_ℝ]
    exact expSeries_div_hasSum_exp (-1 : ℝ)

Goal state after:
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
⊢ ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ i ∈ s, pointCount P i.2

pp: case h
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
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset

Tactic:
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]

Goal state after:
case h
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
⊢ ∀ (p : P × L), p ∈ s ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset

case h
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
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A * #A)

Tactic:
← card_product,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#(A ×ˢ A))
Module: Mathlib.Combinatorics.Configuration

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

Tactic:
by
  induction a with | h a ha =>
  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.Catalan.Basic

Goal state before:
pp: n : ℕ
this : ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
have h := Nat.succ_dvd_centralBinom n

Goal state after:
n : ℕ
this : ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
h : n + 1 ∣ n.centralBinom
⊢ catalan n = n.centralBinom / (n + 1)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ∃ p₁ p₂ p₃ l₁ l₂ l₃, p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃

Tactic:
by
      refine ⟨mk K ![0, 1, 1] ?_, mk K ![1, 0, 0] ?_, mk K ![1, 0, 1] ?_, mk K ![1, 0, 0] ?_,
        mk K ![0, 1, 0] ?_, mk K ![0, 0, 1] ?_, ?_⟩ <;> simp [mem_iff, orthogonal_mk]

Goal state after: