Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₀₁.in₀₂.in₁₂
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₀ a✝⁴, in₁ b✝¹, in₂ c✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

pp: case in₁₀.in₁₂.in₀₂
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₁ b✝¹, in₀ a✝⁴, in₂ c✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

pp: case in₀₂.in₀₁.in₂₁
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₀ a✝⁴, in₂ c✝¹, in₁ b✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

pp: case in₂₀.in₂₁.in₀₁
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₂ c✝¹, in₀ a✝⁴, in₁ b✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

pp: case in₁₂.in₁₀.in₂₀
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₁ b✝¹, in₂ c✝¹, in₀ a✝²} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

pp: case in₂₁.in₂₀.in₁₀
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₂ c✝¹, in₁ b✝¹, in₀ a✝²} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

Tactic:
<;>

Goal state after:
case in₀₁.in₀₂.in₁₂
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₀ a✝⁴, in₁ b✝¹, in₂ c✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

case in₁₀.in₁₂.in₀₂
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₁ b✝¹, in₀ a✝⁴, in₂ c✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

case in₀₂.in₀₁.in₂₁
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₀ a✝⁴, in₂ c✝¹, in₁ b✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

case in₂₀.in₂₁.in₀₁
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₂ c✝¹, in₀ a✝⁴, in₁ b✝} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

case in₁₂.in₁₀.in₂₀
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₁ b✝¹, in₂ c✝¹, in₀ a✝²} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

case in₂₁.in₂₀.in₁₀
α : 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 c,
    {in₀ a, in₁ b, in₂ c} = {in₂ c✝¹, in₁ b✝¹, in₀ a✝²} ∧
      (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)