mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Tactic:
rw [← hcard, card_map]

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
⊢ #u ≤ mulRothNumber s
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: M N : ℕ
⊢ addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤ addRothNumber (range M) + addRothNumber (range N)

Tactic:
← addRothNumber_map_add_left (range N) M

Goal state after:
M N : ℕ
⊢ addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    addRothNumber (range M) + addRothNumber (map (addLeftEmbedding M) (range N))
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
h : Set.BijOn Nat.cast ↑(range ↑k) ↑(Iio k)
⊢ addRothNumber (Iio k) ≤ rothNumberNat ↑k

Tactic:
exact (AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 ≤ log ↑N / ↑(nValue N)

pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (↑(nValue N))⁻¹ ≠ 0

pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹ / 2

Tactic:
le_div_iff₀

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 * ↑(nValue N) ≤ log ↑N

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑(nValue N)

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (↑(nValue N))⁻¹ ≠ 0

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹ / 2
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ √(log ↑N) / 1.38

Tactic:
le_div_iff₀

Goal state after:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log ↑N)

N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ (50 / 19) ^ 2 ≤ log ↑N

Tactic:
have : (12 : ℕ) * log 2 ≤ log N := by
      rw [← log_rpow zero_lt_two, rpow_natCast]
      exact log_le_log (by positivity) (mod_cast hN)

Goal state after:
case hx
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ log ↑N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 2 / ↑n * √(log ↑N) ≤ 2

pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)

Tactic:
div_mul_eq_mul_div,

Goal state after:
case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 2 * √(log ↑N) / ↑n ≤ 2

case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A * A ⊆ x • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
use x

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
x y : Finset α × Finset α
⊢ DevosMulRel x y ↔
    #(x.1 * x.2) < #(y.1 * y.2) ∨
      #(x.1 * x.2) = #(y.1 * y.2) ∧ #y.1 + #y.2 < #x.1 + #x.2 ∨
        #(x.1 * x.2) = #(y.1 * y.2) ∧ #x.1 + #x.2 = #y.1 + #y.2 ∧ #x.1 < #y.1

Tactic:
simp [DevosMulRel, Prod.lex_iff, and_or_left]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ G.maxDegree = G'.maxDegree

Tactic:
maxDegree,

Goal state after:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithBot.unbotD 0 (image (fun v ↦ G.degree v) univ).max = G'.maxDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithBot.unbotD 0 (image (fun v ↦ G.degree v) univ).max = G'.maxDegree

Tactic:
maxDegree,

