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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) G').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) G').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hG'.some
e' : Sym2 ↑G'.verts :=
  Sym2.map
    (⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ G.edgeSet ∧
    ∀ (x : G.Subgraph) (x_1 : Nonempty (H ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map
      (Subtype.val ∘
        ⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm)
      e =
    ⋯.some

Tactic:
← he₁

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) G').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) G').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hG'.some
e' : Sym2 ↑G'.verts :=
  Sym2.map
    (⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ G.edgeSet ∧
    ∀ (x : G.Subgraph) (x_1 : Nonempty (H ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map
      (Subtype.val ∘
        ⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm)
      e =
    Sym2.map Subtype.val e
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ w = u ↔ u = w

Tactic:
rw [eq_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) ↔ x✝ ∈ {u, v}

Tactic:
refine ⟨?_, fun h ↦ h.elim (fun hl ↦ ⟨v, .inl ⟨hl.symm, rfl⟩⟩) fun hr ↦ ⟨u, .inr ⟨rfl, hr.symm⟩⟩⟩

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) → x✝ ∈ {u, v}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), edge u v = x} = G

Tactic:
refine .trans ?_ G.biSup_fromEdgeSet_singleton_eq

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), edge u v = x} = ⨆ e ∈ G.edgeSet, fromEdgeSet {e}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : w.length ≤ i
⊢ w.getVert i = v

Tactic:
by
  induction w generalizing i with
  | nil => rfl
  | cons _ _ ih =>
    cases i
    · cases hi
    · exact ih (Nat.succ_le_succ_iff.1 hi)

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
⊢ ∃ x q, ∃ (h'_1 : G.Adj x w✝), cons h (cons h' p) = q.concat h'_1

Tactic:
obtain ⟨y, q, h'', hc⟩ := ih h'

Goal state after:
case cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
y : V
q : G.Walk u✝ y
h'' : G.Adj y w✝
hc : cons h' p = q.concat h''
⊢ ∃ x q, ∃ (h'_1 : G.Adj x w✝), cons h (cons h' p) = q.concat h'_1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case tail
V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
hx : ¬v = u
a✝ : List.Mem u p.support
⊢ u ∈ p.support

Tactic:
assumption

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
⊢ p₁.support <:+: p₂.support ↔ p₁.darts <:+: p₂.darts

Tactic:
List.infix_iff_getElem?,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
⊢ (∃ k,
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]) ↔
    p₁.darts <:+: p₂.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
h : G.Adj u✝ w
⊢ (nil.concat h).support = nil.support ++ [w]

Tactic:
simp [*, concat_nil]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ w), (p✝.concat h).support = p✝.support ++ [w]
h : G.Adj w✝ w
⊢ ((cons h✝ p✝).concat h).support = (cons h✝ p✝).support ++ [w]

Tactic:
simp [*, concat_nil]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
h : G.Adj u✝ w
⊢ (nil.concat h).darts = nil.darts.concat { fst := u✝, snd := w, adj := h }

Tactic:
simp [*, concat_nil]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ w), (p✝.concat h).darts = p✝.darts.concat { fst := w✝, snd := w, adj := h }
h : G.Adj w✝ w
⊢ ((cons h✝ p✝).concat h).darts = (cons h✝ p✝).darts.concat { fst := w✝, snd := w, adj := h }

Tactic:
simp [*, concat_nil]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ u = w

Tactic:
by simpa using (hl ▸ getVert_takeUntil h (by rfl) :
    (p.takeUntil u h).getVert (p.takeUntil u h).length = p.getVert p.length)

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.take 0 = nil.copy ⋯ ⋯

Tactic:
simp [take]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).take 0 = nil.copy ⋯ ⋯

Tactic:
simp [take]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u : V
⊢ (nil.take 0).Nil ↔ nil.Nil ∨ 0 = 0

Tactic:
simp [take]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).Nil ↔ nil.Nil ∨ n✝ + 1 = 0

Tactic:
simp [take]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).take 0).Nil ↔ (cons h✝ p✝).Nil ∨ 0 = 0

Tactic:
simp [take]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).Nil ↔ (cons h✝ p✝).Nil ∨ n✝ + 1 = 0

Tactic:
simp [take]

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

Goal state before:
pp: case succ.nil
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
h : nil.length ≤ n + 1
⊢ nil.take (n + 1) = nil.copy ⋯ ⋯

