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

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

Tactic:
constructor

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

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

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

Tactic:
constructor

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)

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.Triangle.Basic

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

Tactic:
constructor

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

case mpr
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
⊢ (∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton) → G.EdgeDisjointTriangles
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ G.CliqueFree (Fintype.card β) ↔ ⊤.Free G

Tactic:
by
  rw [← not_iff_not, not_free, not_cliqueFree_iff_top_isContained,
    isContained_congr (Iso.completeGraph (equivFin β)) Iso.refl]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges) ∧ p.append q ≠ Walk.nil ∧ (p.append q).support.tail.Nodup

Tactic:
refine ⟨⟨hp.isTrail, hq.isTrail, ?_⟩, ?_, ?_⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ p.edges.Disjoint q.edges

case refine_2
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ p.append q ≠ Walk.nil

case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.append q).support.tail.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ G.Adj (if a = x then s else φ a) (if b = x then s else φ b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
apply_ite (G.Adj · _),

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ (if a = x then G.Adj s (if b = x then s else φ b) else G.Adj (φ a) (if b = x then s else φ b)) ↔
    (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 ↔ G = ⊥

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G = ⊥

case mpr
α : Type u_1
G : SimpleGraph α
⊢ G = ⊥ → G.CliqueFree 2
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

Tactic:
constructor

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

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

Tactic:
ext

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
x✝ : Finset β
⊢ x✝ ∈ (SimpleGraph.map (⇑e) G).cliqueSet 1 ↔ x✝ ∈ map e.toEmbedding '' G.cliqueSet 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
⊢ nil.bypass.IsPath

Tactic:
simp!

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
⊢ nil.bypass.support <+ nil.support

Tactic:
simp!

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
⊢ nil.bypass.darts <+ nil.darts

Tactic:
simp!

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

Goal state before:
pp: α : 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₂⟩
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
i : (fun x y ↦ (↑x ∩ ↑y).Subsingleton) t₁ t₂
⊢ False

Tactic:
Sym2.eq_iff

Goal state after:
α : 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₂⟩
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
i : (↑t₁ ∩ ↑t₂).Subsingleton
⊢ 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
⊢ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) - ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
      ε ^ 5 / 49 ∧
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) -
        (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
      ε ^ 5 / 49

Tactic:
constructor

Goal state after:
case left
α : 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
⊢ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) - ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ε ^ 5 / 49

case right
α : 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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
    ε ^ 5 / 49
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 α
⊢ ((s \ (G.badVertices ε s t ∪ G.badVertices ε s u)).biUnion fun x ↦
      image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z}

Tactic:
rintro ⟨x, y, z⟩

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x y z : α
⊢ ((x, y, z) ∈
      (s \ (G.badVertices ε s t ∪ G.badVertices ε s u)).biUnion fun x ↦
        image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) →
    (x, y, z) ∈
      {x ∈ s ×ˢ t ×ˢ u |
        match x with
        | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

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

Tactic:
constructor

Goal state after:
case in₀₁.a
α : 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
⊢ (a✝¹, b✝, ?in₀₁.c) ∈ t

case in₀₁.c
α : 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
⊢ γ
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

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

Tactic:
constructor

Goal state after:
case in₁₀.a
α : 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
⊢ (a✝¹, b✝, ?in₁₀.c) ∈ t

case in₁₀.c
α : 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
⊢ γ
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

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

Tactic:
constructor

Goal state after:
case in₀₂.a
α : 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
⊢ (a✝¹, ?in₀₂.b, c✝) ∈ t

case in₀₂.b
α : 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
⊢ β
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

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

Tactic:
constructor

Goal state after:
case in₂₀.a
α : 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
⊢ (a✝¹, ?in₂₀.b, c✝) ∈ t

case in₂₀.b
α : 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
⊢ β
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

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

Tactic:
constructor

Goal state after:
case in₁₂.a
α : 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
⊢ (?in₁₂.a✝, b✝, c✝) ∈ t

case in₁₂.a
α : 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
⊢ α
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

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

Tactic:
constructor

Goal state after:
case in₂₁.a
α : 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
⊢ (?in₂₁.a✝, b✝, c✝) ∈ t

case in₂₁.a
α : 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
⊢ α
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:
constructor

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: α : 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).2.1) (in₀ (a, b, c).1)

Tactic:
constructor

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: α : 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.2)

Tactic:
constructor

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, ?b, (a, b, c).2.2) ∈ t

case b
α : 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: α : 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).2.2) (in₀ (a, b, c).1)

Tactic:
constructor

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, ?b, (a, b, c).2.2) ∈ t

case b
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ 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}))
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)| < ε
this :
  ε ≤
    ↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) /
      (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y})))
hε : 0 ≤ ε
⊢ ε ^ 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:
refine le_trans ?_ (mul_le_of_le_div₀ (Nat.cast_nonneg _) (by positivity) 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)| < ε
this :
  ε ≤
    ↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) /
      (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y})))
hε : 0 ≤ ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤ ε * (↑(#({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
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₂ (a, b, c).2.2)

Tactic:
constructor

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, (a, b, c).2.1, (a, b, c).2.2) ∈ t

case a
α : 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: α : 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).2.2) (in₁ (a, b, c).2.1)

Tactic:
constructor

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, (a, b, c).2.1, (a, b, c).2.2) ∈ t

case a
α : 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: α : 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
⊢ {in₀ ?m.3431, in₁ ?m.3434, in₂ ?m.3437} = {in₀ a✝⁴, in₁ b✝¹, in₂ c✝}

Tactic:
ext

Goal state after:
α : 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, in₁ ?m.3434, in₂ ?m.3437} ↔ a✝ ∈ {in₀ a✝⁵, in₁ b✝¹, in₂ c✝}
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
⊢ {in₀ ?m.3588, in₁ ?m.3591, in₂ ?m.3594} = {in₁ b✝¹, in₀ a✝⁴, in₂ c✝}

Tactic:
ext

Goal state after:
α : 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, in₁ ?m.3591, in₂ ?m.3594} ↔ a✝ ∈ {in₁ b✝¹, in₀ a✝⁵, in₂ c✝}
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
⊢ {in₀ ?m.3745, in₁ ?m.3748, in₂ ?m.3751} = {in₀ a✝⁴, in₂ c✝¹, in₁ b✝}

Tactic:
ext

Goal state after:
α : 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, in₁ ?m.3748, in₂ ?m.3751} ↔ a✝ ∈ {in₀ a✝⁵, in₂ c✝¹, in₁ b✝}
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
⊢ {in₀ ?m.3902, in₁ ?m.3905, in₂ ?m.3908} = {in₂ c✝¹, in₀ a✝⁴, in₁ b✝}

Tactic:
ext

Goal state after:
α : 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, in₁ ?m.3905, in₂ ?m.3908} ↔ a✝ ∈ {in₂ c✝¹, in₀ a✝⁵, in₁ b✝}