awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
c_1 : γ
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁ : a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₂ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₂ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₃ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₄ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₅ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₆ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₇ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₉ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₀ h₂₁ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₃ h₂₄ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₅ : a_2 = in₁ b → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₇ h₂₈ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
have h₂₉ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
Tactic: try tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
c_1 : γ
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁ : a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₂ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₂ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₃ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₄ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₅ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₆ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₇ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₉ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₀ h₂₁ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₃ h₂₄ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₅ : a_2 = in₁ b → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₇ h₂₈ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₉ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₀ h₃₁ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
have h₃₂ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
Tactic: try tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
⊢ ∃ (a : α) (b_2 : β) (c_2 : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b_2, in₂ c_2} {in₂ c, in₁ b, in₀ a_1} ∧
      (graph t).Adj (in₀ a) (in₁ b_2) ∧ (graph t).Adj (in₀ a) (in₂ c_2) ∧ (graph t).Adj (in₁ b_2) (in₂ c_2)
have in₂₁ : (graph t).Adj (in₀ a_1) (in₁ b)
Tactic: refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
      ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
in₂₁ : (graph t).Adj (in₀ a_1) (in₁ b)
⊢ ∃ (a : α) (b_2 : β) (c_2 : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b_2, in₂ c_2} {in₂ c, in₁ b, in₀ a_1} ∧
      (graph t).Adj (in₀ a) (in₁ b_2) ∧ (graph t).Adj (in₀ a) (in₂ c_2) ∧ (graph t).Adj (in₁ b_2) (in₂ c_2)
have in₂₂ : (graph t).Adj (in₀ a_1) (in₂ c)
Tactic: refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
      ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
in₂₁ : (graph t).Adj (in₀ a_1) (in₁ b)
in₂₂ : (graph t).Adj (in₀ a_1) (in₂ c)
⊢ ∃ (a : α) (b_2 : β) (c_2 : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b_2, in₂ c_2} {in₂ c, in₁ b, in₀ a_1} ∧
      (graph t).Adj (in₀ a) (in₁ b_2) ∧ (graph t).Adj (in₀ a) (in₂ c_2) ∧ (graph t).Adj (in₁ b_2) (in₂ c_2)
have in₂₃ : (graph t).Adj (in₁ b) (in₂ c)
Tactic: refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
      ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x)
have simp : (∃ (c : γ), (x.1, x.2.1, c) ∈ t) ∧ (∃ (b : β), (x.1, b, x.2.2) ∈ t) ∧ ∃ (a : α), (a, x.2.1, x.2.2) ∈ t
Tactic: simp only [toTriangle_apply, is3Clique_triple_iff, in₀₁_iff, in₀₂_iff, in₁₂_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
have in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t →
    ∃ z ∈ t,
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
Tactic: cases hxy
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
in₀₁ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
have in₁₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t →
    ∃ z ∈ t,
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
Tactic: cases hxy
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
in₀₁ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
in₁₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
have in₀₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t →
    ∃ z ∈ t,
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
Tactic: cases hxy
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
in₀₁ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
in₁₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
in₀₂ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
have in₂₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t →
    ∃ z ∈ t,
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
Tactic: cases hxy
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
in₀₁ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
in₁₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
in₀₂ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
in₂₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
have in₁₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t →
    ∃ z ∈ t,
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
Tactic: cases hxy
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
in₀₁ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
in₁₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
in₀₂ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
in₂₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
in₁₂ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
have in₂₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t →
    ∃ z ∈ t,
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
Tactic: cases hxy
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
⊢ (graph t).IsNClique 3 s ↔ ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s
have refine_1 : ∀ (h : (graph t).IsNClique 3 s), ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
refine_1 : ∀ (h : (graph t).IsNClique 3 s), ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s
⊢ (graph t).IsNClique 3 s ↔ ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s
have refine_2 : (∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s) → (graph t).IsNClique 3 s
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h : (graph t).IsNClique 3 s
⊢ ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s
have h₁ : ∃ (a : α ⊕ β ⊕ γ) (b : α ⊕ β ⊕ γ) (c : α ⊕ β ⊕ γ),
  (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}
Tactic: rw [is3Clique_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h :
  ∃ (a : α ⊕ β ⊕ γ) (b : α ⊕ β ⊕ γ) (c : α ⊕ β ⊕ γ),
    (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}
⊢ ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s
have refine_1 : ∀ (x y z : α ⊕ β ⊕ γ) (hxy : (graph t).Adj x y) (hxz : (graph t).Adj x z) (hyz : (graph t).Adj y z),
  ∃ x_1 ∈ t,
    Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
      ({x, y, z} : Finset (α ⊕ β ⊕ γ))
Tactic: obtain ⟨x, y, z, hxy, hxz, hyz, rfl⟩ := h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
⊢ ∃ x_1 ∈ t,
    Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
      ({x, y, z} : Finset (α ⊕ β ⊕ γ))
have refine_1 : ∀ (a : α) (b : β) (c : γ) (habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z})
  (hab : (graph t).Adj (in₀ a) (in₁ b)) (hac : (graph t).Adj (in₀ a) (in₂ c)) (hbc : (graph t).Adj (in₁ b) (in₂ c)),
  ∃ x_1 ∈ t,
    Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
      ({x, y, z} : Finset (α ⊕ β ⊕ γ))
Tactic: obtain ⟨a, b, c, habc, hab, hac, hbc⟩ := graph_triple hxy hxz hyz
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
⊢ ∃ x_1 ∈ t,
    Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
      ({x, y, z} : Finset (α ⊕ β ⊕ γ))
have refine_1 : (a, b, c) ∈ t
Tactic: refine ⟨(a, b, c), ?_, habc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
⊢ (a, b, c) ∈ t
have refine_1 : ∀ (c' : γ) (hc' : (a, b, c') ∈ t), (a, b, c) ∈ t
Tactic: obtain ⟨c', hc'⟩ := in₀₁_iff.1 hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
c' : γ
hc' : (a, b, c') ∈ t
⊢ (a, b, c) ∈ t
have refine_1 : ∀ (b' : β) (hb' : (a, b', c) ∈ t), (a, b, c) ∈ t
Tactic: obtain ⟨b', hb'⟩ := in₀₂_iff.1 hac