Goal state after:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithBot.unbotD 0 (image (fun v ↦ G.degree v) univ).max = WithBot.unbotD 0 (image (fun v ↦ G'.degree v) univ).max
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
⊢ G.maxDegree = G'.maxDegree

Tactic:
by
  classical
  have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)
  rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
⊢ P ≤ (Finpartition.empty α).copy ⋯

Tactic:
intro x hx
      simpa [h, P.ne_bot hx] using P.le hx

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : s = ∅
⊢ #s % 0 ≤ 0

Tactic:
← Finset.card_eq_zero

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ #s % 0 ≤ 0
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x✝ : Finset α
inst✝ : DecidableRel ⇑s
x : α
a✝ : x ∈ x✝
⊢ ∃ x₂ ∈ x✝, s x x₂

Tactic:
use x

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

Tactic:
exact log_pos (by simp)

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : Disjoint t t'
⊢ Disjoint (interedges r s t) (interedges r s t')

Tactic:
rw [Finset.disjoint_left] at ht ⊢

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s t'
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ G.edgeDensity s t + Gᶜ.edgeDensity s t = 1

Tactic:
edgeDensity_def,

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) / (↑(#s) * ↑(#t)) + Gᶜ.edgeDensity s t = 1
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) / (↑(#s) * ↑(#t)) + Gᶜ.edgeDensity s t = 1

Tactic:
edgeDensity_def,

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) / (↑(#s) * ↑(#t)) + ↑(#(Gᶜ.interedges s t)) / (↑(#s) * ↑(#t)) = 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : 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
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ 1 = 4 / ε ^ 5 * (ε ^ 5 / 4)

Tactic:
div_mul_div_cancel₀ (pow_pos hε 5).ne'

Goal state after:
α : 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
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ 1 = 4 / 4
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : 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
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ε ^ 5 / 4 * ↑i ≤ 1
⊢ ↑i ≤ 4 / ε ^ 5

Tactic:
div_mul_eq_mul_div,

Goal state after:
α : 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
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ε ^ 5 * ↑i / 4 ≤ 1
⊢ ↑i ≤ 4 / ε ^ 5
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G✝ G₁ G₂ G₃ : SimpleGraph V
H✝ : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst✝ : Fintype V
G : SimpleGraph V
H : SimpleGraph W
⊢ ℕ

Tactic:
by
  classical exact #{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}

Goal state after:
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
⊢ (equitabilise h).parts = {a ∈ (equitabilise h).parts | #a = m ∨ #a = m + 1}

Tactic:
filter_true_of_mem

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
⊢ (equitabilise h).parts = (equitabilise h).parts

α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ ∀ x ∈ (equitabilise h).parts, #x = m ∨ #x = m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Operations

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

Tactic:
· refine ⟨fun h ↦ .inr <| h (by simp_all [edge_adj]), fun hadj v' w' hvw' ↦ ?_⟩
    grind [adj_symm]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
rcases eq_or_ne u v with rfl | h
  · simp [edge_self_eq_bot]
  simp [← disjoint_edgeSet, edgeSet_edge_of_ne h]

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
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
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m ≤ 2 ^ (#P.parts - 1) * ↑m * (2 * ↑(#(G.nonuniformWitness ε U V))) / (↑(#U) * ε)

Tactic:
le_div_iff₀

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
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m * (↑(#U) * ε) ≤ 2 ^ (#P.parts - 1) * ↑m * (2 * ↑(#(G.nonuniformWitness ε U V)))

α : 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
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 0 < ↑(#U) * ε
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length
⊢ False

Tactic:
simp only [takeUntil_takeUntil] at h1 h2

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (p.takeUntil w ⋯).length < (p.takeUntil x ⋯).length
h2 : (p.takeUntil x ⋯).length < (p.takeUntil w hw).length
⊢ False
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
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
⊢ (1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))) ≤ 1

Tactic:
div_mul_eq_mul_div,

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
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
⊢ (1 - ε ^ 5 / 50) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))) / (↑(#(A.sup id)) * ↑(#(B.sup id))) ≤ 1
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:
by
  induction p generalizing n m <;> cases n <;> cases m <;> simp [*, take]

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

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
obtain (⟨hx, hy⟩ | ⟨hx, hy⟩) := h'
    · exact hv.mono le_sup_left hx hy hxy
    · exact hw.mono le_sup_left hx hy hxy

Goal state after:
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

pp: case neg
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:
· rw [p.getVert_of_length_le (by lia : p.length ≤ i + 1),
      hpc.getVert_endpoint_iff (by lia)] at h'
    lia

Goal state after:
case neg
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
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
⊢ 1 ≤ (1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))

Tactic:
div_mul_eq_mul_div,

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

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬s(a, b).IsDiag
⊢ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}.Subsingleton

Tactic:
simp only [Sym2.mk_isDiag_iff] at hab

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬a = b
⊢ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}.Subsingleton
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
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp ≠ q.takeUntil w hwq
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

pp: case neg
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
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp = q.takeUntil w hwq
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
· have := ih _ (hs ▸ length_takeUntil_lt_length hwp hwv) (hp.takeUntil hwp) (hq.takeUntil hwq)
      grind [isSubwalk_takeUntil, IsSubwalk.trans]

Goal state after:
case neg
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
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp = q.takeUntil w hwq
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
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
⊢ {x ∈ s | x ∈ Set.range ⇑f} = s

Tactic:
filter_true_of_mem

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

α : 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
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
p : G.Walk u u
hinj : Injective ⇑f
⊢ (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ↔ p.IsTrail ∧ p ≠ nil

Tactic:
isTrail_map_iff_of_injective hinj,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ p.IsTrail ∧ Walk.map f p ≠ nil ↔ p.IsTrail ∧ p ≠ nil