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

Goal state before:
pp: case inr.calc_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
e : Sym2 V
⊢ e ∈ G.edgeFinset \ (Set.range f).toFinset ↔ e ∈ (G.killCopies H).edgeFinset

Tactic:
induction e using Sym2.inductionOn with | hf v w
   =>  _ 

Goal state after:
case inr.calc_2.hf
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
v w : V
⊢ s(v, w) ∈ G.edgeFinset \ (Set.range f).toFinset ↔ s(v, w) ∈ (G.killCopies H).edgeFinset
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
⊢ 0 ≤ ε

Tactic:
by sz_positivity

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ ↑m ≠ 0

Tactic:
by sz_positivity

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 0 < 100 / ε ^ 5

Tactic:
by sz_positivity

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
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
⊢ 0 ≤ ε ^ 5 / 50

Tactic:
by sz_positivity

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (∃ q r, p = q.append r) → w ∈ p.support

Tactic:
rintro ⟨q, r, rfl⟩
    simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]

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

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

Tactic:
simp [nil_iff_support_eq.mp hq, hyv] at hy

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
n m : ℕ
⊢ (p.take n).take m = (p.take (min n m)).copy ⋯ ⋯

Tactic:
by
  apply ext_support
  simp [support_take, List.take_take, Nat.min_left_comm]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
t u v u✝ : V
h : G.Adj u✝ t
⊢ (nil.concat h).dropLast = nil.copy ⋯ ⋯

pp: case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ((cons h✝ p✝).concat h).dropLast = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
· rfl

Goal state after:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ((cons h✝ p✝).concat h).dropLast = (cons h✝ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : G.Adj p.penultimate v
⊢ p.dropLast.concat hp = p

Tactic:
by
  induction p with
  | nil => simp at hp
  | cons hadj p hind =>
    cases p with
    | nil => rfl
    | _ => simp [hind]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : w = u
h' : ¬i ≤ p.length
⊢ i = 0

Tactic:
subst h

Goal state after:
case neg
V : Type u
G : SimpleGraph V
w : V
i : ℕ
p : G.Walk w w
hp : p.IsPath
h : ¬p.Nil
h' : ¬i ≤ p.length
⊢ i = 0
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
⊢ 0 ≤ ε ^ 5 / 49

Tactic:
by sz_positivity

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ G.IsClique (Subtype.val '' A)

Tactic:
simp only [Set.Pairwise, Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]

Goal state after:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ ∀ ⦃x : α⦄, (∃ (x_1 : x ∈ F), ⟨x, ⋯⟩ ∈ A) → ∀ ⦃y : α⦄, (∃ (x : y ∈ F), ⟨y, ⋯⟩ ∈ A) → x ≠ y → G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝ : β
h : f w✝ = x✝
y✝ : α
⊢ y✝ ∈ Set.range ⇑f → x✝ ≠ y✝ → G.Adj x✝ y✝

Tactic:
⟨_, h'⟩

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
⊢ x✝ ≠ y✝ → G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : f.topEmbedding w✝¹ ≠ f.topEmbedding w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)

Tactic:
rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne,
    ← top_adj, ← f.topEmbedding.map_adj_iff] at nh

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

Goal state before:
pp: case mp.inl.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, b, e} = {a, b, c}

Tactic:
exact ⟨e, by aesop⟩

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

Goal state before:
pp: case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

Tactic:
exact ⟨e, by aesop⟩

Goal state after:
case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

Tactic:
exact ⟨e, by aesop⟩

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

Goal state before:
pp: case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

Tactic:
exact ⟨e, by aesop⟩

Goal state after:
case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
exact ⟨e, by aesop⟩

Goal state after:
case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) → G.IsNClique 3 s

Tactic:
rintro ⟨a, b, c, hab, hbc, hca, rfl⟩
    exact is3Clique_triple_iff.2 ⟨hab, hbc, hca⟩

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
h : Walk.nil.IsPath
⊢ ⟨Walk.nil, h⟩ = Path.nil

pp: case cons
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
h : (Walk.cons h✝ p✝).IsPath
⊢ ⟨Walk.cons h✝ p✝, h⟩ = Path.nil

Tactic:
· rfl

Goal state after:
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
h : (Walk.cons h✝ p✝).IsPath
⊢ ⟨Walk.cons h✝ p✝, h⟩ = Path.nil
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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑m

Tactic:
by sz_positivity

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
have ⟨w, hwp, hwq, hwu, hwv⟩ := hw
    by_cases! p.takeUntil w hwp ≠ q.takeUntil w hwq
    · have := ih _ (hs ▸ length_takeUntil_lt_length hwp hwv) (hp.takeUntil hwp) (hq.takeUntil hwq)
      grind [isSubwalk_takeUntil, IsSubwalk.trans]
    · have := ih _ (hs ▸ length_dropUntil_lt_length hwp hwu) (hp.dropUntil hwp) (hq.dropUntil hwq)
        <| by grind [take_spec]
      grind [isSubwalk_dropUntil, IsSubwalk.trans]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
⊢ image (⇑f) (s.preimage ⇑f ⋯) = s

Tactic:
image_preimage,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
⊢ {x ∈ s | x ∈ Set.range ⇑f} = s
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : 0 < ε
this : 0 < 1 - min 1 ε / 4
⊢ 0 < triangleRemovalBound ε

Tactic:
unfold triangleRemovalBound

Goal state after:
ε : ℝ
hε : 0 < ε
this : 0 < 1 - min 1 ε / 4
⊢ 0 < min (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ ((1 - min 1 ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50
⊢ 0 ≤ ε ^ 5

Tactic:
by sz_positivity

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 α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 0 ≤ ε / 10

Tactic:
by sz_positivity

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

Goal state before:
pp: case refl.refl.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
calc
    _ ≤ (1 - ε / 4) * (ε / (16 * bound (ε / 8) ⌈4 / ε⌉₊)) ^ 3 * card α ^ 3 := by
      gcongr; exact triangleRemovalBound_le hε₁
    _ = (1 - 2 * (ε / 8)) * (ε / 8) ^ 3 * (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) *
          (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) * (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) := by
      ring
    _ ≤ (1 - 2 * (ε / 8)) * (ε / 8) ^ 3 * #s * #Y * #Z := by
      gcongr <;> exact card_bound hP₁ hP₃ ‹_›
    _ ≤ _ :=
      triangle_counting G (by rwa [that]) uXY dXY (by rwa [that]) uXZ dXZ (by rwa [that]) uYZ dYZ

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

Tactic:
set r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))

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
p : ℝ :=
  (∑ 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)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
⊢ 3 / 4 * ε ≤ |p - q|
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✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ #((graph t).cliqueFinset 3) = #t

Tactic:
cliqueFinset_eq_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ #(map toTriangle t) = #t
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
p : ℝ :=
  (∑ 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)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
t : ℝ := ↑(G.edgeDensity U V)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ ε ^ 5 / 49
hqt : |q - t| ≤ ε ^ 5 / 49
⊢ 0 ≤ ε

Tactic:
by sz_positivity

Goal state after:
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).cliqueSet 3 = ↑(map toTriangle t)

Tactic:
cliqueSet_eq_image,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ ⇑toTriangle '' ↑t = ↑(map toTriangle t)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
exact divConst_mul_card _ _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ #(map (Equiv.prodComm (α × α) (α × α)).toEmbedding ({x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2})) =
    Eₘ[t, s]

Tactic:
map_filter

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ #(filter ((fun x ↦ x.1.1 * x.2.1 = x.1.2 * x.2.2) ∘ ⇑(Equiv.prodComm (α × α) (α × α)).symm)
        (map (Equiv.prodComm (α × α) (α × α)).toEmbedding ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    Eₘ[t, s]
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ℤ
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ ↑p ∣ ∑ i ∈ t, a i

Tactic:
simpa [← Int.cast_sum, ZMod.intCast_zmod_eq_zero_iff_dvd]
    using ZMod.erdos_ginzburg_ziv_prime (Int.cast ∘ a) hs

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

Goal state before:
pp: case zero
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * 0 - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = 0 ∧ ↑0 ∣ ∑ i ∈ t, a i

Tactic:
exact ⟨∅, by simp⟩

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

Goal state before:
pp: k : ℕ
⊢ (2 ^ k).bitIndices = [k]

Tactic:
rw [← mul_one (a := 2 ^ k), bitIndices_two_pow_mul]

Goal state after:
k : ℕ
⊢ map (fun x ↦ x + k) (bitIndices 1) = [k]
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case composite.zero
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
hk : 0 ≤ 2 * m - 1
⊢ ∃ 𝒜, #𝒜 = 0 ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
exact ⟨∅, by simp⟩

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

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

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:
· rfl

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h :
  (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝ ≤ (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ ∧
    (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ ≤ (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝
⊢ a₁✝ = a₂✝

Tactic:
geomSum_le_geomSum_iff_toColex_le_toColex hn,

Goal state after:
n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h : toColex a₁✝ ≤ toColex a₂✝ ∧ (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ ≤ (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝
⊢ a₁✝ = a₂✝
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h : toColex a₁✝ ≤ toColex a₂✝ ∧ (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ ≤ (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝
⊢ a₁✝ = a₂✝

Tactic:
geomSum_le_geomSum_iff_toColex_le_toColex hn,

Goal state after:
n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h : toColex a₁✝ ≤ toColex a₂✝ ∧ toColex a₂✝ ≤ toColex a₁✝
⊢ a₁✝ = a₂✝
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case ind.zero
hyp : ∀ m < 0, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin 0)) = numDerangements 0

pp: case ind.succ.zero
hyp : ∀ m < 0 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (0 + 1))) = numDerangements (0 + 1)

pp: case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)

Tactic:
· rfl

Goal state after:
case ind.succ.zero
hyp : ∀ m < 0 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (0 + 1))) = numDerangements (0 + 1)

case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case ind.succ.zero
hyp : ∀ m < 0 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (0 + 1))) = numDerangements (0 + 1)

pp: case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)

Tactic:
· rfl

Goal state after:
case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
⊢ card ↑(derangements (Fin n)) = numDerangements n

Tactic:
by
  induction n using Nat.strongRecOn with | ind n hyp => _
  rcases n with _ | _ | n
  -- knock out cases 0 and 1
  · rfl
  · rfl
  -- now we have n ≥ 2. rewrite everything in terms of card_derangements, so that we can use
  -- `card_derangements_fin_add_two`
  rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp, hyp] <;> lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ∀ (a : ↑(Equiv.RemoveNone.fiber none)), False

Tactic:
Equiv.RemoveNone.fiber_none

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ∀ (a : ↑∅), False