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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : u ∈ (cons ha p').support
⊢ List.count s(u, x) ((cons ha p').takeUntil u h).edges ≤ 1

Tactic:
cases h

Goal state after:
case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x v✝ w✝ : V
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
ha : G.Adj u v✝
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 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✝
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
this : ofSupport (u' :: p.support) ⋯ ⋯ = (cons h₂ p).copy ⋯ ⋯
⊢ ofSupport (cons h₁ (cons h₂ p)).support ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯

Tactic:
simp [this]

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✝
hp : ¬p✝.Nil
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
x✝ : ¬(cons h₁ (cons h₂ p)).Nil
this : ofDarts ({ fst := u', snd := v', adj := h₂ } :: p.darts) ⋯ ⋯ = (cons h₂ p).copy ⋯ ⋯
⊢ ofDarts (cons h₁ (cons h₂ p)).darts ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯

Tactic:
simp [this]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).length = c.length

Tactic:
simpa using (rotate_edges c u h).perm.length_eq

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 + m) ≍ (p.take n).append ((p.drop n).take m)

Tactic:
rw [add_comm]
  induction p generalizing n <;> cases n <;> simp [take, drop]
  grind [drop_getVert]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges

Tactic:
tauto

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ p.take n = p.copy ⋯ ⋯

Tactic:
induction n generalizing p u with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique t ↔ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ G.IsClique (⇑f ⁻¹' t)

case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ ⇑f '' ⇑f ⁻¹' t = t
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
⊢ False

Tactic:
have := hp.three_le_length

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.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
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)))

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

α : 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 < ↑(#(A.sup id)) * ↑(#(B.sup id))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
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
this :
  (p.dropUntil w hwp).length = (p.dropUntil w hwp).length →
    ∃ u' v' p' q', p'.IsSubwalk (p.dropUntil w hwp) ∧ q'.IsSubwalk (q.dropUntil w hwq) ∧ (p'.append q'.reverse).IsCycle
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
grind [isSubwalk_dropUntil, IsSubwalk.trans]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ε ≤ ↑(G.edgeDensity s t)

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : ↑(#s) * ε < ↑(#(G.badVertices ε s t))
this : |↑(G.edgeDensity (G.badVertices ε s t) t) - ↑(G.edgeDensity s t)| < ε
⊢ False

Tactic:
rw [abs_sub_lt_iff] at this

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : ↑(#s) * ε < ↑(#(G.badVertices ε s t))
this :
  ↑(G.edgeDensity (G.badVertices ε s t) t) - ↑(G.edgeDensity s t) < ε ∧
    ↑(G.edgeDensity s t) - ↑(G.edgeDensity (G.badVertices ε s t) t) < ε
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

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

Tactic:
linarith

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

Goal state before:
pp: case hbc
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
⊢ ε ≤ ↑(G.edgeDensity s t) - ε

Tactic:
linarith

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

Goal state before:
pp: case hbc
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
⊢ ε ≤ ↑(G.edgeDensity s u) - ε

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
⊢ ε ≤ ↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))

Tactic:
rw [abs_sub_lt_iff] at this

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this :
  ↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u) < ε ∧
    ↑(G.edgeDensity t u) - ↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) < ε
⊢ ε ≤ ↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
⊢ Rel t y x

Tactic:
cases h

Goal state after:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₁ b✝) (in₀ a✝¹)

case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₀ a✝¹) (in₁ b✝)

case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₂ c✝) (in₀ a✝¹)

case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₀ a✝¹) (in₂ c✝)

case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₂ c✝) (in₁ b✝)

case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ Rel t (in₁ b✝) (in₂ c✝)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this :
  ↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u) < ε ∧
    ↑(G.edgeDensity t u) - ↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) < ε
⊢ ε ≤ ↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))

Tactic:
linarith

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

Goal state before:
pp: case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a

Tactic:
exact ⟨_, ‹_›, by simp⟩

Goal state after:
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
ε : ℝ
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 : ε / 4 ≤ 1
⊢ 0 ≤ 1 - 2 * (ε / 8)

Tactic:
linarith

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

Goal state before:
pp: case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b

Tactic:
exact ⟨_, ‹_›, by simp⟩

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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3431 ∨ a✝ = in₁ ?m.3434 ∨ a✝ = in₂ ?m.3437 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝

Tactic:
tauto

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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3588 ∨ a✝ = in₁ ?m.3591 ∨ a✝ = in₂ ?m.3594 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝

Tactic:
tauto

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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝³ : (a✝⁵, b✝, c✝) ∈ t
a✝² : α
a✝¹ : (a✝², b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3745 ∨ a✝ = in₁ ?m.3748 ∨ a✝ = in₂ ?m.3751 ↔ a✝ = in₀ a✝⁵ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝

Tactic:
tauto

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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝⁵, b✝, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.3902 ∨ a✝ = in₁ ?m.3905 ∨ a✝ = in₂ ?m.3908 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝⁵ ∨ a✝ = in₁ b✝

Tactic:
tauto

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

Goal state before:
pp: case e'_4
α : 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
⊢ ε / 5 = 2 * (ε / 10)

Tactic:
linarith

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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
c✝ : γ
a✝² : (a✝³, b✝¹, c✝) ∈ t
b✝ : β
a✝¹ : (a✝³, b✝, c✝¹) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4059 ∨ a✝ = in₁ ?m.4062 ∨ a✝ = in₂ ?m.4065 ↔ a✝ = in₁ b✝¹ ∨ a✝ = in₂ c✝¹ ∨ a✝ = in₀ a✝³

Tactic:
tauto

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✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.4216 ∨ a✝ = in₁ ?m.4219 ∨ a✝ = in₂ ?m.4222 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝³

Tactic:
tauto

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

Goal state before:
pp: case refine_2.hx₁
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
⊢ x₁ ∈ s

Tactic:
tauto

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

Goal state before:
pp: case refine_2.hx₂
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
⊢ x₂ ∈ s

Tactic:
tauto

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

Goal state before:
pp: case refine_2.hy₁
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
⊢ y₁ ∈ t✝

Tactic:
tauto

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

Goal state before:
pp: case refine_2.hy₂
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
⊢ y₂ ∈ t✝

Tactic:
tauto

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

Goal state before:
pp: case refine_2.hz₁
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
⊢ z₁ ∈ u

Tactic:
tauto

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

Goal state before:
pp: case refine_2.hz₂
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x ↦
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
⊢ z₂ ∈ u

Tactic:
tauto

Goal state after: