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

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ ∀ (a : Finset α) (x x_1 x_2 : α),
    G.Adj x x_1 →
      G.Adj x x_2 → G.Adj x_1 x_2 → a = {x, x_1, x_2} → 3 ≤ #(bipartiteAbove (fun s e ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset a)

Tactic:
rintro _ a b c hab hac hbc rfl

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ 3 ≤ #(bipartiteAbove (fun s e ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})
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
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
·

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
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ ↑{a, b} ⊆ s

pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ ↑{a, b} ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg.refine_1
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
x✝ : V
⊢ x✝ ∈ p.support.tail → x✝ ∈ q.reverse.support.tail → False

pp: case neg.refine_2
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
⊢ 1 < p.length ∨ 1 < q.reverse.length

Tactic:
·

Goal state after:
case neg.refine_1
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
x✝ : V
⊢ x✝ ∈ p.support.tail → x✝ ∈ q.reverse.support.tail → False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg.refine_2
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
⊢ 1 < p.length ∨ 1 < q.reverse.length

Tactic:
·

Goal state after:
case neg.refine_2
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
⊢ 1 < p.length ∨ 1 < q.reverse.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n → s ∈ map f '' G.cliqueSet n

pp: case mpr
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ map f '' G.cliqueSet n → s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n → s ∈ map f '' G.cliqueSet n
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ #(bipartiteBelow (fun s e ↦ e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ #(bipartiteBelow (fun s e ↦ e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ map f '' G.cliqueSet n → s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ map f '' G.cliqueSet n → s ∈ (SimpleGraph.map (⇑f) G).cliqueSet n
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun e s ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)

pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ b ∈ G.cliqueFinset 3, #(bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun e s ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
⊢ (SimpleGraph.map (⇑e) G).cliqueSet 1 = map e.toEmbedding '' G.cliqueSet 1

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
⊢ (SimpleGraph.map (⇑e) G).cliqueSet 1 = map e.toEmbedding '' G.cliqueSet 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = map e.toEmbedding '' G.cliqueSet n
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ (b : Finset α) (x x_1 x_2 : α),
    G.Adj x x_1 →
      G.Adj x x_2 → G.Adj x_1 x_2 → b = {x, x_1, x_2} → #(bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3

Tactic:
rintro _ a b c hab hac hbc rfl

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ #(bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset {a, b, c}) ≤ 3
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_3
G : SimpleGraph α
h : BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s

pp: case neg
α : Type u_3
G : SimpleGraph α
h : ¬BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s

Tactic:
·

Goal state after:
case pos
α : Type u_3
G : SimpleGraph α
h : BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case right.refine_1
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ p'.support <+ p.support

pp: case right.refine_2
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ q'.support <+ q.support

Tactic:
·

Goal state after:
case right.refine_1
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ p'.support <+ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case neg
α : Type u_3
G : SimpleGraph α
h : ¬BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s

Tactic:
·

Goal state after:
case neg
α : Type u_3
G : SimpleGraph α
h : ¬BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case right.refine_2
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ q'.support <+ q.support

Tactic:
·

Goal state after:
case right.refine_2
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ q'.support <+ q.support
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case ha
α : 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
⊢ ∃ x ∈ A, (id x).Nonempty

pp: case hb
α : 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
⊢ ∃ x ∈ B, (id x).Nonempty

Tactic:
·

Goal state after:
case ha
α : 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
⊢ ∃ x ∈ A, (id x).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case hb
α : 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
⊢ ∃ x ∈ B, (id x).Nonempty

Tactic:
·

Goal state after:
case hb
α : 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
⊢ ∃ x ∈ B, (id x).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u✝ hs).IsPath

pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∉ p'.bypass.support
⊢ (cons h✝ p'.bypass).IsPath

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u✝ hs).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∉ p'.bypass.support
⊢ (cons h✝ p'.bypass).IsPath

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∉ p'.bypass.support
⊢ (cons h✝ p'.bypass).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).support <+ u✝ :: p✝.support

pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).support <+ u✝ :: p✝.support

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).support <+ u✝ :: p✝.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).support <+ u✝ :: p✝.support

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).support <+ u✝ :: p✝.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).darts <+ { fst := u✝, snd := v✝, adj := h✝¹ } :: p✝.darts

pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).darts <+ { fst := u✝, snd := v✝, adj := h✝¹ } :: p✝.darts

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).darts <+ { fst := u✝, snd := v✝, adj := h✝¹ } :: p✝.darts
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).darts <+ { fst := u✝, snd := v✝, adj := h✝¹ } :: p✝.darts

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).darts <+ { fst := u✝, snd := v✝, adj := h✝¹ } :: p✝.darts
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mk.refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).1 ∈ s

pp: case mk.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).2 ∈ s

Tactic:
·

Goal state after:
case mk.refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).1 ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mk.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).2 ∈ s

Tactic:
·

Goal state after:
case mk.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} = ∅
⊢ (v, w).2 ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv'✝ : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv'✝ w).IsCircuit
hvv' : s(v, v') ∈ w.bypass.edges
⊢ False

pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ (cons hvv' w.bypass).support.tail.Nodup

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv'✝ : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv'✝ w).IsCircuit
hvv' : s(v, v') ∈ w.bypass.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ (cons hvv' w.bypass).support.tail.Nodup

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ (cons hvv' w.bypass).support.tail.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ (cons hvv' w.bypass).support.tail.Nodup

Tactic:
simpa using (bypass_isPath _).support_nodup

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

Goal state before:
pp: case inl
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : ↥tris → Sym2 α := fun t ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
i : (↑t₁ ∩ ↑t₂).Subsingleton
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯
⊢ False

pp: case inr
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : ↥tris → Sym2 α := fun t ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
i : (↑t₁ ∩ ↑t₂).Subsingleton
t : fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
⊢ False

Tactic:
·

Goal state after:
case inl
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : ↥tris → Sym2 α := fun t ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩
i : (↑t₁ ∩ ↑t₂).Subsingleton
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯
⊢ False