Tactic:
simp [take]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
w✝ : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ s) y → w✝ ≤ y → y ≤ w✝
u v : V
p : G.Walk u v
hp : p.IsTrail
right✝ : p.length = w✝
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsPath ∧ p.length = n}
this : s.Finite
x : V
⊢ ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsPath ∧ p.length = n}
this : s.Finite
x : V
w✝ : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ s) y → w✝ ≤ y → y ≤ w✝
u v : V
p : G.Walk u v
hp : p.IsPath
right✝ : p.length = w✝
⊢ ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
x✝³ : i < p.support.length
x✝² : j < p.support.length
x✝¹ : i < j
x✝ : p.support[i] = p.support[j]
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
this✝ : ¬p'.Nil
this : p'.IsSubwalk p
⊢ False

Tactic:
grind [take_getVert, getVert_eq_support_getElem]

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

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

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

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

Tactic:
· grind [IsPath.disjoint_edges_of_disjoint_support, List.Disjoint.symm]

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

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

Tactic:
assumption

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

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

Tactic:
assumption

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

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

Tactic:
assumption

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

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

Tactic:
assumption

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

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

Tactic:
assumption

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

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

Tactic:
assumption

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

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

Tactic:
rintro ⟨⟩; exact ⟨_, ‹_›⟩

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

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

Tactic:
rintro ⟨⟩; exact ⟨_, ‹_›⟩

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

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

Tactic:
rintro ⟨⟩; exact ⟨_, ‹_›⟩

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

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

Tactic:
rintro ⟨⟩; exact ⟨_, ‹_›⟩

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

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

Tactic:
rintro ⟨⟩; exact ⟨_, ‹_›⟩

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

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

Tactic:
rintro ⟨⟩; exact ⟨_, ‹_›⟩

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

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

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

Tactic:
assumption

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

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

Tactic:
assumption

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

Goal state before:
pp: case in₀₁.in₀₂.in₁₂.refine_1.a
α : 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✝⁴, b✝¹, ?in₀₁.in₀₂.in₁₂.refine_1.c) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₀₁.in₀₂.in₁₂.refine_2.a
α : 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✝⁴, ?in₀₁.in₀₂.in₁₂.refine_2.b, c✝) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₀₁.in₀₂.in₁₂.refine_3.a
α : 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₀₁.in₀₂.in₁₂.refine_3.a✝, b✝¹, c✝) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₁₀.in₁₂.in₀₂.refine_1.a
α : 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✝⁴, b✝¹, ?in₁₀.in₁₂.in₀₂.refine_1.c) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₁₀.in₁₂.in₀₂.refine_2.a
α : 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✝⁴, ?in₁₀.in₁₂.in₀₂.refine_2.b, c✝) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₁₀.in₁₂.in₀₂.refine_3.a
α : 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₁₀.in₁₂.in₀₂.refine_3.a✝, b✝¹, c✝) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₀₂.in₀₁.in₂₁.refine_1.a
α : 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✝⁴, b✝, ?in₀₂.in₀₁.in₂₁.refine_1.c) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₀₂.in₀₁.in₂₁.refine_2.a
α : 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✝⁴, ?in₀₂.in₀₁.in₂₁.refine_2.b, c✝¹) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₀₂.in₀₁.in₂₁.refine_3.a
α : 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₀₂.in₀₁.in₂₁.refine_3.a✝, b✝, c✝¹) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₂₀.in₂₁.in₀₁.refine_1.a
α : 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✝⁴, b✝, ?in₂₀.in₂₁.in₀₁.refine_1.c) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₂₀.in₂₁.in₀₁.refine_2.a
α : 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✝⁴, ?in₂₀.in₂₁.in₀₁.refine_2.b, c✝¹) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₂₀.in₂₁.in₀₁.refine_3.a
α : 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₂₀.in₂₁.in₀₁.refine_3.a✝, b✝, c✝¹) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₁₂.in₁₀.in₂₀.refine_1.a
α : 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✝², b✝¹, ?in₁₂.in₁₀.in₂₀.refine_1.c) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₁₂.in₁₀.in₂₀.refine_2.a
α : 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✝², ?in₁₂.in₁₀.in₂₀.refine_2.b, c✝¹) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₁₂.in₁₀.in₂₀.refine_3.a
α : 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₁₂.in₁₀.in₂₀.refine_3.a✝, b✝¹, c✝¹) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₂₁.in₂₀.in₁₀.refine_1.a
α : 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✝², b✝¹, ?in₂₁.in₂₀.in₁₀.refine_1.c) ∈ t

Tactic:
assumption

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

Goal state before:
pp: case in₂₁.in₂₀.in₁₀.refine_2.a
α : 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✝², ?in₂₁.in₂₀.in₁₀.refine_2.b, c✝¹) ∈ t

Tactic:
assumption

Goal state after: