mathlib-initiative/mathlib-tactics huggingface dataset:
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 * ↑m / ↑(#U) ≤ ε * (ε / 10)

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:
swap

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
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 < ε

α : 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 * ↑m / ↑(#U) ≤ ε * (ε / 10)
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
v w : V
h : v = w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
simp [h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
⊢ G ⊔ edge s t = G

Tactic:
simp [h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), edge u v = x} = ⨆ e ∈ G.edgeSet, fromEdgeSet {e}

Tactic:
simp_rw [edge, ← iSup_subtype'', iSup, Set.range, Subtype.exists, Sym2.exists, mem_edgeSet]

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

Goal state before:
pp: case right.inl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s ∧ w ∈ s ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

Tactic:
simp [h]

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

Goal state before:
pp: case right.inr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s' ∧ w ∈ s' ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

Tactic:
simp [h]

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

Goal state before:
pp: case nil.mp
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ nil.IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv

Tactic:
rintro ⟨_ | _, _, ⟨⟩⟩
      simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
hadj : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.takeUntil w h).support = ((p.take (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons hadj p).support
⊢ ((cons hadj p).takeUntil w h).support = (((cons hadj p).take (List.idxOf w (cons hadj p).support)).copy ⋯ ⋯).support

Tactic:
grind [takeUntil, support, copy_rfl_rfl, support_take]

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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
sub_le_sub_iff_left

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
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
⊢ ε ^ 5 / 50 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 50
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'
hnil : ¬p₁.Nil
⊢ p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts

Tactic:
rw [isSubwalk_iff_support_isInfix, List.infix_iff_getElem?, List.infix_iff_getElem?]
  refine ⟨fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩,
    fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩⟩
  · rw [getElem?_pos _ _ <| by grind, Option.some_inj]
    ext <;> grind [fst_darts_getElem, snd_darts_getElem]
  · rw [getElem?_pos _ _ <| by grind, Option.some_inj]
    by_cases hi' : i = p₁.length
    · have := h <| i - 1
      grind [not_nil_iff_lt_length, snd_darts_getElem]
    have := h i
    grind [fst_darts_getElem]

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
d : G.Dart
h : d ∈ p.darts
⊢ d.symm ∈ p.reverse.darts

Tactic:
simp [h]

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).getVert m = p.getVert (min n m)

Tactic:
induction p generalizing n m <;> cases n <;> cases m

Goal state after:
case nil.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).getVert 0 = nil.getVert (min 0 0)

case nil.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take 0).getVert (n✝ + 1) = nil.getVert (min 0 (n✝ + 1))

case nil.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).getVert 0 = nil.getVert (min (n✝ + 1) 0)

case nil.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝¹ n✝ : ℕ
⊢ (nil.take (n✝¹ + 1)).getVert (n✝ + 1) = nil.getVert (min (n✝¹ + 1) (n✝ + 1))

case cons.zero.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
⊢ ((cons h✝ p✝).take 0).getVert 0 = (cons h✝ p✝).getVert (min 0 0)

case cons.zero.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take 0).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min 0 (n✝ + 1))

case cons.succ.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert 0 = (cons h✝ p✝).getVert (min (n✝ + 1) 0)

case cons.succ.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n✝¹ n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝¹ + 1)).getVert (n✝ + 1) = (cons h✝ p✝).getVert (min (n✝¹ + 1) (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsTrail
⊢ p₁.IsTrail

Tactic:
obtain ⟨_, _, h⟩ := h
  rw [h] at h₂
  exact h₂.of_append_left.of_append_right

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsPath
⊢ p₁.IsPath

Tactic:
obtain ⟨_, _, h⟩ := h
  rw [h] at h₂
  exact h₂.of_append_left.of_append_right

Goal state after:
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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#B) * ↑(#y) * (↑m / (↑m + 1)) ≤ ↑(#(B.sup id))

Tactic:
· apply le_sum_card_subset_chunk_parts hB hy

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : p.length ≤ n
⊢ List.take (n + 1) p.support ++ [] = p.support

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
obtain (ht | ht) := le_or_gt #t 1

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ↔ ¬1 < #t ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
simp [ht]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
h : G.IsClique ↑s
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑(map f s)

Tactic:
by
  simpa

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

Goal state before:
pp: case right.refine_2
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
⊢ q'.support <+ q.support

Tactic:
· exact isSubwalk_iff_support_isInfix.mp hq' |>.sublist

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
⊢ (Walk.map f p).edges.Nodup ↔ p.edges.Nodup

Tactic:
edges_map,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
⊢ (List.map (Sym2.map ⇑f) p.edges).Nodup ↔ p.edges.Nodup
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
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
have dXZ := P.disjoint hX hZ nXZ

Goal state after:
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
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    #((s * t).disjiUnion (fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ?h)

pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ (↑(s * t)).PairwiseDisjoint fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}

Tactic:
swap

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ (↑(s * t)).PairwiseDisjoint fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    #((s * t).disjiUnion (fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ?h)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

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

pp: case h₂.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
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

Tactic:
swap

Goal state after:
case h₂.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
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
⊢ 0 ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

case h₂.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
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
UVl : 4 / 5 * ε * (4 / 5 * ε) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts * (↑(#(star hP G ε hV U)) / 4 ^ #P.parts)
⊢ ε ^ 4 / 3 ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts * (↑(#(star hP G ε hV U)) / 4 ^ #P.parts) * (9 / 4 ^ 2 * ε ^ 2)
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a n : ℕ
ha : a ∈ n.bitIndices
⊢ n.testBit a = true

Tactic:
by simpa using ha

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ toColex s < toColex {a} ↔ ∀ b ∈ s, b < a

Tactic:
lt_iff_le_and_ne,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ toColex s ≤ toColex {a} ∧ toColex s ≠ toColex {a} ↔ ∀ b ∈ s, b < a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Colex (Finset α)
hst : s ≠ t
⊢ (ofColex s ∆ ofColex t).Nonempty

Tactic:
by
  simpa

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

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

Tactic:
induction n using Nat.prime_composite_induction generalizing ι with

Goal state after:
Module: Mathlib.Combinatorics.Colex

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

Tactic:
lt_iff_le_and_ne,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s ≤ toColex t ∧ toColex s ≠ toColex t ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
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:
lt_iff_le_and_ne,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Colex (Finset α)
⊢ s ≤ t ∧ s ≠ t ↔ ∃ (h : s ≠ t), (ofColex s ∆ ofColex t).max' ⋯ ∈ ofColex t
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : -(w 0 • v) + v 0 • w = 0 → -w 0 = 0 ∧ v 0 = 0
h21 : -(w 1 • v) + v 1 • w = 0 → -w 1 = 0 ∧ v 1 = 0
h22 : -(w 2 • v) + v 2 • w = 0 → -w 2 = 0 ∧ v 2 = 0
⊢ False

Tactic:
neg_add_eq_zero,

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : w 0 • v = v 0 • w → -w 0 = 0 ∧ v 0 = 0
h21 : w 1 • v = v 1 • w → -w 1 = 0 ∧ v 1 = 0
h22 : w 2 • v = v 2 • w → -w 2 = 0 ∧ v 2 = 0
⊢ False
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
a : Finset α
ha : a ∈ 𝒜
⊢ toColex a ∈ ⇑ofColex ⁻¹' ↑𝒜

Tactic:
by simpa using ha

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
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 ∈ {i | i.1 ∈ i.2} ↔ p.1 ∈ {p_1 | p_1 ∈ p.2}

Tactic:
exact fun p => Iff.rfl

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
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 ∈ {i | i.1 ∈ i.2} ↔ p.2 ∈ {l | p.1 ∈ l}

Tactic:
exact fun p => Iff.rfl

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
⊢ lineCount L p = lineCount L q

Tactic:
cases nonempty_fintype P

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝ : Fintype P
⊢ lineCount L p = lineCount L q
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
⊢ lineCount L q = pointCount P l

Tactic:
cases nonempty_fintype P

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
val✝ : Fintype P
⊢ lineCount L q = pointCount P l
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:
by
    have h := Nat.succ_dvd_centralBinom n
    exact mod_cast this

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ ↑H
⊢ x ∈ c ↔ ↑H <• x = c

Tactic:
refine ⟨fun hx => ?_, fun hx =>
    by simp only [← hx, mem_rightCoset_iff, mul_inv_cancel, SetLike.mem_coe, one_mem]⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ ↑H
hx : x ∈ c
⊢ ↑H <• x = c
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest ≠ 0

Tactic:
simp [← toList_ne_nil, nest]

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

Goal state before:
pp: case pos
p q : DyckWord
h : p = 0
⊢ (p + q).firstReturn = q.firstReturn

Tactic:
simp [h]

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

Goal state before:
pp: case pos
p q : DyckWord
h : p = 0
⊢ q ≤ p + q

Tactic:
simp [h]

Goal state after:
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
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B

Tactic:
have : (#(A ∩ B) + #(A ∪ B) : ℝ) = #A + #B := mod_cast card_inter_add_card_union A B
  have : K * #(A ∩ B) + K * #(A ∪ B) = K * #A + K * #B := by simp only [← mul_add, this]
  have : (#(A * S ∩ (B * S)) + #(A * S ∪ B * S) : ℝ) = #(A * S) + #(B * S) :=
    mod_cast card_inter_add_card_union (A * S) (B * S)
  have : (#((A ∩ B) * S) : ℝ) ≤ #(A * S ∩ (B * S)) := by grw [inter_mul_subset]
  simp_rw [expansion, union_mul]
  nlinarith

Goal state after:
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
r : ℝ
⊢ r ≤ connectivity K S ↔ ∀ ⦃A : Finset G⦄, A.Nonempty → r ≤ expansion K S A

Tactic:
have : Nonempty {A : Finset G // A.Nonempty} := ⟨{1}, by simp⟩
  simp [connectivity, le_ciInf_iff, bddBelow_expansion, *]

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

Goal state before:
pp: n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ k < n + 1

Tactic:
simp at hk

Goal state after:
n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k ≤ n
⊢ k < n + 1