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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n + 1 ≤ q.length + 1

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ q.length + 1

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' ↑s)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
t : Finset β
f : α ↪ β
h' : #t ≤ 1
hn : 1 < #t
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
t : Finset β
f : α ↪ β
h' : #t ≤ 1
hn : 1 < #t
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - n ∧ p.length - n ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - n ∧ p.length - n ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - m ∧ p.length - m ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - m ∧ p.length - m ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s = ∅ → G.IsClique ↑s

Tactic:
;

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s = ∅ → G.IsClique ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ↑∅

Tactic:
;

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ↑∅
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ (∃ a, s = {a}) → G.IsClique ↑s

Tactic:
;

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ (∃ a, s = {a}) → G.IsClique ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique ↑{a}

Tactic:
;

Goal state after:
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique ↑{a}
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
this : 3 ≤ p.length
⊢ 1 ≤ p.length

Tactic:
;

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
⊢ 1 ≤ p.length
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
this : 3 ≤ p.length
⊢ 1 ≤ p.length - 1

Tactic:
;

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
⊢ 1 ≤ p.length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ i ∧ i ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ i ∧ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ p.length ∧ p.length ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ p.length ∧ p.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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
⊢ i ≤ p.length - 1 + 1

Tactic:
;

Goal state after:
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
⊢ i ≤ p.length - 1 + 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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
⊢ i + 1 ≤ p.length - 1

Tactic:
;

Goal state after:
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
⊢ i + 1 ≤ p.length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsCircuit ↔ c.IsCircuit

Tactic:
simp [isCircuit_def]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ n ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ n ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
a b : Fin n
| (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
;

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
a b : Fin n
| (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G H : SimpleGraph α
ε δ : 𝕜
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
⊢ ((G.cliqueSet 3).Pairwise fun x y ↦ ∀ a ∈ x ∩ y, ∀ b ∈ x ∩ y, a = b) ↔
    (G.cliqueSet 3).Pairwise fun x y ↦ (↑(x ∩ y)).Subsingleton

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G H : SimpleGraph α
ε δ : 𝕜
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
⊢ ((G.cliqueSet 3).Pairwise fun x y ↦ ∀ a ∈ x ∩ y, ∀ b ∈ x ∩ y, a = b) ↔
    (G.cliqueSet 3).Pairwise fun x y ↦ (↑(x ∩ y)).Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Set α
ht : G.IsClique t
fint : Fintype ↑t
M : G.IsMaximumClique t.toFinset
hsub : ↑t.toFinset ⊆ t
hc : ¬t ⊆ ↑t.toFinset
⊢ False

Tactic:
;

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Set α
ht : G.IsClique t
fint : Fintype ↑t
M : G.IsMaximumClique t.toFinset
hsub : ↑t.toFinset ⊆ t
hc : ¬t ⊆ ↑t.toFinset
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = ⇑{ toFun := map e.toEmbedding, inj' := ⋯ } '' G.cliqueSet n

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = ⇑{ toFun := map e.toEmbedding, inj' := ⋯ } '' G.cliqueSet n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w ↦ ¬G.Adj v w

Tactic:
;

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w ↦ ¬G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj

Tactic:
;

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
;

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

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

Tactic:
;

Goal state after:
ε : ℝ
hε : 0 < ε
this : min 1 ε ≤ 1
⊢ 0 < 1 - min 1 ε / 4
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case hbc
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε ≤ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹

Tactic:
;

Goal state after:
case hbc
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε ≤ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹
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}))
⊢ ↑(#t) * ε ≤ ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
;

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}))
⊢ ↑(#t) * ε ≤ ↑(#t) * (↑(G.edgeDensity s t) - ε)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case h
ε : ℝ
hε : 0 < ε
⊢ ↑⌈4 / ε⌉₊ ^ 3 ≠ 0

Tactic:
;

Goal state after:
case h
ε : ℝ
hε : 0 < ε
⊢ ↑⌈4 / ε⌉₊ ^ 3 ≠ 0
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:
;

Goal state after:
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) - ε
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}))
⊢ ↑(#u) * ε ≤ ↑(#u) * (↑(G.edgeDensity s u) - ε)

Tactic:
;

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}))
⊢ ↑(#u) * ε ≤ ↑(#u) * (↑(G.edgeDensity s u) - ε)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case a
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ #G.edgeFinset ≤ (Fintype.card α).choose 2

Tactic:
;

Goal state after:
case a
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ #G.edgeFinset ≤ (Fintype.card α).choose 2
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:
;

Goal state after:
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) - ε
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}))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))

Tactic:
have := utu (filter_subset (G.Adj x) _) (filter_subset (G.Adj x) _) hY hZ

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)| < ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
          match x with
          | (y, z) => G.Adj y z}))
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:
;

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: case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t

Tactic:
;

Goal state after:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t
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
⊢ ∃ c, (a, b, c) ∈ t

Tactic:
;

Goal state after:
case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t
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
⊢ ∃ b, (a, b, c) ∈ t

Tactic:
;

Goal state after:
case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t
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
⊢ ∃ b, (a, b, c) ∈ t

Tactic:
;

Goal state after:
case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t
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
⊢ ∃ a, (a, b, c) ∈ t

Tactic:
;

Goal state after:
case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t
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
⊢ ∃ a, (a, b, c) ∈ t

Tactic:
;

Goal state after:
case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t
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:
;

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₁ (a, b, c).2.1)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₁ (a, b, c).2.1)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, (a, b, c).2.1, ?c) ∈ t

pp: case c
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ γ

Tactic:
;

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, (a, b, c).2.1, ?c) ∈ t

case c
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ γ
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:
;

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