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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m

pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

Tactic:
·

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : m = 0
hnm : p.getVert (n - 1) = (cons h p).getVert 0
hvp : v ∉ p.support
⊢ n - 1 ≤ p.length

Tactic:
by lia

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : ¬m = 0
hnm : p.getVert (n - 1) = p.getVert (m - 1)
⊢ n - 1 ≤ p.length

Tactic:
by lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : ¬m = 0
hnm : p.getVert (n - 1) = p.getVert (m - 1)
⊢ m - 1 ≤ p.length

Tactic:
by lia

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
⊢ i = 0

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

Tactic:
·

Goal state after:
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
⊢ i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Paths

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

Tactic:
·

Goal state after:
case neg
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
⊢ i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
i : ℕ
hp : Walk.nil.IsPath
hi : i ≤ Walk.nil.length
⊢ Walk.nil.getVert i = u ↔ i = 0

pp: case cons
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).IsPath
hi : i ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert i = u ↔ i = 0

Tactic:
·

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
i : ℕ
hp : Walk.nil.IsPath
hi : i ≤ Walk.nil.length
⊢ Walk.nil.getVert i = u ↔ i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).IsPath
hi : i ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert i = u ↔ i = 0

Tactic:
·

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).IsPath
hi : i ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert i = u ↔ i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.reverse.length - i ≤ p.reverse.length

Tactic:
by lia

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

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
u : α
hu : u ∈ s
v : α
hv : v ∈ s
hne : u ≠ v
⊢ G.Adj u v

pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
u : α
hu : u ∈ s
v : α
hv : v ∈ s
hne : u ≠ v
⊢ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: 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)

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

Tactic:
·

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)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

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

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Subsingleton
⊢ (SimpleGraph.map (⇑f) G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Subsingleton
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Nontrivial
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Subsingleton
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t → ∃ s, G.IsClique ↑s ∧ map f s = t

pp: case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) → (SimpleGraph.map (⇑f) G).IsClique ↑t

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t → ∃ s, G.IsClique ↑s ∧ map f s = t
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
this : ∀ {p q : G.Walk u v}, (∀ (k : ℕ), p.getVert k = q.getVert k) → p.length ≤ q.length → p = q
hpq : ¬p.length ≤ q.length
⊢ p = q

pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
⊢ p = q

Tactic:
·

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
this : ∀ {p q : G.Walk u v}, (∀ (k : ℕ), p.getVert k = q.getVert k) → p.length ≤ q.length → p = q
hpq : ¬p.length ≤ q.length
⊢ p = q
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: 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

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

Tactic:
·

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

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Tactic:
·

Goal state after:
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
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
⊢ 0 ≤ (cons h q).length

Tactic:
by lia

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ G.LocallyLinear

pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e) G).LocallyLinear

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ G.LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e) G).LocallyLinear

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e) G).LocallyLinear
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

pp: case neg
α : 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:
·

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

Goal state before:
pp: case pos.inl
α : 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
hx : x ∈ s \ {v}
hy : y ∈ s \ {v}
⊢ (G ⊔ edge v w).Adj x y

pp: case pos.inr
α : 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
hx : x ∈ s \ {w}
hy : y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
·

Goal state after:
case pos.inl
α : 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
hx : x ∈ s \ {v}
hy : y ∈ s \ {v}
⊢ (G ⊔ edge v w).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s →
    G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

pp: case mpr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) →
    (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s

Tactic:
·

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s →
    G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos.inr
α : 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
hx : x ∈ s \ {w}
hy : y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
·

Goal state after:
case pos.inr
α : 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
hx : x ∈ s \ {w}
hy : y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case neg
α : 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:
·

Goal state after:
case neg
α : 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
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
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ n - 1 ≤ p.tail.length

Tactic:
by lia

Goal state after:
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
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ m - 1 ≤ p.tail.length

Tactic:
by lia

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n → ∃ s, G.IsNClique n s ∧ map f s = t

pp: case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsNClique n s ∧ map f s = t) → (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n → ∃ s, G.IsNClique n s ∧ map f s = t
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique ↑(insert a s)

pp: case card_eq
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ #(insert a s) = n + 1

Tactic:
·

Goal state after:
case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique ↑(insert a s)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case card_eq
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ #(insert a s) = n + 1

Tactic:
·

Goal state after:
case card_eq
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ #(insert a s) = n + 1
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:
·

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

Tactic:
by lia

Goal state after:
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) = u
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ i - 1 ≤ p.length

Tactic:
by lia

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

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

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

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

Tactic:
·

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : v = w
⊢ (c.takeUntil w h).IsPath

pp: case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : v = w
⊢ (c.takeUntil w h).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) →
    (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s

Tactic:
·

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) →
    (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s
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
⊢ ↑(#(interedges G.Adj x y)) ≤
    ↑(#(interedges G.Adj x y)) *
      ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))))

pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))

Tactic:
·

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